Skip to content

Commit

Permalink
dedupe closures generated by #let (#4584)
Browse files Browse the repository at this point in the history
Previously we were generating one LHS term in each `#let` lambda per use
of a particular variable. This introduced complexity for the resulting
rule which needed to check that each capture of the same variable had
the same value, which is unnecessary work. We fix this by simply
deduping the closure so that each variable can be captured at most once
by any given lambda.
  • Loading branch information
Dwight Guth authored Aug 16, 2024
1 parent dcd3440 commit fdff3e7
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ private List<KVariable> closure(K k) {
List<KVariable> result = new ArrayList<>();
new GatherVarsVisitor(true, errors, vars, false).apply(k);
new ComputeUnboundVariables(true, true, errors, vars, result::add).apply(k);
return result;
return result.stream().distinct().collect(Collectors.toList());
}

private Production funProd(KLabel fun, K k, Sort arg, boolean total) {
Expand Down

0 comments on commit fdff3e7

Please sign in to comment.