CSC & Andrea patch to speedup the process: typeof called instead of Hashtbl lookup

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index a7d3cbc70e07ad609b9f714594cea80d1a468566..e1c964c76073ac21388a1abf79ee9968c0c45e23 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/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
@@ -127,17 +135,17 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
    prerr_endline
     ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
 *)
+    let time = ref 0. in
     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 +156,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 +168,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 +178,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 +211,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 -> ()
@@ -371,7 +386,9 @@ 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
+  let res = aux global_computeinnertypes None context idrefs t in
+  prerr_endline (">>>> aux : " ^ string_of_float !time);
+  res
 ;;
 
 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =