Module Logtk.Substs (.ml)

module Substs: LogtkSubsts

type scope = int 
A scope is an integer. Variables can only be bound in one scope, and variables from distinct scopes are distinct too.
type 'a scoped = 'a * scope 
type term = LogtkScopedTerm.t 


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


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 lookup : t ->
term -> scope -> term * scope
Lookup variable in substitution.
Raises Not_found if variable not bound.
val get_var : t ->
term -> scope -> term * scope
Lookup recursively the var in the substitution, until it is not a variable anymore, or it is not bound
val mem : t -> term -> scope -> bool
Check whether the variable is bound by the substitution
exception KindError
val bind : t ->
term ->
scope -> term -> scope -> t
Add v -> t to the substitution. Both terms have a context. It is important that the bound term is De-Bruijn-closed (assert).
val append : t -> t -> t
append s1 s2 is the substitution that maps t to s2 (s1 t).
val remove : t -> term -> int -> t
Remove the given binding. No other variable should depend on it...

Set operations

val domain : t -> (term * scope) Sequence.t
Domain of substitution
val codomain : t -> (term * scope) Sequence.t
Codomain (image terms) of substitution
val introduced : t -> (term * scope) 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 LogtkInterfaces.PRINT
val fold : t ->
'a ->
('a ->
term ->
scope -> term -> scope -> 'a) ->
val iter : t ->
(term ->
scope -> term -> scope -> unit) ->
val to_seq : t ->
(term * scope * term * scope)
val to_list : t ->
(term * scope * term * scope)
val of_seq : ?init:t ->
(term * scope * term * scope)
Sequence.t -> t
val of_list : ?init:t ->
(term * scope * term * scope)
list -> t

Applying a substitution

val apply : t ->
renaming:Renaming.t ->
term -> scope -> 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 -> scope -> term
Same as LogtkSubsts.apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!


module type SPECIALIZED = sig .. end
module Ty: SPECIALIZED  with type term = LogtkType.t
module FO: SPECIALIZED  with type term = LogtkFOTerm.t
module HO: SPECIALIZED  with type term = LogtkHOTerm.t
module Form: SPECIALIZED  with type term = LogtkFormula.FO.t