Module type LogtkUnif.UNARY

module type UNARY = sig .. end

type term 
val unification : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
term ->
LogtkUnif.scope -> term -> LogtkUnif.scope -> LogtkUnif.subst
LogtkUnify terms, returns a subst or
Raises Fail if the terms are not unifiable
env1 : environment for the first term
env2 : environment for the second term
val matching : ?allow_open:bool ->
?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
pattern:term ->
LogtkUnif.scope -> term -> LogtkUnif.scope -> LogtkUnif.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
allow_open : if true, variables can bind to non-closed DB terms (default false)
subst : initial substitution (default empty)
val matching_same_scope : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?protect:term Sequence.t ->
?subst:LogtkUnif.subst ->
scope:LogtkUnif.scope ->
pattern:term -> term -> LogtkUnif.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 : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?protect:term Sequence.t ->
?subst:LogtkUnif.subst ->
pattern:term ->
LogtkUnif.scope -> term -> LogtkUnif.scope -> LogtkUnif.subst
Call either LogtkUnif.UNARY.matching or LogtkUnif.UNARY.matching_same_scope depending on whether the given scopes are the same or not.
protect : used if scopes are the same, see LogtkUnif.UNARY.matching_same_scope
val variant : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
?subst:LogtkUnif.subst ->
term ->
LogtkUnif.scope -> term -> LogtkUnif.scope -> LogtkUnif.subst
Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent
val eq : ?env1:LogtkUnif.env ->
?env2:LogtkUnif.env ->
subst:LogtkUnif.subst ->
term ->
LogtkUnif.scope -> term -> LogtkUnif.scope -> bool
eq 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