Skip to content

do not test critical pairs with rules containing higher-order pattern variables #1406

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fblanqui merged 2 commits into from
Jun 10, 2026
Merged

do not test critical pairs with rules containing higher-order pattern variables #1406

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
91c22e0
critical pair computations: do not test new rules with higher-order p…
fblanqui Jun 10, 2026
8da3c4a
Merge remote-tracking branch 'dk/master' into lcr
fblanqui Jun 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 10 additions & 4 deletions src/tool/lcr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -392,12 +392,12 @@ let iter_cps_of_rules : cp_fun -> Pos.popt -> sym_rule list -> unit =
(** [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]. *)
let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
if Logger.log_enabled() then log_cp "typability_constraints %a" term t;
(* Replace Patt's by Meta's. *)
let open Stdlib in
let p = new_problem()
and p2m : meta IntMap.t ref = ref IntMap.empty
and m2p : (int * string) MetaMap.t ref = ref MetaMap.empty in
if Logger.log_enabled() then log_cp "typability_constraints %a" term t;
let rec patt_to_meta : term -> term = fun t ->
match unfold t with
| Patt(Some i,n,[||]) ->
Expand Down Expand Up @@ -552,6 +552,7 @@ let check_cp : cp_fun = fun pos _ l r p l_p _ g d s ->
all the subterms of the [sr1] LHS and all the possible rule LHS's. *)
let check_cps_subterms_eq : Pos.popt -> sym_rule -> unit =
fun pos ((_,x) as lr) ->
if Logger.log_enabled() then log_cp "check_cps_subterms_eq";
(*if Logger.log_enabled() then
log_cp "check_cps_subterms_eq@.%a@.%a" Print.rule lr Print.rule gd;*)
let l = shift (lhs lr) and r = shift (rhs lr) in
Expand All @@ -577,15 +578,18 @@ let check_cps_subterms_eq : Pos.popt -> sym_rule -> unit =
between all the rules of the signature and [sym_map]. *)
let check_cps_sign_with : Pos.popt -> Sign.t -> rule list SymMap.t -> unit =
fun pos sign sym_map ->
if Logger.log_enabled() then log_cp "check_cps_sign_with";
let f s' rs' =
match SymMap.find_opt s' !(sign.Sign.sign_cp_pos) with
| None -> ()
| Some cps ->
let h (i,l,r,p,l_p) =
let h' r' =
let i = match i with Some p -> p | None -> assert false in
let gd = (s',r') in let j = id_sym_rule gd in
cp_cand_fun check_cp pos i l r p l_p j (lhs gd) (rhs gd)
if not (is_ho r') then
let i = match i with Some p -> p | None -> assert false in
let gd = (s',r') in
let j = id_sym_rule gd in
cp_cand_fun check_cp pos i l r p l_p j (lhs gd) (rhs gd)
in List.iter h' rs'
in
List.iter h cps
Expand All @@ -597,6 +601,7 @@ let check_cps_sign_with : Pos.popt -> Sign.t -> rule list SymMap.t -> unit =
let check_cps :
Pos.popt -> Sign.t -> sym_rule list -> rule list SymMap.t -> unit =
fun pos sign srs sym_map ->
if Logger.log_enabled() then log_cp "check_cps";
(* Verification of CP*(S,S). *)
iter_cps_of_rules check_cp pos srs;
(* Verification of CP*(S,R). /!\ Here, we use the fact that decision trees
Expand Down Expand Up @@ -625,6 +630,7 @@ let update_cp_pos : Pos.popt -> cp_pos list SymMap.t -> rule list SymMap.t ->
SymMap.update s h map
in
fun pos cp_pos_map rules_map ->
if Logger.log_enabled() then log_cp "update_cp_pos";
let open Stdlib in
let map = ref cp_pos_map in
let f s rs =
Expand Down
Loading