X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2Fcic2acic.ml;h=d8392f6206ab745e2647a75286e30745e481e18a;hb=5682bf51adcde903c53a96e05475a7ded8fb255d;hp=a7d3cbc70e07ad609b9f714594cea80d1a468566;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index a7d3cbc70..d8392f620 100644
--- a/components/cic_acic/cic2acic.ml
+++ b/components/cic_acic/cic2acic.ml
@@ -41,18 +41,12 @@ let sort_of_sort = function
 
 (* let hashtbl_add_time = ref 0.0;; *)
 
+let xxx_add_profiler = HExtlib.profile "xxx_add";;
 let xxx_add h k v =
-(*  let t1 = Sys.time () in *)
-  Hashtbl.add h k v ;
-(*   let t2 = Sys.time () in
-   hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 *)
+ xxx_add_profiler.HExtlib.profile (Hashtbl.add h k) v
 ;;
 
-(* let number_new_type_of_aux' = ref 0;;
-let type_of_aux'_add_time = ref 0.0;; *)
-
 let xxx_type_of_aux' m c t =
-(*  let t1 = Sys.time () in *)
  let res,_ =
    try
     CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
@@ -61,11 +55,13 @@ let xxx_type_of_aux' m c t =
    | CicTypeChecker.TypeCheckerFailure _ ->
        Cic.Sort Cic.Prop, CicUniv.empty_ugraph
   in
-(*  let t2 = Sys.time () in
- type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
  res
 ;;
 
+let xxx_type_of_aux'_profiler = HExtlib.profile "xxx_type_of_aux'";;
+let xxx_type_of_aux' m c t =
+ xxx_type_of_aux'_profiler.HExtlib.profile (xxx_type_of_aux' m c) t
+
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
@@ -98,6 +94,18 @@ let rec get_nth l n =
   | (_,_) -> raise NotEnoughElements
 ;;
 
+
+let profiler_for_find = HExtlib.profile "CicHash" ;;
+let profiler_for_whd = HExtlib.profile "whd" ;;
+
+let cic_CicHash_find a b =  
+  profiler_for_find.HExtlib.profile (Cic.CicHash.find a) b
+;;
+
+let cicReduction_whd c t = 
+ profiler_for_whd.HExtlib.profile (CicReduction.whd c) t
+;;
+
 let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
   seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
   metasenv context idrefs t expectedty
@@ -130,14 +138,13 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
     let rec aux computeinnertypes father context idrefs tt =
      let fresh_id'' = fresh_id' father tt in
      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
-     let aux' = aux computeinnertypes (Some fresh_id'') in
       (* First of all we compute the inner type and the inner sort *)
       (* of the term. They may be useful in what follows.          *)
       (*CSC: This is a very inefficient way of computing inner types *)
       (*CSC: and inner sorts: very deep terms have their types/sorts *)
       (*CSC: computed again and again.                               *)
       let sort_of t =
-       match CicReduction.whd context t with 
+       match cicReduction_whd context t with 
           C.Sort C.Prop  -> `Prop
         | C.Sort C.Set   -> `Set
         | C.Sort (C.Type u) -> `Type u
@@ -148,6 +155,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
             assert false
       in
        let ainnertypes,innertype,innersort,expected_available =
+
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
 (*CSC: (expected type + inferred type). Just for now we use the usual *)
 (*CSC: type-inference, but the result is very poor. As a very weak    *)
@@ -159,7 +167,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
 (* *)
         let {D.synthesized = synthesized; D.expected = expected} =
          if computeinnertypes then
-          Cic.CicHash.find terms_to_types tt
+          cic_CicHash_find terms_to_types tt
          else
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)
@@ -169,7 +177,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
             (*if global_computeinnertypes then
               Cic.Sort (Cic.Type (CicUniv.fresh()))
             else*)
-              CicReduction.whd context (xxx_type_of_aux' metasenv context tt);
+              cicReduction_whd context (xxx_type_of_aux' metasenv context tt);
           D.expected = None}
         in
 (*          incr number_new_type_of_aux' ; *)
@@ -202,6 +210,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
 	  (* TASSI non dovrebbe fare danni *)
 (* *)
        in
+        let aux' =
+         if innersort = `Prop then
+          aux computeinnertypes (Some fresh_id'')
+         else
+          aux false (Some fresh_id'')
+        in
         let add_inner_type id =
          match ainnertypes with
             None -> ()
@@ -287,12 +301,19 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
-             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = `Prop then
-              add_inner_type fresh_id'' ;
-             C.ALetIn
-              (fresh_id'', n, aux' context idrefs s,
-               aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
+             let s_ty =
+              try
+               (cic_CicHash_find terms_to_types s).D.synthesized
+              with
+               Not_found ->
+                cicReduction_whd context (xxx_type_of_aux' metasenv context s);
+             in
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+              if innersort = `Prop then
+               add_inner_type fresh_id'' ;
+              C.ALetIn
+               (fresh_id'', n, aux' context idrefs s,
+                aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = `Prop then
@@ -371,7 +392,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
           res
 *)
-        aux global_computeinnertypes None context idrefs t
+  aux global_computeinnertypes None context idrefs t
 ;;
 
 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
@@ -460,7 +481,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=true) obj =
+let acic_object_of_cic_object ?(eta_fix=false) obj =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
@@ -485,7 +506,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
-       let bo' = eta_fix [] [] bo in
+       let bo' = (*eta_fix [] []*) bo in
        let ty' = eta_fix [] [] ty in
        let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
@@ -542,8 +563,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
              = aconjecture_of_conjecture' conjectures conjecture in
            (cid,i,acanonical_context,aterm))
           conjectures' in 
-(*        let time1 = Sys.time () in *)
-       let bo' = eta_fix conjectures' [] bo in
+       (* let bo' = eta_fix conjectures' [] bo in *)
+       let bo' = bo in
        let ty' = eta_fix conjectures' [] ty in
 (*
        let time2 = Sys.time () in