From 7c3850896b6324306bdbe8ef430f500cc9cb7f83 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 10 Apr 2008 18:14:47 +0000 Subject: [PATCH] New: cache of translated fixpoints (to avoid the generative fix restriction and to avoid pollution of the environment). Many more Matita objects now pass. TODO: the caching machinery should be debugged and better understood (what about metasenv and subst?) --- helm/software/components/ng_kernel/Makefile | 2 +- .../software/components/ng_kernel/alluris.txt | 115 ++++++------ .../components/ng_kernel/oCic2NCic.ml | 165 ++++++++++++++---- 3 files changed, 192 insertions(+), 90 deletions(-) diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 8269534d5..56915b13e 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -4,9 +4,9 @@ PREDICATES = INTERFACE_FILES = \ nUri.mli \ nReference.mli \ - oCic2NCic.mli \ nCicUtils.mli \ nCicSubstitution.mli \ + oCic2NCic.mli \ nCicEnvironment.mli \ nCicPp.mli \ nCicReduction.mli \ diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt index 84385385c..4692a4f14 100644 --- a/helm/software/components/ng_kernel/alluris.txt +++ b/helm/software/components/ng_kernel/alluris.txt @@ -1,3 +1,59 @@ +cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con +cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con +cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con +cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con +cic:/matita/algebra/CoRN/SetoidFun/app_strext.con +cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con +cic:/matita/algebra/CoRN/SetoidFun/appA.con +cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con +cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con +cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con +cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con +cic:/matita/algebra/CoRN/SetoidFun/UR.con +cic:/matita/algebra/CoRN/SetoidFun/UQ.con +cic:/matita/algebra/CoRN/SetoidFun/UP.con +cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con +cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con +cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con +cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind +cic:/matita/algebra/CoRN/SetoidFun/Tapp.con +cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con +cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con +cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con +cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con +cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con +cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con +cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con +cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind +cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con +cic:/matita/algebra/CoRN/SetoidFun/Inv.con +cic:/matita/algebra/CoRN/SetoidFun/Fid.con +cic:/matita/algebra/CoRN/SetoidFun/Fconst.con +cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con +cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con +cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con +cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con +cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con +cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con +cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con +cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind +cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con +cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con +cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con +cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con +cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind +cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con +cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con +cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con +cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind +cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con +cic:/matita/algebra/CoRN/SetoidFun/BR.con +cic:/matita/algebra/CoRN/SetoidFun/BQ.con +cic:/matita/algebra/CoRN/SetoidFun/BP.con +cic:/matita/algebra/CoRN/SetoidFun/Astar.con +cic:/matita/demo/realisability/correct2.con +cic:/matita/demo/realisability/correct.con +cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con cic:/matita/demo/realisability/type_OF_SP.con cic:/matita/demo/realisability/true_impl_realized.con cic:/matita/demo/realisability/sigma_rect.con @@ -2057,65 +2113,6 @@ cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con cic:/matita/technicalities/setoids/relation_class_of_argument_class.con cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con -# -- fine -- -# # the same fix in different contexts has different lamb-lifted counterpart + generative fix -# cic:/matita/demo/realisability/correct2.con -# cic:/matita/demo/realisability/correct.con -# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con -# # depending on the previous -# cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con -# cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con -# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con -# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con -# cic:/matita/algebra/CoRN/SetoidFun/app_strext.con -# cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con -# cic:/matita/algebra/CoRN/SetoidFun/appA.con -# cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con -# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con -# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con -# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con -# cic:/matita/algebra/CoRN/SetoidFun/UR.con -# cic:/matita/algebra/CoRN/SetoidFun/UQ.con -# cic:/matita/algebra/CoRN/SetoidFun/UP.con -# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con -# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con -# cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con -# cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind -# cic:/matita/algebra/CoRN/SetoidFun/Tapp.con -# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con -# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con -# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con -# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con -# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con -# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con -# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con -# cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind -# cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con -# cic:/matita/algebra/CoRN/SetoidFun/Inv.con -# cic:/matita/algebra/CoRN/SetoidFun/Fid.con -# cic:/matita/algebra/CoRN/SetoidFun/Fconst.con -# cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con -# cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con -# cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con -# cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con -# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con -# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con -# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con -# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind -# cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con -# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con -# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con -# cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con -# cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind -# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con -# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con -# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con -# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind -# cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con -# cic:/matita/algebra/CoRN/SetoidFun/BR.con -# cic:/matita/algebra/CoRN/SetoidFun/BQ.con -# cic:/matita/algebra/CoRN/SetoidFun/BP.con -# cic:/matita/algebra/CoRN/SetoidFun/Astar.con # # mutual fix # cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con # # depending on the previous diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 8b6fd7f45..3880e361b 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -1,14 +1,67 @@ module Ref = NReference +type ctx = + | Ce of NCic.hypothesis * NCic.obj list + | Fix of Ref.reference * string * NCic.term + +(***** A function to restrict the context of a term getting rid of unsed + variables *******) + +let restrict octx ctx ot = + let odummy = Cic.Implicit None in + let dummy = NCic.Meta (~-1,(0,NCic.Irl 0)) in + let rec aux m acc ot t = + function + [],[] -> (ot,t),acc + | ohe::otl as octx,he::tl -> + if CicTypeChecker.does_not_occur octx 0 1 ot then + aux (m+1) acc (CicSubstitution.subst odummy ot) + (NCicSubstitution.subst dummy t) (otl,tl) + else + (match ohe,he with + None,_ -> assert false + | Some (name,Cic.Decl oty),Ce ((name', NCic.Decl ty),objs) -> + aux (m+1) ((m+1,objs,None)::acc) (Cic.Lambda (name,oty,ot)) + (NCic.Lambda (name',ty,t)) (otl,tl) + | Some (name,Cic.Decl oty),Fix (ref,name',ty) -> + aux (m+1) ((m+1,[],Some ref)::acc) (Cic.Lambda (name,oty,ot)) + (NCic.Lambda (name',ty,t)) (otl,tl) + | Some (name,Cic.Def (obo,oty)),Ce ((name', NCic.Def (bo,ty)),objs) -> + aux (m+1) ((m+1,objs,None)::acc) (Cic.LetIn (name,obo,oty,ot)) + (NCic.LetIn (name',bo,ty,t)) (otl,tl) + | _,_ -> assert false) + | _,_ -> assert false in + let rec split_lambdas_and_letins octx ctx infos (ote,te) = + match infos, ote, te with + ([], _, _) -> octx,ctx,ote + | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) -> + split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx) + (Ce ((name',NCic.Decl so),objs)::ctx) tl (ota,ta) + | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) -> + split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx) + (Fix (r,name',so)::ctx) tl (ota,ta) + | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))-> + split_lambdas_and_letins ((Some (name,(Cic.Def (obo,oty))))::octx) + (Ce ((nam',NCic.Def (bo,ty)),objs)::ctx) tl (ota,ta) + | (_, _, _) -> assert false + in + let long_t,infos = aux 0 [] ot dummy (octx,ctx) in + let clean_octx,clean_ctx,clean_ot= split_lambdas_and_letins [] [] infos long_t + in +(*prerr_endline ("RESTRICT PRIMA: " ^ CicPp.pp ot (List.map (function None -> None | Some (name,_) -> Some name) octx)); +prerr_endline ("RESTRICT DOPO: " ^ CicPp.pp clean_ot (List.map (function None -> None | Some (name,_) -> Some name) clean_octx)); +*) + clean_octx,clean_ctx,clean_ot, List.map (fun (rel,_,_) -> rel) infos +;; + + +(**** The translation itself ****) + let cn_to_s = function | Cic.Anonymous -> "_" | Cic.Name s -> s ;; -type ctx = - | Ce of NCic.hypothesis * NCic.obj list - | Fix of Ref.reference * string * NCic.term - let splat mk_pi ctx t = List.fold_left (fun (t,l) c -> @@ -35,38 +88,47 @@ let context_tassonomy ctx = split true 0 1 ctx ;; -let splat_args_for_rel ctx t = +let splat_args_for_rel ctx t ?rels n_fix = + let rels = + match rels with + Some rels -> rels + | None -> + let rec mk_irl = function 0 -> [] | n -> n::mk_irl (n - 1) in + mk_irl (List.length ctx) + in let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in if free = 0 then t else let rec aux = function - | 0 -> [] - | n -> - match List.nth ctx (n+bound) with - | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> - NCic.Const refe :: aux (n-1) - | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (n+bound)::aux (n-1) - | Ce ((_, NCic.Def _),_) -> aux (n-1) + | n,_ when n = bound + n_fix -> [] + | n,he::tl -> + (match List.nth ctx (n-1) with + | Fix (refe, _, _) when n < primo_ce_dopo_fix -> + NCic.Const refe :: aux (n-1,tl) + | Fix _ | Ce ((_, NCic.Decl _),_)-> NCic.Rel (he - n_fix)::aux(n-1,tl) + | Ce ((_, NCic.Def _),_) -> aux (n-1,tl)) + | _,_ -> assert false in - NCic.Appl (t:: aux free) + NCic.Appl (t:: aux (List.length ctx,rels)) ;; -let splat_args ctx t n_fix = +let splat_args ctx t n_fix rels = let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in if ctx = [] then t else let rec aux = function - | 0 -> [] - | n -> + | 0,[] -> [] + | n,he::tl -> (match List.nth ctx (n-1) with - | Ce ((_, NCic.Decl _),_) when n <= bound -> NCic.Rel n:: aux (n-1) + | Ce ((_, NCic.Decl _),_) when n <= bound -> NCic.Rel he:: aux (n-1,tl) | Fix (refe, _, _) when n < primo_ce_dopo_fix -> - splat_args_for_rel ctx (NCic.Const refe):: aux (n-1) - | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (n - n_fix):: aux (n-1) - | Ce ((_, NCic.Def _),_) -> aux (n - 1) + splat_args_for_rel ctx (NCic.Const refe) ~rels n_fix :: aux (n-1,tl) + | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (he - n_fix)::aux(n-1,tl) + | Ce ((_, NCic.Def _),_) -> aux (n - 1,tl) ) + | _,_ -> assert false in - NCic.Appl (t:: aux (List.length ctx)) + NCic.Appl (t:: aux ((List.length ctx,rels))) ;; exception Nothing_to_do;; @@ -210,6 +272,44 @@ let get_fresh,reset_seed = (function () -> seed := 0) ;; +exception Found of NReference.reference;; +let cache = Hashtbl.create 313;; +let same_obj = + function + (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty1,_],_)), + (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty2,_],_)) + when ty1 = ty2 -> true + | _ -> false +;; +let find_in_cache name obj ref = + try + List.iter + (function (ref',obj') -> + let recno = + match ref with + NReference.Ref (_,_,NReference.Fix (_,recno)) -> recno + | _ -> assert false in + let recno' = + match ref' with + NReference.Ref (_,_,NReference.Fix (_,recno)) -> recno + | _ -> assert false in + if recno = recno' && same_obj (obj,obj') then +(*(prerr_endline "!!!!!!!!!!! CACHE HIT !!!!!!!!!!";*) + raise (Found ref') +(*);*) +(* + else +(prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref'); + raise Not_found +) +*) + ) (Hashtbl.find_all cache name); +(*prerr_endline "<<< CACHE MISS >>>";*) + Hashtbl.add cache name (ref,obj); + None + with Found ref -> Some ref +;; + (* we are lambda-lifting also variables that do not occur *) (* ctx does not distinguish successive blocks of cofix, since there may be no * lambda separating them *) @@ -259,9 +359,12 @@ let convert_term uri t = in splat_args ctx (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno))) - n_fix, + n_fix (assert false), fixpoints @ [obj] - | Cic.Fix (fixno, fl) -> + | Cic.Fix _ as fix -> + let octx,ctx,fix,rels = restrict octx ctx fix in + let fixno,fl = + match fix with Cic.Fix (fixno,fl) -> fixno,fl | _ -> assert false in let buri = UriManager.uri_of_string (UriManager.buri_of_uri uri^"/"^ @@ -307,18 +410,20 @@ let convert_term uri t = in let obj = NUri.nuri_of_ouri buri,max_int,[],[], - NCic.Fixpoint (true, fl, (`Generated, `Definition)) + NCic.Fixpoint (true, fl, (`Generated, `Definition)) in + let r = Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in + let obj,r = + let _,name,_,_,_ = List.hd fl in + match find_in_cache name obj r with + Some r' -> [],r' + | None -> [obj],r in - splat_args ctx - (NCic.Const - (Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)))) - n_fix, - fixpoints @ [obj] + splat_args ctx (NCic.Const r) n_fix rels, fixpoints @ obj | Cic.Rel n -> let bound, _, _, primo_ce_dopo_fix = context_tassonomy ctx in (match List.nth ctx (n-1) with | Fix (r,_,_) when n < primo_ce_dopo_fix -> - splat_args_for_rel ctx (NCic.Const r), [] + splat_args_for_rel ctx (NCic.Const r) n_fix, [] | Ce _ when n <= bound -> NCic.Rel n, [] | Fix _ when n <= bound -> assert false | Fix _ | Ce _ when k = true -> NCic.Rel n, [] -- 2.39.2