logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Unif . Ty
include S with type term = Type.t and type ty = Type.t
type ty = Type.t
type term = Type.t
val bind : ?check:bool -> Unif_intf.subst -> ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.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 -> Unif_intf.subst -> ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.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:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> Unif_intf.subst

Unify terms syntictally, returns a subst

  • raises Fail

    if the terms are not unifiable

Unify terms, returns a subst + constraints or

  • raises Fail

    if the terms are not unifiable

val matching : ?subst:Unif_intf.subst -> pattern:term Scoped.t -> term Scoped.t -> Unif_intf.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:Unif_intf.subst -> scope:int -> pattern:term -> term -> Unif_intf.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:Unif_intf.subst -> pattern:term Scoped.t -> term Scoped.t -> Unif_intf.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

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

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

equal subst t1 s1 t2 s2 returns true iff the two terms are equal under the given substitution, i.e. if applying the substitution will return the same term.

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
val type_is_unifiable : term -> bool

Can we (syntactically) unify terms of this type?