Module `Unif.FO`

include S with type term = Term.t and type ty = Type.t

type ty = Type.t
type term = Term.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

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

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

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

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_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 anti_unify : ?⁠cut:int -> term -> term -> (term * term) list option

anti-unification of the two terms, returning disagreement pairs

parameter cut: if cut=n, then the returned list will have length at most n (if it's too long then None is returned)

val pair_lists : term -> term list -> term -> term list -> term list * term list