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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 4ccb78ace32522efbd43d8b9706bbe7f81deca71..3ee088696db48a6bc58eb67372214132f5df906c 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/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/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml
index 93cb165452d1996d5d375c9d274f1679e4b6e956..19d96a91aa7ef042f7113656a43cb8a4ce99f4fa 100644 (file)
--- a/components/acic_procedural/proceduralOptimizer.ml
+++ b/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/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index 2d3c915f7234e7ed8b7437086277ec4d77740d85..8a60f9658047118ad4c8c0ddc7b2dc4674d19326 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/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