From 41a526ec0fede7bd53659b6a50918a5d589bb57b Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Wed, 13 Mar 2024 17:30:54 +0100 Subject: [PATCH] [sc-504] Fix wrong variable being used on match binds with same name --- src/lib.rs | 20 +++++++++++++++++++ ...compile_file__repeated_bind_match.hvm.snap | 2 +- .../compile_file__repeated_bind_rule.hvm.snap | 2 +- 3 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 1926c3d87..1f70acbe6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -136,6 +136,26 @@ pub fn desugar_book( ctx.check_unbound_vars()?; ctx.book.convert_match_def_to_term(); + + // TODO: We give variables fresh names before the match + // simplification to avoid `foo a a = a` binding to the wrong + // variable (it should be the second `a`). Ideally we'd like this + // pass to create the binds in the correct order, but to do that we + // have to reverse the order of the created let expressions when we + // have multiple consecutive var binds without a match in between, + // and I couldn't think of a simple way of doing that. + // + // In the paper this is not a problem because all var matches are + // pushed to the end, so it only needs to fix it in the irrefutable + // rule case. We could maybe do the opposite and do all var matches + // first, when it would also become easy to deal with. But this + // would potentially generate suboptimal lambda terms, need to think + // more about it. + // + // We technically still generate the let bindings in the wrong order + // but since lets can float between the binds it uses in its body + // and the places where its variable is used, this is not a problem. + ctx.book.make_var_names_unique(); ctx.simplify_matches()?; if opts.linearize_matches.enabled() { diff --git a/tests/snapshots/compile_file__repeated_bind_match.hvm.snap b/tests/snapshots/compile_file__repeated_bind_match.hvm.snap index 6cc335d6c..5daf52ad6 100644 --- a/tests/snapshots/compile_file__repeated_bind_match.hvm.snap +++ b/tests/snapshots/compile_file__repeated_bind_match.hvm.snap @@ -8,4 +8,4 @@ In definition 'main': @List.cons = (a (b {2 {2 a {2 b c}} {2 * c}})) @List.nil = {2 * {2 a a}} -@main = ({2 {2 a {2 * a}} {2 * b}} b) +@main = ({2 {2 * {2 a a}} {2 * b}} b) diff --git a/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap b/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap index 4d647e2d6..38c6a4ed8 100644 --- a/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap +++ b/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap @@ -6,6 +6,6 @@ Warnings: In definition 'Foo': Repeated bind inside rule pattern: 'a'. -@Foo = (a (* a)) +@Foo = (* (a a)) @main = a & @Foo ~ (#1 (#2 a))