From: Enrico Tassi Date: Mon, 17 Oct 2005 16:01:50 +0000 (+0000) Subject: added coercions to Prod X-Git-Tag: V_0_7_2_3~210 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0245778d76e4d7656c1d8a05dc19738f1a953d68;p=helm.git added coercions to Prod --- diff --git a/helm/matita/contribs/LAMBDA-TYPES/.depend b/helm/matita/contribs/LAMBDA-TYPES/.depend index 98ea66214..85e7c6d76 100644 --- a/helm/matita/contribs/LAMBDA-TYPES/.depend +++ b/helm/matita/contribs/LAMBDA-TYPES/.depend @@ -1,6 +1,18 @@ -/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -./tlt_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo -/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma -./terms_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -./lref_map_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo +/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +./lref_map_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo +/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma /home/tassi/helm/matita/coq.moo +./terms_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +./tlt_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo +!! TOTAL TIME SPENT IN disambiguate_thing: 0. +!! TOTAL TIME SPENT IN disambiguate_thing.refine_thing: 0. +!! TOTAL TIME SPENT IN add_obj: 0. +!! TOTAL TIME SPENT IN add_obj.index_obj: 0. +!! TOTAL TIME SPENT IN add_obj.typecheck_obj: 0. +!! TOTAL TIME SPENT IN alias_diff (conteggiato anche in include): 0. +!! TOTAL TIME SPENT IN disambiguate_thing.refine_thing: 0. +!! TOTAL TIME SPENT IN CicRefine: 0. +!! TOTAL TIME SPENT IN CicRefine.fo_unif: 0. +!! TOTAL TIME SPENT IN clean_and_fill: 0. +!! TOTAL TIME SPENT IN mysql: 0. +!! TOTAL TIME SPENT IN Xml.pp: 0. diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 9b3267fec..5e2526748 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -133,7 +133,7 @@ let _ = (fun (s,t,u) -> MatitaLog.debug (UriManager.name_of_uri u ^ ":" - ^ UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t)) + ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) (CoercDb.to_list ())); addDebugItem "print top-level grammar entries" CicNotationParser.print_l2_pattern; diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 61d69cbb9..20fee8c18 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -568,16 +568,9 @@ let eval_coercion status coercion = in let ty_src,ty_tgt = extract_last_two_p coer_ty in let context = [] in - let src_uri = - let ty_src = CicReduction.whd context ty_src in - CicUtil.uri_of_term ty_src - in - let tgt_uri = - let ty_tgt = CicReduction.whd context ty_tgt in - CicUtil.uri_of_term ty_tgt - in + let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_src) in + let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_tgt) in let new_coercions = - (* also adds them to the Db *) CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in let status = List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status) diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index 7c4031971..1d874def3 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -38,10 +38,10 @@ intros. elim a. clear a.left.left. reflexivity. -clear H.clear H1.clear a.right. - exists.exact s.exists.exact s1.reflexivity. clear H.clear a.left.right. exists.exact s.reflexivity. +clear H.clear H1.clear a.right. + exists.exact s.exists.exact s1.reflexivity. qed. theorem t: 0=0 \to stupidtype. @@ -72,6 +72,7 @@ theorem t: \forall x,y. \forall H: sum x y O. (\lambda a,b,K. y=a \to O=b \to match K with [ (k a b p) \Rightarrow a ] = x) ? ? ? H). + goal 16. simplify. intros. generalize in match H1. rewrite < H2; rewrite < H3.intro. diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index b450d2502..e3392bf05 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -51,7 +51,7 @@ in profiler.HExtlib.profile foo () (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; - + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -259,11 +259,61 @@ and type_of_aux' metasenv context t ugraph = type_of_aux subst' metasenv' ((Some (name,(C.Decl s')))::context) t ugraph1 in - let sop,subst''',metasenv''',ugraph3 = - sort_of_prod subst'' metasenv'' - context (name,s') (sort1,sort2) ugraph2 - in - C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 + (try + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod subst'' metasenv'' + context (name,s') (sort1,sort2) ugraph2 + in + C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 + with + | RefineFailure _ as exn -> + (* given [t] of type [type_to_coerce] returns + * a term that has type [tgt_sort] eventually + * derived from (coercion [t]) *) + let refined_target = t' in + let sort_of_refined_target = sort2 in + let carr t subst context = CicMetaSubst.apply_subst subst t in + let coerce_to_sort tgt_sort t type_to_coerce subst ctx = + match type_to_coerce with + | Cic.Sort _ -> t + | term -> + let coercion_src = carr type_to_coerce subst ctx in + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let search = CoercGraph.look_for_coercion in + (match search coercion_src coercion_tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain "Coercions on metas") + | CoercGraph.SomeCoercion c -> Cic.Appl [c;t]) + in + (* this is probably not the best... *) + let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in + let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in + let new_src = + coerce_to_sort tgt_sort_for_pi_source s sort1 subst context + in + let context_with_new_src = + ((Some (name,(C.Decl new_src)))::context) + in + let new_tgt = + coerce_to_sort + tgt_sort_for_pi_target + refined_target sort_of_refined_target + subst context_with_new_src + in + let newprod = C.Prod (name,new_src,new_tgt) in + let _,sort_of_refined_prod,subst,metasenv,ugraph3 = + type_of_aux subst metasenv context newprod ugraph2 + in + (* this if for a coercion on the tail of the arrow *) + let new_target = + match sort_of_refined_target with + | Cic.Sort _ -> refined_target + | _ -> new_tgt + in + C.Prod(name,new_src,new_target), + sort_of_refined_prod,subst,metasenv,ugraph3) | C.Lambda (n,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -800,35 +850,39 @@ and type_of_aux' metasenv context t ugraph = let t2'' = CicReduction.whd ~subst context_for_t2 t2 in match (t1'', t2'') with (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different than Coq manual!!! *) C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) let t' = CicUniv.fresh() in let ugraph1 = CicUniv.add_ge t' t1 ugraph in let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in C.Sort (C.Type t'),subst,metasenv,ugraph2 | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) C.Sort (C.Type t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we * brake the invariant that refine produce only well typed terms *) - (* TODO if we check the non meta term and if it is a sort then we are - * likely to know the exact value of the result e.g. if the rhs is a - * Sort (Prop | Set | CProp) then the result is the rhs *) + (* TODO if we check the non meta term and if it is a sort then we + * are likely to know the exact value of the result e.g. if the rhs + * is a Sort (Prop | Set | CProp) then the result is the rhs *) let (metasenv,idx) = CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv,ugraph1) = - fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph + fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' ugraph in t2'',subst,metasenv,ugraph1 - | (_,_) -> - raise (RefineFailure (Reason (sprintf - "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" - (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2'')))) + | _,_ -> + raise + (RefineFailure + (Reason + (sprintf + ("Two sorts were expected, found %s " ^^ + "(that reduces to %s) and %s (that reduces to %s)") + (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) + (CicPp.ppterm t2'')))) and eat_prods subst metasenv context hetype tlbody_and_type ugraph = let rec mk_prod metasenv context = @@ -899,13 +953,20 @@ and type_of_aux' metasenv context t ugraph = hete,subst,metasenv,ugraph1 with exn -> (* we search a coercion from hety to s *) - let coer = CoercGraph.look_for_coercion - (CicMetaSubst.apply_subst subst hety) - (CicMetaSubst.apply_subst subst s) + let coer = + let carr t subst context = + CicMetaSubst.apply_subst subst t + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s in match coer with - | None -> raise exn - | Some c -> + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain "Coercions on meta") + | CoercGraph.SomeCoercion c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in let coerced_args,metasenv',subst',t',ugraph2 = diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml index 859445f44..e636f8759 100644 --- a/helm/ocaml/cic_unification/coercDb.ml +++ b/helm/ocaml/cic_unification/coercDb.ml @@ -23,9 +23,41 @@ * http://helm.cs.unibo.it/ *) +type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term +exception EqCarrNotImplemented of string +exception EqCarrOnNonMetaClosed + let db = ref [] let use_coercions = ref true +let coerc_carr_of_term t = + try + Uri (CicUtil.uri_of_term t) + with Invalid_argument _ -> + match t with + | Cic.Sort s -> Sort s + | t -> Term t +;; + +let eq_carr src tgt = + match src, tgt with + | Uri src, Uri tgt -> UriManager.eq src tgt + | Sort (Cic.Type _), Sort (Cic.Type _) -> true + | Sort src, Sort tgt when src = tgt -> true + | Term t1, Term t2 when + CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 -> + raise + (EqCarrNotImplemented + ("Unsupported carr for coercions: " ^ + CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)) + | _ -> raise EqCarrOnNonMetaClosed + +let name_of_carr = function + | Uri u -> UriManager.name_of_uri u + | Sort s -> CicPp.ppsort s + | Term _ -> assert false + + let to_list () = !db diff --git a/helm/ocaml/cic_unification/coercDb.mli b/helm/ocaml/cic_unification/coercDb.mli index ba563ddd6..7b0e6c531 100644 --- a/helm/ocaml/cic_unification/coercDb.mli +++ b/helm/ocaml/cic_unification/coercDb.mli @@ -24,19 +24,25 @@ *) (** XXX WARNING: non-reentrant *) +type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term +exception EqCarrNotImplemented of string +exception EqCarrOnNonMetaClosed +val eq_carr: coerc_carr -> coerc_carr -> bool +val coerc_carr_of_term: Cic.term -> coerc_carr +val name_of_carr: coerc_carr -> string val use_coercions: bool ref (** initial status is true *) val to_list: unit -> - (UriManager.uri * UriManager.uri * UriManager.uri) list + (coerc_carr * coerc_carr * UriManager.uri) list val add_coercion: - UriManager.uri * UriManager.uri * UriManager.uri -> unit + coerc_carr * coerc_carr * UriManager.uri -> unit val remove_coercion: - (UriManager.uri * UriManager.uri * UriManager.uri -> bool) -> unit + (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit val find_coercion: - (UriManager.uri * UriManager.uri -> bool) -> UriManager.uri list + (coerc_carr * coerc_carr -> bool) -> UriManager.uri list diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index c6a929619..469e334a7 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,48 +25,65 @@ open Printf;; +type coercion_search_result = + | SomeCoercion of Cic.term + | NoCoercion + | NotMetaClosed + | NotHandled of string + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () + (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion src tgt = - try - let src = CicUtil.uri_of_term src in - let tgt = CicUtil.uri_of_term tgt in - let l = - CoercDb.find_coercion - (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) - in - match l with - | [] -> debug_print (lazy ":( coercion non trovata"); None - | u::_ -> - debug_print (lazy ( - sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" - (List.length l) - (UriManager.name_of_uri src) - (UriManager.name_of_uri tgt) - (UriManager.name_of_uri u))); - Some (CicUtil.term_of_uri u) - with Invalid_argument s -> - debug_print (lazy (":( coercion non trovata (fallita la uri_of_term): " ^ s)); - None + try + let l = + CoercDb.find_coercion + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) + in + match l with + | [] -> debug_print (lazy ":( coercion non trovata"); NoCoercion + | u::_ -> + debug_print (lazy ( + sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt) + (UriManager.name_of_uri u))); + SomeCoercion (CicUtil.term_of_uri u) + with + | CoercDb.EqCarrNotImplemented s -> NotHandled s + | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed ;; +let look_for_coercion src tgt = + let src_uri = CoercDb.coerc_carr_of_term src in + let tgt_uri = CoercDb.coerc_carr_of_term tgt in + look_for_coercion src_uri tgt_uri + (* given the new coercion uri from src to tgt returns the list * of new coercions to create. hte list elements are * (source, list of coercions to follow, target) *) let get_closure_coercions src tgt uri coercions = - let c_from_tgt = List.filter (fun (f,_,_) -> UriManager.eq f tgt) coercions in - let c_to_src = List.filter (fun (_,t,_) -> UriManager.eq t src) coercions in - (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ - (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ - (List.fold_left ( - fun l (s,_,u1) -> - ((List.map (fun (_,t,u2) -> - (s,[u1;uri;u2],t) - )c_from_tgt)@l) ) - [] c_to_src) + match src,tgt with + | CoercDb.Uri _, CoercDb.Uri _ -> + let c_from_tgt = + List.filter (fun (f,_,_) -> CoercDb.eq_carr f tgt) coercions + in + let c_to_src = + List.filter (fun (_,t,_) -> CoercDb.eq_carr t src) coercions + in + (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ + (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ + (List.fold_left ( + fun l (s,_,u1) -> + ((List.map (fun (_,t,u2) -> + (s,[u1;uri;u2],t) + )c_from_tgt)@l) ) + [] c_to_src) + | _ -> [] (* do not close in case source or target is not an indty ?? *) ;; let obj_attrs = [`Class `Coercion; `Generated] @@ -113,11 +130,16 @@ let filter_duplicates l coercions = List.filter ( fun (src,_,tgt) -> not (List.exists (fun (s,t,u) -> - UriManager.eq s src && - UriManager.eq t tgt) + CoercDb.eq_carr s src && + CoercDb.eq_carr t tgt) coercions)) l +let term_of_carr = function + | CoercDb.Uri u -> CicUtil.term_of_uri u + | CoercDb.Sort _ -> assert false + | CoercDb.Term _ -> assert false + (* given a new coercion uri from src to tgt returns * a list of (new coercion uri, coercion obj, universe graph) *) @@ -133,21 +155,21 @@ let close_coercion_graph src tgt uri = match l with | [] -> assert false | he :: tl -> - let term_of_uri' uri = CicUtil.term_of_uri uri in let first_step = - Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [], - obj_attrs) + Cic.Constant ("", + Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs) in let o,u = - List.fold_left (fun (o,u) coer -> + List.fold_left (fun (o,univ) coer -> match o with | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (term_of_uri' coer) u + generate_composite_closure c (term_of_carr (CoercDb.Uri + coer)) univ | _ -> assert false ) (first_step, CicUniv.empty_ugraph) tl in - let name_src = UriManager.name_of_uri src in - let name_tgt = UriManager.name_of_uri tgt in + let name_src = CoercDb.name_of_carr src in + let name_tgt = CoercDb.name_of_carr tgt in let name = name_tgt ^ "_of_" ^ name_src in let buri = UriManager.buri_of_uri uri in let c_uri = diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli index 03acb4a6d..dfba8f5dc 100644 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -23,11 +23,17 @@ * http://cs.unibo.it/helm/. *) +type coercion_search_result = + | SomeCoercion of Cic.term + | NoCoercion + | NotMetaClosed + | NotHandled of string + val look_for_coercion : - Cic.term -> Cic.term -> Cic.term option + Cic.term -> Cic.term -> coercion_search_result (* also adds them to the Db *) val close_coercion_graph: - UriManager.uri -> UriManager.uri -> UriManager.uri -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list