From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 May 2007 17:08:57 +0000 (+0000)
Subject: more informations on nodes, fixed a bug on conversion, we use ; instead of . whenever... 
X-Git-Tag: make_still_working~6334
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2921483dad22e14c2e697cbe5597a0b32af04090;p=helm.git

more informations on nodes, fixed a bug on conversion, we use ; instead of . whenever possible in rendering
---

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 4ccb78ace..3ee088696 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -215,16 +215,16 @@ let get_intro = function
    | C.Anonymous -> None
    | C.Name s    -> Some s
 
-let mk_intros st script =
+let mk_intros st what script =
    let intros st script =
       if st.intros = [] then script else
       let count = List.length st.intros in
       T.Intros (Some count, List.rev st.intros, "") :: script
    in
    let clears st script =
-      if st.clears = [] then script else T.Clear (st.clears, st.clears_note) :: script
+      if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
    in
-   intros st (clears st script)   
+   intros st (clears st (convert st what @ script))   
 
 let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
@@ -289,18 +289,18 @@ and proc_letin st what name v t =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_rel st what = 
    let _, dtext = test_depth st in
    let text = "assumption" in
    let script = [T.Apply (what, dtext ^ text)] in 
-   mk_intros st script
+   mk_intros st what script
 
 and proc_mutconstruct st what = 
    let _, dtext = test_depth st in
    let script = [T.Apply (what, dtext)] in 
-   mk_intros st script   
+   mk_intros st what script   
 
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
@@ -320,7 +320,7 @@ and proc_appl st what hd tl =
       in
       let synth = mk_synth I.S.empty decurry in
       let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
-      let script = List.rev (mk_arg st hd) @ convert st what in
+      let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
 	    let classes, tl, _, where = split2_last classes tl in
@@ -345,12 +345,12 @@ and proc_appl st what hd tl =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_other st what =
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
    let script = [T.Note text] in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_proof st t = 
    let f st =
diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 93cb16545..19d96a91a 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -261,12 +261,13 @@ and opt2_term g c t =
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       let g bo = 
-         Printf.eprintf "Optimized: %s\nNodes    : %u" 
+         Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
 	    (Pp.ppterm bo) (I.count_nodes 0 bo);
 	 let _ = H.get_type [] (C.Cast (bo, ty)) in
 	 C.Constant (name, Some bo, ty, pars, attrs)
       in
-      Printf.eprintf "BEGIN: %s\n" name;
+      Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
+         name (I.count_nodes 0 bo);
       begin try opt1_term g (* (opt2_term g []) *) true [] bo
       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
    | obj                                         -> obj
diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 2d3c915f7..8a60f9658 100644
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -208,7 +208,7 @@ and render_steps sep a = function
    | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
       render_steps sep (render_step mk_sc a p) ps
    | p :: ps                                     ->
-      render_steps sep (render_step mk_dot a p) ps
+      render_steps sep (render_step mk_sc a p) ps
 
 let render_steps a = render_steps mk_dot a