X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=071377c63f0a90eb5665c85ce80043e9032557e0;hb=2b53a3735b2a6130726e0a0451993cd679fd5935;hp=1660df50dd9401d80c445f92388d1271d566c1aa;hpb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 1660df50d..071377c63 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 ******************************************************************)
 
@@ -92,7 +93,7 @@ let push st = {st with case = 1 :: st.case}
 
 let inc st =
    {st with case = match st.case with 
-      | []       -> assert false
+      | []       -> []
       | hd :: tl -> succ hd :: tl
    }
 
@@ -146,12 +147,6 @@ try
    with Not_found -> `Type (CicUniv.fresh())
 with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
-let get_type msg st bo =
-try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
-   ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -160,16 +155,6 @@ let get_entry st id =
    in
    aux st.context
 
-let get_ind_names uri tno =
-try   
-   let ts = match E.get_obj Un.oblivion_ugraph uri with
-      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
-      | _                                      -> assert false
-   in
-   match List.nth ts tno with
-      | (_, _, _, cs) -> List.map fst cs  
-with Invalid_argument _ -> failwith "A2P.get_ind_names"
-
 let string_of_atomic = function
    | C.ARel (_, _, _, s)               -> s
    | C.AVar (_, uri, _)                -> H.name_of_uri uri None None
@@ -187,6 +172,8 @@ let get_sub_names head l =
    let names, _ = List.fold_left map ([], 1) l in 
    List.rev names
 
+let get_type msg st t = H.get_type msg st.context (H.cic t) 
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "PREMISE"
@@ -208,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)
@@ -232,7 +219,7 @@ 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 =
@@ -355,7 +342,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 classes2, tl2, _, where = split2_last classes tl in
 	    let script2 = List.rev (mk_arg st where) @ script in
 	    let synth2 = I.S.add 1 synth in
-	    let names = get_ind_names uri tyno in
+	    let names = H.get_ind_names uri tyno in
 	    let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
             if List.length qs <> List.length names then
 	       let qs = proc_bkd_proofs (next st) synth [] classes tl in
@@ -503,10 +493,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       context     = [];
       case        = []
    } in
+   L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st ?flavour anobj in
+   L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
-   List.rev (T.render_steps [] steps)
+   let r = List.rev (T.render_steps [] steps) in
+   L.time_stamp "P : DONE     "; r
 
 let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    prefix context annterm =