X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=2531620096f3a2ce1a65dae35a1c13faacbcf4a4;hb=c14ddc094a1cfa93b5337e5aecc6831f72dfc22b;hp=ce6316de1f3ad8702c51b0776543f95ad6d0afda;hpb=2ea5357bace160aaf57750d9dcfb3077fe5a1b38;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index ce6316de1..253162009 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -39,6 +39,7 @@ module PEH  = ProofEngineHelpers
 module HEL  = HExtlib
 module DTI  = DoubleTypeInference
 module NU   = CicNotationUtil
+module L    = Librarian
 
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
@@ -54,7 +55,7 @@ type status = {
    case: int list
 }
 
-let debug = false
+let debug = ref false
 
 (* helpers ******************************************************************)
 
@@ -194,7 +195,7 @@ let mk_convert st ?name sty ety note =
    let e = Cn.hole "" in
    let csty, cety = H.cic sty, H.cic ety in
    let script = 
-      if debug then
+      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)
@@ -218,20 +219,8 @@ let mk_convert st ?name sty ety note =
 let convert st ?name v = 
    match get_inner_types st v with
       | None            -> 
-         if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
+         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 =
-   match t, get_inner_types st t, get_inner_types st v with
-      | _, None, _
-      | _, _, None                                            -> [(* T.Note "ELIM: NO INNER TYPES"*)]
-      | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
-         let where = List.hd (List.rev tl) in
-         let cty = Cn.elim_inferred_type 
-	     st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
-	 in
-         mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
-      | _, Some _, Some _                                     -> assert false
 	  
 let get_intro = function 
    | C.Anonymous -> None
@@ -255,10 +244,9 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
    if (Cn.does_not_occur e) then st, [] else 
    match where with
       | C.ARel (_, _, i, premise) as w ->
-(*         let _script = convert_elim st ~name:(premise, i) v w e in *) 
          let script name =
             let where = Some (premise, name) in
-	    let script = mk_arg st what @ mk_arg st w (* @ script *) in
+	    let script = mk_arg st what @ mk_arg st w in
 	    T.Rewrite (direction, what, where, e, dtext) :: script
 	 in
 	 if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
@@ -278,8 +266,7 @@ let mk_rewrite st dtext where qs tl direction t =
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    let script = [T.Branch (qs, "")] in
-   if (Cn.does_not_occur e) then script else 
-(*   let script = convert_elim st t t e in *)
+   if (Cn.does_not_occur e) then script else
    T.Rewrite (direction, where, None, e, dtext) :: script
 
 let rec proc_lambda st what name v t =
@@ -341,7 +328,10 @@ and proc_const st what =
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
-      let ty = get_type "TC2" st hd in
+      let ty = match get_inner_types st hd with
+         | Some (ity, _) -> H.cic ity 
+	 | None          -> get_type "TC2" st hd 
+      in
       let classes, rc = Cl.classify st.context ty in
       let goal_arity, goal = match get_inner_types st what with
          | None            -> 0, None
@@ -378,7 +368,7 @@ and proc_appl st what hd tl =
 	       let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
 	       let using = Some hd in
-	       (* convert_elim st what what e @ *) script2 @ 
+	       script2 @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let names = get_sub_names hd tl in
@@ -489,13 +479,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       context     = [];
       case        = []
    } in
-   H.print_times "LEVEL 2";
+   L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st ?flavour anobj in
-   H.print_times "RENDERING";
+   L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in
-   H.print_times "DONE     "; r
+   L.time_stamp "P : DONE     "; r
 
 let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    prefix context annterm =