From: Enrico Tassi Date: Tue, 15 Sep 2009 13:53:04 +0000 (+0000) Subject: improved check in delift for flexible lc entries. X-Git-Tag: make_still_working~3464 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8049c166a37789d7a1b1ca1c3a1174712bbf87ba;p=helm.git improved check in delift for flexible lc entries. added a function to easily delift a term w.r.t. other terms, thanks to delift, used to propagate the expected type of a letin. --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 927c288a0..60abe85c3 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -206,12 +206,29 @@ and restrict metasenv subst i restrictions = | NCicUtils.Meta_not_found _ -> assert false ;; -let rec flexible_arg subst = function +let rec flexible_arg context subst = function | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> (try let _,_,t,_ = List.assoc i subst in - flexible_arg subst t + flexible_arg context subst t with Not_found -> true) + (* this is a cheap whd, it only performs zeta-reduction. + * + * it works when the **omissis** disambiguation algorithm + * is run on `let x := K a b in t`, K is substituted for a + * ? and thus in t metavariables have a flexible Rel + *) + | NCic.Rel i -> + (try + match List.nth context (i-1) + with + | _,NCic.Def (bo,_) -> + flexible_arg context subst + (NCicSubstitution.lift i bo) + | _ -> false + with + | Failure _ -> assert false + | Invalid_argument _ -> assert false) | _ -> false ;; @@ -258,8 +275,8 @@ let delift ~unify metasenv subst context n l t = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> - if flexible_arg subst t || contains_in_scope subst t then None else - let lb = List.map (fun t -> t, flexible_arg subst t) l in + if flexible_arg context subst t || contains_in_scope subst t then None else + let lb = List.map (fun t -> t, flexible_arg context subst t) l in HExtlib.list_findopt (fun (li,flexible) i -> if flexible || i < in_scope then None else diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7c199f8c0..56ec069d2 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -114,10 +114,14 @@ let rec typeof rdb (NCicPp.ppterm ~metasenv ~subst:[] ~context expty))); try let metasenv, subst = + (*D*)inside 'U'; try let rc = NCicUnification.unify rdb metasenv subst context infty expty + (*D*)in outside(); rc with exc -> outside (); raise exc in metasenv, subst, t, expty - with exc -> + with + | NCicUnification.Uncertain _ + | NCicUnification.UnificationFailure _ as exc -> try_coercions rdb ~localise metasenv subst context t orig infty expty true exc) | None -> metasenv, subst, t, infty @@ -229,8 +233,18 @@ let rec typeof rdb let metasenv, subst, t, _ = typeof_aux metasenv subst context (Some ty) t in let context1 = (n, C.Def (t,ty)) :: context in + let metasenv, subst, expty1 = + match expty with + | None -> metasenv, subst, None + | Some x -> + let m, s, x = + NCicUnification.delift_term_wrt_terms + rdb metasenv subst context x [t] + in + m, s, Some x + in let metasenv, subst, bo, bo_ty = - typeof_aux metasenv subst context1 None bo + typeof_aux metasenv subst context1 expty1 bo in let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty @@ -509,11 +523,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he let metasenv,subst, flex_prod, _ = typeof rdb ~localise metasenv subst context flex_prod None in +(* pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context ^ "\nOF: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); +*) let metasenv, subst = try NCicUnification.unify rdb metasenv subst context t flex_prod with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index c22470853..2f6332d51 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -95,8 +95,8 @@ let outside () = let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -let pp _ = ();; +let pp _ = ();; let ppcontext = NCicPp.ppcontext;; let ppmetasenv = NCicPp.ppmetasenv;; @@ -152,20 +152,11 @@ let rec lambda_intros rdb metasenv subst context t args = in metasenv, subst, bo | (arg,ty)::tail -> + let metasenv, subst, telescopic_ty = + delift_term_wrt_terms rdb metasenv subst context_of_args ty + (List.rev processed_args) + in let name = "HBeta"^string_of_int n in - let metasenv,_,instance,_ = - NCicMetaSubst.mk_meta metasenv context_of_args `Term in - let meta_applied = - NCicUntrusted.mk_appl instance (List.rev processed_args) in -let metasenv,subst,_,_ = - !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None -in - let metasenv,subst = - unify rdb true metasenv subst context_of_args meta_applied ty in - let telescopic_ty = NCicSubstitution.lift n instance in - let telescopic_ty = - NCicUntrusted.mk_appl - telescopic_ty (mk_irl (List.length processed_args)) in let metasenv, subst, bo = mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1) (arg::processed_args) tail @@ -669,8 +660,23 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn (*D*) in outside(); rc with exn -> outside (); raise exn + +and delift_term_wrt_terms rdb metasenv subst context t args = + let metasenv, _, instance, _ = + NCicMetaSubst.mk_meta metasenv context `Term in + let meta_applied = NCicUntrusted.mk_appl instance args in + let metasenv,subst,meta_applied,_ = + !refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) + metasenv subst context meta_applied None + in + let metasenv, subst = + unify rdb true metasenv subst context meta_applied t in + let t = NCicSubstitution.lift (List.length args) instance in + let t = NCicUntrusted.mk_appl t (mk_irl (List.length args)) in + metasenv, subst, t ;; + let unify rdb ?(test_eq_only=false) = indent := ""; unify rdb test_eq_only;; diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 891c0738e..944b4c187 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -32,38 +32,9 @@ val unify : (* this should be moved elsewhere *) val fix_sorts: NCic.term -> NCic.term -(* -exception UnificationFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -(* fo_unif metasenv context t1 t2 *) -(* unifies [t1] and [t2] in a context [context]. *) -(* Only the metavariables declared in [metasenv] *) -(* can be used in [t1] and [t2]. *) -(* The returned substitution can be directly *) -(* withouth first unwinding it. *) -val fo_unif : - Cic.metasenv -> Cic.context -> - Cic.term -> Cic.term -> CicUniv.universe_graph -> - Cic.substitution * Cic.metasenv * CicUniv.universe_graph - -(* fo_unif_subst metasenv subst context t1 t2 *) -(* unifies [t1] and [t2] in a context [context] *) -(* and with [subst] as the current substitution *) -(* (i.e. unifies ([subst] [t1]) and *) -(* ([subst] [t2]) in a context *) -(* ([subst] [context]) using the metasenv *) -(* ([subst] [metasenv]) *) -(* Only the metavariables declared in [metasenv] *) -(* can be used in [t1] and [t2]. *) -(* [subst] and the substitution returned are not *) -(* unwinded. *) -(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la - cosa all'apply_subst!!!*) -val fo_unif_subst : - Cic.substitution -> Cic.context -> Cic.metasenv -> - Cic.term -> Cic.term -> CicUniv.universe_graph -> - Cic.substitution * Cic.metasenv * CicUniv.universe_graph +val delift_term_wrt_terms: + #NRstatus.status -> + NCic.metasenv -> NCic.substitution -> NCic.context -> + NCic.term -> NCic.term list -> + NCic.metasenv * NCic.substitution * NCic.term - *) diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 105946ce0..c5d90654b 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,11 +1,10 @@ logic/cprop.ma hints_declaration.ma sets/setoids1.ma -sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma -topology/igft.ma logic/connectives.ma +sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma +topology/igft.ma sets/sets.ma datatypes/bool.ma logic/pts.ma sets/setoids1.ma properties/relations1.ma sets/setoids.ma logic/equality.ma logic/connectives.ma properties/relations.ma sets/setoids.ma logic/connectives.ma properties/relations.ma -.unnamed.ma logic/pts.ma logic/connectives.ma logic/pts.ma datatypes/pairs.ma logic/pts.ma algebra/abelian_magmas.ma algebra/magmas.ma @@ -14,7 +13,7 @@ nat/minus.ma nat/order.ma algebra/magmas.ma sets/sets.ma properties/relations1.ma logic/pts.ma nat/big_ops.ma algebra/magmas.ma nat/order.ma -nat/nat.ma logic/equality.ma sets/setoids.ma +nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma properties/relations.ma logic/pts.ma nat/compare.ma datatypes/bool.ma nat/order.ma hints_declaration.ma logic/pts.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index 521bb637d..b987610af 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -3,12 +3,13 @@ digraph g { "logic/cprop.ma" -> "hints_declaration.ma" []; "logic/cprop.ma" -> "sets/setoids1.ma" []; "sets/sets.ma" []; + "sets/sets.ma" -> "hints_declaration.ma" []; "sets/sets.ma" -> "logic/connectives.ma" []; "sets/sets.ma" -> "logic/cprop.ma" []; "sets/sets.ma" -> "properties/relations1.ma" []; "sets/sets.ma" -> "sets/setoids1.ma" []; "topology/igft.ma" []; - "topology/igft.ma" -> "logic/connectives.ma" []; + "topology/igft.ma" -> "sets/sets.ma" []; "datatypes/bool.ma" []; "datatypes/bool.ma" -> "logic/pts.ma" []; "sets/setoids1.ma" []; @@ -20,8 +21,6 @@ digraph g { "sets/setoids.ma" []; "sets/setoids.ma" -> "logic/connectives.ma" []; "sets/setoids.ma" -> "properties/relations.ma" []; - ".unnamed.ma" []; - ".unnamed.ma" -> "logic/pts.ma" []; "logic/connectives.ma" []; "logic/connectives.ma" -> "logic/pts.ma" []; "datatypes/pairs.ma" []; @@ -42,6 +41,7 @@ digraph g { "nat/big_ops.ma" -> "algebra/magmas.ma" []; "nat/big_ops.ma" -> "nat/order.ma" []; "nat/nat.ma" []; + "nat/nat.ma" -> "hints_declaration.ma" []; "nat/nat.ma" -> "logic/equality.ma" []; "nat/nat.ma" -> "sets/setoids.ma" []; "properties/relations.ma" []; diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index 04d00a692..e3fb6c252 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index e33ddfa1d..40ecd43b4 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -13,15 +13,19 @@ (**************************************************************************) include "sets/sets.ma". -include "nat/plus.ma". (* tempi biblici neggli include che fa plus.ma *) +include "nat/plus.ma". include "nat/compare.ma". include "nat/minus.ma". include "datatypes/pairs.ma". - +alias symbol "eq" (instance 2) = "leibnitz's equality". +alias symbol "eq" (instance 1) = "setoid eq". +alias symbol "eq" = "setoid eq". +alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". +alias symbol "eq" = "setoid1 eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -129,9 +133,10 @@ nlemma partition_splits_card: ∀A. ∀P:partition A. ∀n,s. ∀f:isomorphism ?? (Nat_ n) (indexes ? P). (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) → - (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) A). - #A; #P; #Sn; ncases Sn - [ #s; #f; #fi; nlapply (covers ? P); *; #_; #H; + (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)). +#A; #P; #Sn; ncases Sn + [ #s; #f; #fi; + ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H; (* nlapply (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f); @@ -139,7 +144,7 @@ nlemma partition_splits_card: nelim daemon (* impossibile *) | #n; #s; #f; #fi; @ [ @ - [ napply (λm.let p ≝ iso_nat_nat_union s m n in iso_f ???? (fi (fst … p)) (snd … p)) + [ napply (λm.let p ≝ (iso_nat_nat_union s m n) in iso_f ???? (fi (fst … p)) (snd … p)) | #a; #a'; #H; nrewrite < H; napply refl ] ##| #x; #Hx; nwhd; napply I ##| #y; #_; @@ -147,12 +152,12 @@ nlemma partition_splits_card: ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2; ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2; ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ? - [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##] + [##2: napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] *; #nindex2; *; #Hni21; #Hni22; nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2); napply (ex_intro … xxx); napply conj [ napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption ] - ##| nwhd in ⊢ (???%%); napply (.= ?) [ nassumption|##skip] + ##| nwhd in ⊢ (???%%); napply (.= ?) [##3: nassumption|##skip] ngeneralize in match (iso_nat_nat_union_char n s xxx ?) in ⊢ ? [##2: napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##] *; *; #K1; #K2; #K3; @@ -168,7 +173,7 @@ nlemma partition_splits_card: ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ? [##2,3: napply f_closed; nassumption |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj - [ napply f_closed; nassumption ##| napply (. ?‡#) [##2: nassumption | ##3: ##skip] + [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip] nwhd; napply f_closed; nassumption]##] #E'; ngeneralize in match (? : i1=i1') in ⊢ ? [##2: napply (f_inj … E'); nassumption @@ -204,4 +209,4 @@ ndefinition partition_of_compatible_equivalence_relation: napply sym; nassumption | nnormalize; napply conj [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##] -nqed. \ No newline at end of file +nqed.