package logtk

  1. Overview
  2. Docs

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

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.

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
  • deprecated this function doesn't work anymore on HO terms
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?