include S with type term = Term.t and type ty = Type.ttype ty = Type.ttype term = Term.tval bind :
?check:bool ->
Unif_intf.subst ->
ty HVar.t Scoped.t ->
term Scoped.t ->
Unif_intf.substbind subst v t binds v to t, but fails if v occurs in t (performs an occur-check first)
if true, perform occur check
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.substbind subst v t replaces the binding of v to t, but fails if v occurs in t (performs an occur-check first)
if true, perform occur check
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.substUnify terms syntictally, returns a subst
Fail if the terms are not unifiable
val unify_full :
?subst:Unif_intf.unif_subst ->
term Scoped.t ->
term Scoped.t ->
Unif_intf.unif_substUnify terms, returns a subst + constraints or
Fail if the terms are not unifiable
val matching :
?subst:Unif_intf.subst ->
pattern:term Scoped.t ->
term Scoped.t ->
Unif_intf.substmatching ~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.
initial substitution (default empty)
Fail if the terms do not match.
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.substmatches 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.
the common scope of both terms
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.substCall either matching or matching_same_scope depending on whether the given scopes are the same or not.
used if scopes are the same, see matching_same_scope
val variant :
?subst:Unif_intf.subst ->
term Scoped.t ->
term Scoped.t ->
Unif_intf.substSucceeds 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 -> boolequal 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.
anti-unification of the two terms, returning disagreement pairs
if cut=n, then the returned list will have length at most n (if it's too long then None is returned)