Fixed: was using compare in place of eta_eq

in particular, eta_eq ignores arities of variables

there used to be cases of duplicate entries in PS (up to arities of variables)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 788fe5983357dddd15e531364f8203664570ed86..ed43936638020efe31958242c0edd27b11834f60 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -126,7 +126,7 @@ let simple_expand_match ps =
     (try
        (match u with
          | #i_n_var as u ->
-            let i = index_of (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
+            let i = index_of ~eq:eta_eq (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
             let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in
             if t <> torig then
              aux_i_num_var level t

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 34245f074b5eb38fc1fbf2ae8c595f0a9f6638e0..b49cf7733578832c022cc994b87ccc6599660a3e 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -285,7 +285,7 @@ solve_many [
    (* 3 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a";
    (* 4 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a";
  ];
- (*problem_of
+ problem_of
  (* DISPLAY PROBLEM (main) - measure=561
     Discriminating sets (deltas):
     0 <> 1 <> 2 <> 3 <> 4
@@ -303,7 +303,7 @@ solve_many [
    (* 2 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a";
    (* 3 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a";
    (* 4 *) "g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a";
- ]*)
+ ]
 ];;
 
 (* This fails *)