lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.tool
Module Tool . Lcr
val log_cp : 'a Lplib.Base.outfmt -> 'a

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

val is_ho : Core.Term.rule -> bool

is_ho r says if r uses higher-order variables.

val is_definable : Core.Term.sym -> bool

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.

val occurs : int -> Core.Term.term -> bool

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.

val apply_subs : subs -> Core.Term.term -> Core.Term.term

apply_subs s t applies the pattern substitution s to t.

Type of subterm iterators.

val iter_subterms_from_pos : Core.Term.subterm_pos -> iter

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.

val iter_subterms_eq : iter

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

val iter_subterms : iter

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.

val can_handle : Core.Term.sym_rule -> bool

can_handle r says if the sym_rule r can be handled.

val iter_rules : ( Core.Term.rule -> unit ) -> Core.Term.sym -> Core.Term.rule list -> unit

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

val iter_sym_rules : ( Core.Term.sym_rule -> unit ) -> Core.Term.sym_rule list -> unit

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

val iter_rules_of_sym : ( Core.Term.rule -> unit ) -> Core.Term.sym -> unit

iter_rules_of_sym h s iterates f on every rule of s.

type rule_id = Common.Pos.pos

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.

val id_sym_rule : Core.Term.sym_rule -> rule_id

id_sym_rule r returns the rule id of r.

val new_rule_id : unit -> rule_id

new_rule_id() generates a new unique rule id.

val is_generated : rule_id -> bool

is_generated i says if i is a generated rule id.

val int_of_rule_id : rule_id -> int

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.

val cp_cand_fun : cp_fun -> cp_cand_fun

cp_cand_fun turns a cp_fun into a cp_cand_fun.

val iter_cps_with_rule : iter -> cp_fun -> Common.Pos.popt -> Core.Term.sym_rule -> Core.Term.sym_rule -> unit

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.

val iter_cps_of_rules : cp_fun -> Common.Pos.popt -> Core.Term.sym_rule list -> unit

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

val typability_constraints : Common.Pos.popt -> Core.Term.term -> subs option

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.

val check_cp : cp_fun

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.

val check_cps_subterms_eq : Common.Pos.popt -> Core.Term.sym_rule -> unit

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.

val check_cps_sign_with : Common.Pos.popt -> Core.Sign.t -> Core.Term.rule list Core.Term.SymMap.t -> unit

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