Module Substs

module Substs: sig .. end

Substitutions

Substitutions map variables to terms/types. They work on free variables (within a scope, so that the same variable can live within several scopes).

The concept of scope is to allow the same free variable to be used in several contexts without being renamed. A scope is kind of a namespace, where variables from distinct namespaces are always distinct.


type term = InnerTerm.t 
type var = InnerTerm.t HVar.t 

Renamings

A renaming is used to disambiguate variables that come from distinct scopes but have the same index. It is used to merge together several scopes, in a sound way, by ensuring variables from those scopes are mapped to distinct variables of the new scope. For instance, a given renaming applied to (X,0) and (X,1) will return two different variables, as if one of the X had been renamed prior to unification/binding.
module Renaming: sig .. end

Basics


type t 
A substitution that binds term variables to other terms
type subst = t 
val empty : t
The identity substitution
val is_empty : t -> bool
Is the substitution empty?

Operations on Substitutions


val find_exn : t -> var Scoped.t -> term Scoped.t
Lookup variable in substitution.
Raises Not_found if variable not bound.
val find : t -> var Scoped.t -> term Scoped.t option
val deref : t -> term Scoped.t -> term Scoped.t
deref t s_t dereferences t as long as t is a variable bound in subst
val get_var : t -> var Scoped.t -> term Scoped.t option
Lookup recursively the var in the substitution, until it is not a variable anymore, or it is not bound.
Returns None if the variable is not bound, Some (deref (t, sc_t)) if v is bound to t, sc_t
val mem : t -> var Scoped.t -> bool
Check whether the variable is bound by the substitution
exception InconsistentBinding of var Scoped.t * term Scoped.t * term Scoped.t
val bind : t -> var Scoped.t -> term Scoped.t -> t
Add v -> t to the substitution. Both terms have a context. It is important that the bound term is De-Bruijn-closed (assert).
Raises InconsistentBinding if v is already bound in the same context, to another term.
val append : t -> t -> t
append s1 s2 is the substitution that maps t to s2 (s1 t).
val remove : t -> var Scoped.t -> t
Remove the given binding. No other variable should depend on it...

Set operations


val domain : t -> var Scoped.t Sequence.t
Domain of substitution
val codomain : t -> term Scoped.t Sequence.t
Codomain (image terms) of substitution
val introduced : t -> var Scoped.t Sequence.t
Variables introduced by the substitution (ie vars of codomain)
val is_renaming : t -> bool
Check whether the substitution is a variable renaming
include Interfaces.PRINT
val fold : ('a -> var Scoped.t -> term Scoped.t -> 'a) ->
'a -> t -> 'a
val iter : (var Scoped.t -> term Scoped.t -> unit) -> t -> unit
val to_seq : t -> (var Scoped.t * term Scoped.t) Sequence.t
val to_list : t -> (var Scoped.t * term Scoped.t) list
val of_seq : ?init:t ->
(var Scoped.t * term Scoped.t) Sequence.t -> t
val of_list : ?init:t ->
(var Scoped.t * term Scoped.t) list -> t

Applying a substitution


val apply : t -> renaming:Renaming.t -> term Scoped.t -> term
Apply the substitution to the given term. This function assumes that all terms in the substitution are closed, and it will not perform De Bruijn indices shifting. For instance, applying {X -> f(db0)} (with db0 the De Bruijn index 0) to the term forall. p(X) will yield forall. p(f(db0)) (capturing) and not forall. p(f(db1)).
renaming : used to desambiguate free variables from distinct scopes
val apply_no_renaming : t -> term Scoped.t -> term
Same as Substs.apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!

Specializations


module type SPECIALIZED = sig .. end
module Ty: SPECIALIZED  with type term = Type.t
module FO: SPECIALIZED  with type term = FOTerm.t