(* 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
| 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}
;;
| (_,_) -> 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
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
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 *)
(* *)
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. *)
(*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' ; *)
(* 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 -> ()
(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
let fresh_idrefs =
List.map (function _ -> gen_id seed) funs in
let new_idrefs = List.rev fresh_idrefs @ idrefs in
- let tys =
- List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) funs
in
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = `Prop then
let fresh_idrefs =
List.map (function _ -> gen_id seed) funs in
let new_idrefs = List.rev fresh_idrefs @ idrefs in
- let tys =
- List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) funs
in
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = `Prop then
("+++++++++++++ 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 =
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
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
= 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
C.AMutCase (fresh_id, uri, tyno, aux context outty,
aux context term, List.map (aux context) patterns)
| C.Fix (funno, funs) ->
- let tys =
- List.map
- (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+ len+1
+ ) ([],0) funs
in
C.AFix (fresh_id, funno,
List.map2
) tys funs
)
| C.CoFix (funno, funs) ->
- let tys =
- List.map (fun (name,ty,_) ->
- mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+ len+1
+ ) ([],0) funs
in
C.ACoFix (fresh_id, funno,
List.map2
projects / helm.git / blobdiff