Module Unif.Ty

module Ty: S  with type term = Type.t and type ty = Type.t

type ty

type term

val bind : 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)
Raises Fail if occurs-check fires

val unification : ?subst:Unif_intf.subst ->
       term Scoped.t -> term Scoped.t -> Unif_intf.subst

Unify terms, returns a subst 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.
Raises

Fail if the terms do not match.
Invalid_argument if the two scopes are equal

subst : initial substitution (default empty)

val matching_same_scope : ?protect:ty HVar.t Sequence.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.

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

scope : the common scope of both terms

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

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

protect : used if scopes are the same, see Unif_intf.S.matching_same_scope

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

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

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

val are_variant : term -> term -> bool