From 2921483dad22e14c2e697cbe5597a0b32af04090 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 May 2007 17:08:57 +0000
Subject: [PATCH] more informations on nodes, fixed a bug on conversion, we use
; instead of . whenever possible in rendering
---
.../acic_procedural/acic2Procedural.ml | 18 +++++++++---------
.../acic_procedural/proceduralOptimizer.ml | 5 +++--
.../acic_procedural/proceduralTypes.ml | 2 +-
3 files changed, 13 insertions(+), 12 deletions(-)
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
--
2.39.5