From 6a4cf39f4ad37545b33db31f3610d960375ce2a5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 May 2006 08:25:34 +0000 Subject: [PATCH] CSC & Andrea patch to speedup the process: typeof called instead of Hashtbl lookup --- helm/software/components/cic_acic/cic2acic.ml | 47 +++++++++++++------ 1 file changed, 32 insertions(+), 15 deletions(-) diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index a7d3cbc70..e1c964c76 100644 --- 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 = -- 2.39.2