From fdff3e7b7cf8e5b24907479f8957f7a61beaef5b Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 16 Aug 2024 11:45:06 -0500 Subject: [PATCH] dedupe closures generated by #let (#4584) 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. --- k-frontend/src/main/java/org/kframework/compile/ResolveFun.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java index ed7fccdd4d3..3e958126829 100644 --- a/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java +++ b/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java @@ -214,7 +214,7 @@ private List closure(K k) { List 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) {