logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module type Logtk . Unif_intf . S
type ty
type term
val bind : ?check:bool -> subst -> ty HVar.t Scoped.t -> term Scoped.t -> subst

bind subst v t binds v to t, but fails if v occurs in t (performs an occur-check first)

  • parameter check

    if true, perform occur check

  • raises Fail

    if occurs-check fires or if the variable is bound already

val update : ?check:bool -> subst -> ty HVar.t Scoped.t -> term Scoped.t -> subst

bind subst v t replaces the binding of v to t, but fails if v occurs in t (performs an occur-check first)

  • parameter check

    if true, perform occur check

  • raises Fail

    if occurs-check fires or if the variable is not yet bound

val unify_syn : ?subst:subst -> term Scoped.t -> term Scoped.t -> subst

Unify terms syntictally, returns a subst

  • raises Fail

    if the terms are not unifiable

val unify_full : ?subst:unif_subst -> term Scoped.t -> term Scoped.t -> unif_subst

Unify terms, returns a subst + constraints or

  • raises Fail

    if the terms are not unifiable

val matching : ?subst:subst -> pattern:term Scoped.t -> term Scoped.t -> subst

matching ~pattern scope_p b scope_b returns sigma such that sigma pattern = b, or fails. Only variables from the scope of pattern can be bound in the subst.

  • parameter subst

    initial substitution (default empty)

  • raises Fail

    if the terms do not match.

  • raises Invalid_argument

    if the two scopes are equal

val matching_same_scope : ?protect:ty HVar.t Iter.t -> ?subst:subst -> scope:int -> pattern:term -> term -> subst

matches pattern (more general) with the other term. The two terms live in the same scope, which is passed as the scope argument. It needs to gather the variables of the other term to make sure they are not bound.

  • parameter scope

    the common scope of both terms

  • parameter protect

    a sequence of variables to protect (they cannot be bound during matching!). Variables of the second term are automatically protected.

val matching_adapt_scope : ?protect:ty HVar.t Iter.t -> ?subst:subst -> pattern:term Scoped.t -> term Scoped.t -> subst

Call either matching or matching_same_scope depending on whether the given scopes are the same or not.

  • parameter protect

    used if scopes are the same, see matching_same_scope

val variant : ?subst:subst -> term Scoped.t -> term Scoped.t -> subst

Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent

val equal : subst:subst -> term Scoped.t -> term Scoped.t -> bool
val are_unifiable_full : term -> term -> bool

Unifiable with some additional constraints?

val are_unifiable_syn : term -> term -> bool

Unifiable syntactically?

val matches : pattern:term -> term -> bool
val are_variant : term -> term -> bool