From ade2363e357db3ac3f258e645fe6bba988e7e7dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 19 Nov 2015 22:49:25 +0100 Subject: About building of substitutions from instances. Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. --- kernel/vars.mli | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'kernel/vars.mli') diff --git a/kernel/vars.mli b/kernel/vars.mli index ab10ba93b..a84cf0114 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -56,6 +56,24 @@ val lift : int -> constr -> constr type substl = constr list +(** Let [Γ] be a context interleaving declarations [x₁:T₁..xn:Tn] + and definitions [y₁:=c₁..yp:=cp] in some context [Γ₀]. Let + [u₁..un] be an {e instance} of [Γ], i.e. an instance in [Γ₀] + of the [xi]. Then, [subst_of_rel_context_instance Γ u₁..un] + returns the corresponding {e substitution} of [Γ], i.e. the + appropriate interleaving [σ] of the [u₁..un] with the [c₁..cp], + all of them in [Γ₀], so that a derivation [Γ₀, Γ, Γ₁|- t:T] + can be instantiated into a derivation [Γ₀, Γ₁ |- t[σ]:T[σ]] using + [substnl σ |Γ₁| t]. + Note that the instance [u₁..un] is represented starting with [u₁], + as if usable in [applist] while the substitution is + represented the other way round, i.e. ending with either [u₁] or + [c₁], as if usable for [substl]. *) +val subst_of_rel_context_instance : rel_context -> constr list -> substl + +(** For compatibility: returns the substitution reversed *) +val adjust_subst_to_rel_context : rel_context -> constr list -> 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 [an],...,[a1] and [c]. In terms of typing, if -- cgit v1.2.3