From 79e9bd64d15490dd5abc353cc5b09378d3c640d1 Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 14:39:10 +0200 Subject: [PATCH] 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) --- ocaml/lambda4.ml | 2 +- ocaml/problems.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 788fe59..ed43936 100644 --- 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 34245f0..b49cf77 100644 --- 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 *) -- 2.39.2