From: Ferruccio Guidi 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