Module `Logtk__Subst`

Substitutions

type term = Logtk.InnerTerm.t
type var = Logtk.InnerTerm.t Logtk.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 Logtk.Scoped.t -> term Logtk.Scoped.t

Lookup variable in substitution.

raises Not_found: if variable not bound.

val find : t -> var Logtk.Scoped.t -> term Logtk.Scoped.t option
val deref : t -> term Logtk.Scoped.t -> term Logtk.Scoped.t: deref t s_t dereferences t as long as t is a variable bound in subst

val get_var : t -> var Logtk.Scoped.t -> term Logtk.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 Logtk.Scoped.t -> bool: Check whether the variable is bound by the substitution

exception InconsistentBinding of var Logtk.Scoped.t * term Logtk.Scoped.t * term Logtk.Scoped.t

val bind : t -> var Logtk.Scoped.t -> term Logtk.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 update : t -> var Logtk.Scoped.t -> term Logtk.Scoped.t -> t

Replace v -> ? by v -> t in the substitution. Both terms have a context. It is important that the bound term is De-Bruijn-closed (assert).

raises InconsistentBinding: if v is not yet bound in the same context.

val merge : t -> t -> t

merge s1 s2 is the substitution that maps t to (s1 t) or to (s2 t).

raises InconsistentBinding: if the substitutions disagree.

val remove : t -> var Logtk.Scoped.t -> t: Remove the given binding. No other variable should depend on it...

val filter_scope : t -> Logtk.Scoped.scope -> t: Only keep bindings from this scope

Set operations

val domain : t -> var Logtk.Scoped.t Iter.t: Domain of substitution

val codomain : t -> term Logtk.Scoped.t Iter.t: Codomain (image terms) of substitution

val introduced : t -> var Logtk.Scoped.t Iter.t: Variables introduced by the substitution (ie vars of codomain)

val normalize : t -> t: Normalize bindings that are in the same scope. E.g. x0 -> f(y0), y0 -> g(z0), z0->a becomes x0->f(g(a))0, y0->g(a)0, z0->g(z0)

val map : (term -> term) -> t -> t: Map on term

val filter : (var Logtk.Scoped.t -> term Logtk.Scoped.t -> bool) -> t -> t: Filter bindings

val is_renaming : t -> bool: Check whether the substitution is a variable renaming

val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int

include Logtk.Interfaces.PRINT with type t := t

type t

val pp : t CCFormat.printer
val to_string : t -> string

val pp_bindings : t CCFormat.printer: Only print the bindings, no box

val fold : ('a -> var Logtk.Scoped.t -> term Logtk.Scoped.t -> 'a) -> 'a -> t -> 'a
val iter : (var Logtk.Scoped.t -> term Logtk.Scoped.t -> unit) -> t -> unit
val to_iter : t -> (var Logtk.Scoped.t * term Logtk.Scoped.t) Iter.t
val to_list : t -> (var Logtk.Scoped.t * term Logtk.Scoped.t) list
val of_iter : ?⁠init:t -> (var Logtk.Scoped.t * term Logtk.Scoped.t) Iter.t -> t
val of_list : ?⁠init:t -> (var Logtk.Scoped.t * term Logtk.Scoped.t) list -> t

Applying a substitution

val apply : ?⁠shift_vars:int -> Renaming.t -> t -> term Logtk.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)).

parameter renaming: used to desambiguate free variables from distinct scopes

Specializations

module type SPECIALIZED = sig ... end

module Ty : SPECIALIZED with type term = Logtk.Type.t

module FO : sig ... end

Projections for proofs

module Projection : sig ... end