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.
| 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
;;
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
(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
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
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
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
-let pp _ = ();;
+let pp _ = ();;
let ppcontext = NCicPp.ppcontext;;
let ppmetasenv = NCicPp.ppmetasenv;;
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
| 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;;
(* 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
- *)
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
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
"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" [];
"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" [];
"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" [];
(**************************************************************************)
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;
∀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);
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; #_;
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;
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
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.
projects / helm.git / commitdiff
