X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_acic%2Fcic2acic.ml;h=bb00476b97b73faf25e2fed68d891855c3a06aaf;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=8540e0e6492fb4c15c3026e38f47c94b38e52202;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml index 8540e0e64..bb00476b9 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} ;; @@ -86,16 +82,28 @@ let fresh_id seed ids_to_terms ids_to_father_ids = let source_id_of_id id = "#source#" ^ id;; -exception NotEnoughElements;; +exception NotEnoughElements of string;; (*CSC: cut&paste da cicPp.ml *) (* get_nth l n returns the nth element of the list l if it exists or *) (* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = +let rec get_nth msg l n = match (n,l) with (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements + | (n, he::tail) when n > 1 -> get_nth msg tail (n-1) + | (_,_) -> raise (NotEnoughElements msg) +;; + + +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 @@ -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,17 +167,17 @@ 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. *) { D.synthesized = (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) - if global_computeinnertypes then + (*if global_computeinnertypes then Cic.Sort (Cic.Type (CicUniv.fresh())) - else - CicReduction.whd context (xxx_type_of_aux' metasenv context tt); + else*) + 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 -> () @@ -210,7 +224,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes match tt with C.Rel n -> let id = - match get_nth context n with + match get_nth "1" context n with (Some (C.Name s,_)) -> s | _ -> "__" ^ string_of_int n in @@ -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 @@ -332,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes 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 @@ -349,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes 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 @@ -371,7 +400,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 +489,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 @@ -479,30 +508,30 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = let aconjecture_of_conjecture' = aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed in - let eta_fix metasenv context t = + let eta_fix_and_unshare metasenv context t = let t = if eta_fix then E.eta_fix metasenv context t else t in Unshare.unshare t in let aobj = match obj with C.Constant (id,Some bo,ty,params,attrs) -> - let bo' = eta_fix [] [] bo in - let ty' = eta_fix [] [] ty in + let bo' = (*eta_fix_and_unshare[] [] bo*) Unshare.unshare bo in + let ty' = eta_fix_and_unshare [] [] 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 C.AConstant ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs) | C.Constant (id,None,ty,params,attrs) -> - let ty' = eta_fix [] [] ty in + let ty' = eta_fix_and_unshare [] [] ty in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in C.AConstant ("mettereaposto",None,id,None,aty,params,attrs) | C.Variable (id,bo,ty,params,attrs) -> - let ty' = eta_fix [] [] ty in + let ty' = eta_fix_and_unshare [] [] ty in let abo = match bo with None -> None | Some bo -> - let bo' = eta_fix [] [] bo in + let bo' = eta_fix_and_unshare [] [] bo in Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty')) in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in @@ -519,16 +548,16 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = match d with None -> None | Some (n, C.Decl t)-> - Some (n, C.Decl (eta_fix conjectures canonical_context' t)) + Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t)) | Some (n, C.Def (t,None)) -> Some (n, - C.Def ((eta_fix conjectures canonical_context' t),None)) + C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None)) | Some (_,C.Def (_,Some _)) -> assert false in d::canonical_context' ) canonical_context [] in - let term' = eta_fix conjectures canonical_context' term in + let term' = eta_fix_and_unshare conjectures canonical_context' term in (i,canonical_context',term') ) conjectures in @@ -542,9 +571,9 @@ 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 ty' = eta_fix conjectures' [] ty in + (* let bo' = eta_fix conjectures' [] bo in *) + let bo' = bo in + let ty' = eta_fix_and_unshare conjectures' [] ty in (* let time2 = Sys.time () in prerr_endline @@ -614,7 +643,7 @@ let plain_acic_term_of_cic_term = match t with C.Rel n -> let idref,id = - match get_nth context n with + match get_nth "2" context n with idref,(Some (C.Name s,_)) -> idref,s | idref,_ -> idref,"__" ^ string_of_int n in @@ -666,9 +695,12 @@ let plain_acic_term_of_cic_term = 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 @@ -677,9 +709,12 @@ let plain_acic_term_of_cic_term = ) 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