diff options
| -rw-r--r-- | kernel/vars.ml | 21 | ||||
| -rw-r--r-- | kernel/vars.mli | 70 |
2 files changed, 60 insertions, 31 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index a800e2531..f8c0a65e6 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -151,6 +151,11 @@ let make_subst = function done; subst +(* The type of substitutions, with term substituting most recent + binder at the head *) + +type substl = Constr.t list + let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c @@ -159,13 +164,6 @@ let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r -let substnl_named_decl laml k d = - map_named_declaration (fun c -> substnl laml k c) d -let substl_named_decl laml d = - map_named_declaration (fun c -> substnl laml 0 c) d -let subst1_named_decl lam d = - map_named_declaration (fun c -> subst1 lam c) d - (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function @@ -197,15 +195,10 @@ let replace_vars var_alist x = in substrec 0 x -(* -let repvarkey = Profile.declare_profile "replace_vars";; -let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; -*) - -(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) +(* (subst_var str t) substitute (Var str) by (Rel 1) in t *) let subst_var str t = replace_vars [(str, Constr.mkRel 1)] t -(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) +(* (subst_vars [id1;...;idn] t) substitute (Var idj) by (Rel j) in t *) let substn_vars p vars c = let _,subst = List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars diff --git a/kernel/vars.mli b/kernel/vars.mli index c0fbeeb6e..ab10ba93b 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -42,33 +42,69 @@ val liftn : int -> int -> constr -> constr (** [lift n c] lifts by [n] the positive indexes in [c] *) val lift : int -> constr -> constr -(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] +(** The type [substl] is the type of substitutions [u₁..un] of type + some context Δ and defined in some environment Γ. Typing of + substitutions is defined by: + - Γ ⊢ ∅ : ∅, + - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ u{_n} : An\[u₁..u{_n-1}\] implies + Γ ⊢ u₁..u{_n} : Δ,x{_n}:A{_n} + - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ un : A{_n}\[u₁..u{_n-1}\] implies + Γ ⊢ u₁..u{_n} : Δ,x{_n}:=c{_n}:A{_n} when Γ ⊢ u{_n} ≡ c{_n}\[u₁..u{_n-1}\] + + Note that [u₁..un] is represented as a list with [un] at the head of + the list, i.e. as [[un;...;u₁]]. *) + +type substl = constr list + +(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates - accordingly indexes in [a1],...,[an] and [c] *) -val substnl : constr list -> int -> constr -> constr -val substl : constr list -> constr -> constr + accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if + Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then + Γ, Γ' ⊢ [substnl [a₁;...;an] k c] : [substnl [a₁;...;an] k T]. *) +val substnl : substl -> int -> constr -> constr + +(** [substl σ c] is a short-hand for [substnl σ 0 c] *) +val substl : substl -> constr -> constr + +(** [substl a c] is a short-hand for [substnl [a] 0 c] *) val subst1 : constr -> constr -> constr -val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration -val substl_decl : constr list -> rel_declaration -> rel_declaration -val subst1_decl : constr -> rel_declaration -> rel_declaration +(** [substnl_decl [a₁;...;an] k Ω] substitutes in parallel [a₁], ..., [an] + for respectively [Rel(k+1)], ..., [Rel(k+n)] in [Ω]; it relocates + accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if + Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then + Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *) +val substnl_decl : substl -> int -> rel_declaration -> rel_declaration + +(** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *) +val substl_decl : substl -> rel_declaration -> rel_declaration -val substnl_named_decl : constr list -> int -> named_declaration -> named_declaration -val subst1_named_decl : constr -> named_declaration -> named_declaration -val substl_named_decl : constr list -> named_declaration -> named_declaration +(** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *) +val subst1_decl : constr -> rel_declaration -> rel_declaration +(** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by + [cj] in [t]. *) val replace_vars : (Id.t * constr) list -> constr -> constr -(** (subst_var str t) substitute (VAR str) by (Rel 1) in t *) -val subst_var : Id.t -> constr -> constr -(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t] - if two names are identical, the one of least indice is kept *) -val subst_vars : Id.t list -> constr -> constr +(** [substn_vars k [id₁;...;idn] t] substitutes [Var idj] by [Rel j+k-1] in [t]. + If two names are identical, the one of least index is kept. In terms of + typing, if Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ t:T, together with id{_j}:T{_j} and + Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ T{_j}\[id{_j+1}..id{_n}:=x{_j+1}..x{_n}\] ≡ Uj, + then Γ\\{id₁,...,id{_n}\},x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ [substn_vars + (|Γ'|+1) [id₁;...;idn] t] : [substn_vars (|Γ'|+1) [id₁;...;idn] + T]. *) -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] - if two names are identical, the one of least indice is kept *) val substn_vars : int -> Id.t list -> constr -> constr +(** [subst_vars [id1;...;idn] t] is a short-hand for [substn_vars + [id1;...;idn] 1 t]: it substitutes [Var idj] by [Rel j] in [t]. If + two names are identical, the one of least index is kept. *) +val subst_vars : Id.t list -> constr -> constr + +(** [subst_var id t] is a short-hand for [substn_vars [id] 1 t]: it + substitutes [Var id] by [Rel 1] in [t]. *) +val subst_var : Id.t -> constr -> constr + (** {3 Substitution of universes} *) open Univ |