From b266ed97b63400d62ab4ba6a4ebdfbc1d5b0c2bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Sep 2009 15:57:02 +0000 Subject: [PATCH] fixed coercion mechanism w.r.t. undo/require --- .../grafite_engine/grafiteEngine.ml | 24 ++- .../grafite_engine/nCicCoercDeclaration.ml | 174 +++++++++++------- .../grafite_engine/nCicCoercDeclaration.mli | 10 +- .../components/ng_kernel/nCicLibrary.ml | 3 - helm/software/matita/nlibrary/sets/sets.ma | 4 +- 5 files changed, 130 insertions(+), 85 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index f7df56315..ec9f3866f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -41,6 +41,11 @@ type options = { do_heavy_checks: bool ; } +let concat_nuris uris nuris = + match uris,nuris with + | `New uris, `New nuris -> `New (nuris@uris) + | _ -> assert false +;; (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) @@ -767,9 +772,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = eval_ncommand opts status ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml)) in - match uris,nuris with - `New uris, `New nuris -> status,`New (nuris@uris) - | _ -> assert false + status, concat_nuris uris nuris with NCicTypeChecker.TypeCheckerFailure msg when Lazy.force msg = @@ -785,16 +788,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (fun (name,is_coercion,arity) -> if is_coercion then Some(name,leftno,arity) else None) fields | _ -> [] in - let status = + let status,uris = List.fold_left - (fun status (name,cpos,arity) -> + (fun (status,uris) (name,cpos,arity) -> let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,CicNotationPt.Ident (name,None)) in assert (metasenv = [] && subst = []); - NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity - status (name,t,cpos,arity) - ) status coercions + let status, nuris = + NCicCoercDeclaration. + basic_eval_and_record_ncoercion_from_t_cpos_arity + status (name,t,cpos,arity) + in + let uris = concat_nuris nuris uris in + status, uris) + (status,uris) coercions in status,uris with diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml index 141ae369e..550cb93c4 100644 --- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml @@ -130,14 +130,61 @@ let only_head = function | t -> t ;; -let basic_eval_ncoercion (name,t,s,d,p,a) status = - let to_s = - NCicCoercion.look_for_coercion status [] [] [] skel_dummy s +let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = + let status, src, cpos = + let rec aux cpos ctx = function + | NCic.Prod (name,ty,bo) -> + if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo + else + (try + let metasenv,subst,status,src = + GrafiteDisambiguate.disambiguate_nterm + None status ctx [] [] ("",0,src) in + let src = NCicUntrusted.apply_subst subst [] src in + (* CHECK that the declared pattern matches the abstraction *) + let _ = NCicUnification.unify status metasenv subst ctx ty src in + let src = cleanup_skel () src in + status, src, cpos + with + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ + | MultiPassDisambiguator.DisambiguationError _ -> + raise (GrafiteTypes.Command_error "bad source pattern")) + | _ -> assert false + in + aux 0 [] ty in - let from_d = - NCicCoercion.look_for_coercion status [] [] [] d skel_dummy + let status, tgt, arity = + let metasenv,subst,status,tgt = + GrafiteDisambiguate.disambiguate_nterm + None status [] [] [] ("",0,tgt) in + let tgt = NCicUntrusted.apply_subst subst [] tgt in + (* CHECK che sia unificabile mancante *) + let rec count_prod = function + | NCic.Prod (_,_,x) -> 1 + count_prod x + | _ -> 0 + in + let arity = count_prod tgt in + let tgt= + if arity > 0 then cleanup_funclass_skel tgt + else cleanup_skel () tgt + in + status, tgt, arity in - let status = NCicCoercion.index_coercion status name t s d a p in + status, src, tgt, cpos, arity +;; + +let fresh_uri status prefix suffix = + let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in + let rec diverge u i = + if NCicLibrary.aliases_of u = [] then u + else diverge (mk ("__" ^ string_of_int i)) (i+1) + in + diverge (mk "") 0 +;; + + +let close_graph name t s d to_s from_d p a status = let c = List.find (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) @@ -194,86 +241,77 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity)); - Some (name,bo,src,tgt,arity,pos) + let uri = fresh_uri status name ".con" in + let obj_kind = NCic.Constant + ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity)) + in + let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in + let obj = uri,height,[],[],obj_kind in + let c = + NCic.Const + (NReference.reference_of_spec uri (NReference.Def height)) + in + Some (obj,name,c,src,tgt,pos,arity) with | NCicTypeChecker.TypeCheckerFailure _ | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None ) composites in + composites +;; + +(* idempotent *) +let basic_index_ncoercion (name,t,s,d,position,arity) status = + NCicCoercion.index_coercion status name t s d arity position +;; + +let basic_eval_ncoercion (name,t,s,d,p,a) status = + let to_s = + NCicCoercion.look_for_coercion status [] [] [] skel_dummy s + in + let from_d = + NCicCoercion.look_for_coercion status [] [] [] d skel_dummy + in + let status = NCicCoercion.index_coercion status name t s d a p in + let composites = close_graph name t s d to_s from_d p a status in List.fold_left - (fun st (name,t,s,d,a,p) -> NCicCoercion.index_coercion st name t s d a p) - status composites + (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> + let info = name,t,s,d,p,a in + let st = NCicLibrary.add_obj st obj in + let st = basic_index_ncoercion info st in + uri::uris, info::infos, st) + ([],[],status) composites ;; -let inject_ncoercion = - let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe - ~refresh_uri_in_term - = +let record_ncoercion = + let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term = let t = refresh_uri_in_term t in let s = refresh_uri_in_term s in let d = refresh_uri_in_term d in - basic_eval_ncoercion (name,t,s,d,p,a) + basic_index_ncoercion (name,t,s,d,p,a) in - NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion -;; - -let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = - let status, src, cpos = - let rec aux cpos ctx = function - | NCic.Prod (name,ty,bo) -> - if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo - else - (try - let metasenv,subst,status,src = - GrafiteDisambiguate.disambiguate_nterm - None status ctx [] [] ("",0,src) in - let src = NCicUntrusted.apply_subst subst [] src in - (* CHECK that the declared pattern matches the abstraction *) - let _ = NCicUnification.unify status metasenv subst ctx ty src in - let src = cleanup_skel () src in - status, src, cpos - with - | NCicUnification.UnificationFailure _ - | NCicUnification.Uncertain _ - | MultiPassDisambiguator.DisambiguationError _ -> - raise (GrafiteTypes.Command_error "bad source pattern")) - | _ -> assert false - in - aux 0 [] ty - in - let status, tgt, arity = - let metasenv,subst,status,tgt = - GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,tgt) in - let tgt = NCicUntrusted.apply_subst subst [] tgt in - (* CHECK che sia unificabile mancante *) - let rec count_prod = function - | NCic.Prod (_,_,x) -> 1 + count_prod x - | _ -> 0 - in - let arity = count_prod tgt in - let tgt= - if arity > 0 then cleanup_funclass_skel tgt - else cleanup_skel () tgt - in - status, tgt, arity - in - status, src, tgt, cpos, arity + let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term = + List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l + in + NRstatus.Serializer.register "ncoercion" aux_l ;; -let basic_eval_and_inject_ncoercion infos status = - let status = basic_eval_ncoercion infos status in - let dump = inject_ncoercion infos::status#dump in - status#set_dump dump +let basic_eval_and_record_ncoercion infos status = + let uris, cinfos, status = basic_eval_ncoercion infos status in + let dump = record_ncoercion (infos::cinfos) :: status#dump in + status#set_dump dump, uris ;; -let basic_eval_and_inject_ncoercion_from_t_cpos_arity +let basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) = let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in - basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status + let status, uris = + basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status + in + status,`New uris ;; let eval_ncoercion status name t ty (id,src) tgt = @@ -289,9 +327,9 @@ let eval_ncoercion status name t ty (id,src) tgt = let status, src, tgt, cpos, arity = src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in - let status = - basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status + let status, uris = + basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status in - status,`New [] + status,`New uris ;; diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli index 666981568..aee0e9fc3 100644 --- a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli @@ -12,17 +12,17 @@ (* evals a coercion declaration statement: name t ty (id,src) tgt *) val eval_ncoercion: - GrafiteTypes.status as 'status -> + #GrafiteTypes.status as 'status -> string -> CicNotationPt.term -> CicNotationPt.term -> string * CicNotationPt.term -> - CicNotationPt.term -> 'status * [> `New of 'c list ] + CicNotationPt.term -> 'status * [> `New of NUri.uri list ] (* for records, the term is the projection, already refined, while the * first integer is the number of left params and the second integer is * the arity in the `:arity>` syntax *) -val basic_eval_and_inject_ncoercion_from_t_cpos_arity: - (GrafiteTypes.status as 'status) -> - string * NCic.term * int * int -> 'status +val basic_eval_and_record_ncoercion_from_t_cpos_arity: + #GrafiteTypes.status as 'status -> + string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ] diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index fb733cdfc..9a2842e0e 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -270,12 +270,9 @@ let resolve name = ;; let aliases_of uri = - try HExtlib.filter_map (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !local_aliases - with - Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) ;; let add_obj status ((u,_,_,_,_) as obj) = diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index f3bd3b889..f140ef770 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -39,7 +39,6 @@ ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }. ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }. -ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?). nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S. #A; #S; #x; #H; nassumption. @@ -62,6 +61,9 @@ nqed. include "sets/setoids1.ma". +(* this has to be declared here, so that it is combined with carr *) +ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?). + ndefinition powerclass_setoid: Type[0] → setoid1. #A; @[ napply (Ω^A)| napply seteq ] nqed. -- 2.39.2