module Substs: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.
typeterm =
InnerTerm.t
typevar =
InnerTerm.t HVar.t
module Renaming:sig
..end
type
t
typesubst =
t
val empty : t
val is_empty : t -> bool
val find_exn : t -> var Scoped.t -> term Scoped.t
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
Some (deref (t, sc_t))
if v
is bound to t, sc_t
val mem : t -> var Scoped.t -> bool
exception InconsistentBinding of var Scoped.t * term Scoped.t * term Scoped.t
val bind : t -> var Scoped.t -> term Scoped.t -> t
v
-> t
to the substitution. Both terms have a context.
It is important that the bound term is De-Bruijn-closed (assert).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
val domain : t -> var Scoped.t Sequence.t
val codomain : t -> term Scoped.t Sequence.t
val introduced : t -> var Scoped.t Sequence.t
val is_renaming : t -> bool
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
val apply : t -> renaming:Renaming.t -> term Scoped.t -> term
{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 scopesval apply_no_renaming : t -> term Scoped.t -> term
Substs.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 = Type.t
module FO:SPECIALIZED
with type term = FOTerm.t