rule_of_pair ppf x prints on ppf the pair of term x as a rule.

is_ho r says if r uses higher-order variables.

is_definable s says if s is definable and non opaque but not AC.

rule_of_def s d creates the rule s --> d.

replace t p u replaces the subterm of t at position p by u.

occurs i t returns true iff Patt(i,_,_) is a subterm of t.

shift t replaces in t every pattern index i by -i-1.

Type for pattern variable substitutions.

apply_subs s t applies the pattern substitution s to t.

Type of subterm iterators.

iter_subterms_eq pos f p t iterates f on all subterms of t headed by a defined function symbol. p is the position of t in reverse order.

iter_subterms_eq pos f t iterates f on all subterms of t headed by a defined function symbol.

iter_subterms pos f t iterates f on all strict subterms of t headed by a defined function symbol.

unif pos t u returns None if t and u are not unifiable, and Some s with s an idempotent mgu otherwise. Precondition: l and r must have distinct indexes in Patt subterms.

can_handle r says if the sym_rule r can be handled.

iter_rules h rs iterates function f on every rule of rs.

iter_sym_rules h rs iterates function f on every rule of rs.

iter_rules_of_sym h s iterates f on every rule of s.

Type of rule identifiers. Hack: we use the rule position to distinguish between user-defined and generated rules (in completion), by giving a unique negative start_line to every generated rule.

id_sym_rule r returns the rule id of r.

new_rule_id() generates a new unique rule id.

is_generated i says if i is a generated rule id.

int_of_rule_id i returns a unique integer from i. /!\ i must be a generated rule.

Type of functions on critical pairs.

Type of functions on critical pair candidates.

cp_cand_fun turns a cp_fun into a cp_cand_fun.

iter_cps_with_rule iter_subterms h pos sr1 sr2 applies h on all the critical pairs between all the subterms of the sr1 LHS and the sr2 LHS using the iterator iter_subterms.

iter_cps_of_rules h pos rs applies h on all the critical pairs of rs with itself.

typability_constraints pos t returns None if t is not typable, and Some s where s is a substitution implied by the typability of t.

check_cp pos _ l r p l_p _ g d s checks that, if l_p and g are unifiable with mgu s, then s(r) and s(l[d]_p) are joinable. Precondition: l and r must have distinct indexes in Patt subterms.

check_cps_subterms_eq pos sr1 checks the critical pairs between all the subterms of the sr1 LHS and all the possible rule LHS's.

check_cps_sign_with pos rs' checks all the critical pairs between all the rules of the signature and rs'.

check_cps rs checks all the critical pairs generated by adding rs.

update_cp_pos pos map rs extends map by mapping every definable symbol s' such that there is a rule l-->r of rs and a position p of l such that l_p is headed by s' to (l,r,p,l_p).