Library
Module
Module type
Parameter
Class
Class type
val log_cp : 'a Lplib.Base.outfmt -> 'a
val rule_of_pair : (Core.Term.term * Core.Term.term) Lplib.Base.pp
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.
val rule_of_def : Core.Term.sym -> Core.Term.term -> Core.Term.rule
rule_of_def s d
creates the rule s --> d
.
val replace :
Core.Term.term ->
Core.Term.subterm_pos ->
Core.Term.term ->
Core.Term.term
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
.
val shift : Core.Term.term -> Core.Term.term
shift t
replaces in t
every pattern index i by -i-1.
type subs = Core.Term.term Lplib.Extra.IntMap.t
Type for pattern variable substitutions.
val subs : Core.Term.term Lplib.Extra.IntMap.t Lplib.Base.pp
val apply_subs : subs -> Core.Term.term -> Core.Term.term
apply_subs s t
applies the pattern substitution s
to t
.
type iter =
Common.Pos.popt ->
( Core.Term.sym -> Core.Term.subterm_pos -> Core.Term.term -> unit ) ->
Core.Term.term ->
unit
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.
val unif :
Common.Pos.popt ->
Core.Term.term ->
Core.Term.term ->
Core.Term.term Lplib.Extra.IntMap.t option
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 cp_fun =
Common.Pos.popt ->
rule_id ->
Core.Term.term ->
Core.Term.term ->
Core.Term.subterm_pos ->
Core.Term.term ->
rule_id ->
Core.Term.term ->
Core.Term.term ->
subs ->
unit
Type of functions on critical pairs.
type cp_cand_fun =
Common.Pos.popt ->
rule_id ->
Core.Term.term ->
Core.Term.term ->
Core.Term.subterm_pos ->
Core.Term.term ->
rule_id ->
Core.Term.term ->
Core.Term.term ->
unit
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'
.
val check_cps :
Common.Pos.popt ->
Core.Sign.t ->
Core.Term.sym_rule list ->
Core.Term.rule list Core.Term.SymMap.t ->
unit
check_cps rs
checks all the critical pairs generated by adding rs
.
val update_cp_pos :
Common.Pos.popt ->
Core.Term.cp_pos list Core.Term.SymMap.t ->
Core.Term.rule list Core.Term.SymMap.t ->
Core.Term.cp_pos list Core.Term.SymMap.t
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).