From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 4 Jul 2008 18:46:29 +0000 (+0000)
Subject: - we replaced a normalize with a whd in the classification algorithm
X-Git-Tag: make_still_working~4954
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=790eccfa6b94dc82826d919691f8d4bfadb04573;p=helm.git

- we replaced a normalize with a whd in the classification algorithm
- we turned on the display of the inner types to debug drop/props.ma
---

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index ecd4abc74..29b567731 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -58,6 +58,8 @@ type status = {
    skip_thm_and_qed : bool;
 }
 
+let debug = true
+
 (* helpers ******************************************************************)
 
 let split2_last l1 l2 =
@@ -195,24 +197,32 @@ let mk_exp_args hd tl classes synth =
 let mk_convert st ?name sty ety note =
    let e = Cn.hole "" in
    let csty, cety = H.cic sty, H.cic ety in
-   let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
-      note (Pp.ppterm csty) (Pp.ppterm cety)
+   let script = 
+      if debug then
+         let sname = match name with None -> "" | Some (id, _) -> id in
+         let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
+            note sname (Pp.ppterm csty) (Pp.ppterm cety)
+	 in 
+	 [T.Note note]
+      else []
    in
    assert (Ut.is_sober csty); 
    assert (Ut.is_sober cety);
-   if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
+   if Ut.alpha_equivalence csty cety then script else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
-      | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
+      | None         -> T.Change (sty, ety, None, e, "") :: script
       | Some (id, i) -> 
          begin match get_entry st id with
-	    | C.Def _  -> assert false (* [T.ClearBody (id, note)] *)
-	    | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, "" (* note *))] 
+	    | C.Def _  -> assert false (* T.ClearBody (id, "") :: script *)
+	    | C.Decl _ -> 
+	       T.Change (ety, sty, Some (id, Some id), e, "") :: script 
          end
 
 let convert st ?name v = 
    match get_inner_types st v with
-      | None            -> [(*T.Note "NORMAL: NO INNER TYPES"*)]
+      | None            -> 
+         if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
       | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
 
 let convert_elim st ?name t v pattern =
diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index e69b471ca..981acc969 100644
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -78,7 +78,7 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_normalize (c, t) in
+   let vs, h = PEH.split_with_whd (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in