module LogtkSubsts:`sig`

..`end`

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`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`

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?

`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 **important** that the bound term is De-Bruijn-closed (assert).

**Raises**

`v`

-> `t`

to the substitution. Both terms have a context.
It is `Invalid_argument`

if`v`

is already bound in the same context, to another term.`KindError`

if a term of a given kind is bound to a term of another kind (see`LogtkScopedTerm.Kind.t`

)

`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...

`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) ->

'a

`val iter : ``t ->`

(term ->

scope -> term -> scope -> unit) ->

unit

`val to_seq : ``t ->`

(term * scope * term * scope)

Sequence.t

`val to_list : ``t ->`

(term * scope * term * scope)

list

`val of_seq : ``?init:t ->`

(term * scope * term * scope)

Sequence.t -> t

`val of_list : ``?init:t ->`

(term * scope * term * scope)

list -> t

`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 **Caution**, can entail collisions between scopes!

`LogtkSubsts.apply`

, but performs no renaming of free variables.
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`