From 861cda4d22e19a17d76068100ebe8a9bd40b949c Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 17 Sep 2024 10:26:37 -0500 Subject: [PATCH] Handle list random access patterns in frontend (#4634) This PR adds support for the `L [ I <- X ]` syntax on the LHS of rules, which allows you to pattern match on an arbitrary element of a list. The code is not fully polished; it is not integrated with configuration abstraction or cell collections. It is not likely to be further improved upon presently because the code it was intended to support ended up not proving worth merging. However, it is broadly useful functionality (along with the accompanying LLVM backend PR) and thus ought to be merged. --------- Co-authored-by: Dwight Guth --- docs/user_manual.md | 10 ++++-- .../include/kframework/builtin/domains.md | 2 +- .../tests/regression-new/list-set/00.test | 1 + .../tests/regression-new/list-set/00.test.out | 10 ++++++ .../tests/regression-new/list-set/01.test | 1 + .../tests/regression-new/list-set/01.test.out | 10 ++++++ .../tests/regression-new/list-set/11.test | 1 + .../tests/regression-new/list-set/11.test.out | 10 ++++++ .../tests/regression-new/list-set/22.test | 1 + .../tests/regression-new/list-set/22.test.out | 10 ++++++ .../tests/regression-new/list-set/Makefile | 7 ++++ .../tests/regression-new/list-set/test.k | 11 ++++++ .../kframework/backend/kore/ModuleToKORE.java | 6 +++- .../compile/checks/CheckFunctions.java | 6 ++++ .../utils/errorsystem/KEMException.java | 2 +- .../scala/org/kframework/attributes/Att.scala | 2 ++ .../kframework/backend/llvm/LLVMBackend.java | 36 ++++++++++--------- pyk/src/pyk/kast/att.py | 1 + pyk/src/pyk/konvert/_module_to_kore.py | 6 ++-- 19 files changed, 107 insertions(+), 26 deletions(-) create mode 100644 k-distribution/tests/regression-new/list-set/00.test create mode 100644 k-distribution/tests/regression-new/list-set/00.test.out create mode 100644 k-distribution/tests/regression-new/list-set/01.test create mode 100644 k-distribution/tests/regression-new/list-set/01.test.out create mode 100644 k-distribution/tests/regression-new/list-set/11.test create mode 100644 k-distribution/tests/regression-new/list-set/11.test.out create mode 100644 k-distribution/tests/regression-new/list-set/22.test create mode 100644 k-distribution/tests/regression-new/list-set/22.test.out create mode 100644 k-distribution/tests/regression-new/list-set/Makefile create mode 100644 k-distribution/tests/regression-new/list-set/test.k diff --git a/docs/user_manual.md b/docs/user_manual.md index 4d3de7eda70..b397361d148 100644 --- a/docs/user_manual.md +++ b/docs/user_manual.md @@ -2225,6 +2225,9 @@ ListItem(E1) ListItem(E2) L:List ListItem(E3) ListItem(E4) // the empty list .List +// 1 or more list update operations applied to a variable +L:List [ K1 <- E1 ] [ K2 <- E2 ] + // 0 or more elements in any order plus 0 or 1 variables of sort Set // in any order SetItem(K1) SetItem(K2) S::Set SetItem(K3) SetItem(K4) @@ -2255,9 +2258,10 @@ though E3 is itself unbound. In the above examples, E1, E2, E3, and E4 can be any pattern that is normally allowed on the lhs of a rule. -When a map or set key contains function symbols, we know that the variables in -that key are bound (because of the above restriction), so it is possible to -evaluate the function to a concrete term prior to performing the lookup. +When a map, set, or list key contains function symbols, we know that the +variables in that key are bound (because of the above restriction), so it is +possible to evaluate the function to a concrete term prior to performing the +lookup. Indeed, this is the precise semantics which occurs; the function is evaluated and the result is looked up in the collection. diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 675a7338f7a..b04af99c8e8 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -926,7 +926,7 @@ side, it is O(N), where N is the number of elements matched on the front and back of the list. ```k - syntax List ::= List List [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), format(%1%n%2)] + syntax List ::= List List [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), update(List:set), format(%1%n%2)] ``` ### List unit diff --git a/k-distribution/tests/regression-new/list-set/00.test b/k-distribution/tests/regression-new/list-set/00.test new file mode 100644 index 00000000000..7b2f1465b52 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/00.test @@ -0,0 +1 @@ +l(0, 0) diff --git a/k-distribution/tests/regression-new/list-set/00.test.out b/k-distribution/tests/regression-new/list-set/00.test.out new file mode 100644 index 00000000000..100c9ef574d --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/00.test.out @@ -0,0 +1,10 @@ + + + .K + + + ListItem ( 0 ) + ListItem ( 1 ) + ListItem ( 2 ) + + diff --git a/k-distribution/tests/regression-new/list-set/01.test b/k-distribution/tests/regression-new/list-set/01.test new file mode 100644 index 00000000000..16f2fff0444 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/01.test @@ -0,0 +1 @@ +l(0, 1) diff --git a/k-distribution/tests/regression-new/list-set/01.test.out b/k-distribution/tests/regression-new/list-set/01.test.out new file mode 100644 index 00000000000..88ae6f598f4 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/01.test.out @@ -0,0 +1,10 @@ + + + l ( 0 , 1 ) ~> .K + + + ListItem ( 0 ) + ListItem ( 1 ) + ListItem ( 2 ) + + diff --git a/k-distribution/tests/regression-new/list-set/11.test b/k-distribution/tests/regression-new/list-set/11.test new file mode 100644 index 00000000000..fba64fc21b7 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/11.test @@ -0,0 +1 @@ +l(1, 1) diff --git a/k-distribution/tests/regression-new/list-set/11.test.out b/k-distribution/tests/regression-new/list-set/11.test.out new file mode 100644 index 00000000000..100c9ef574d --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/11.test.out @@ -0,0 +1,10 @@ + + + .K + + + ListItem ( 0 ) + ListItem ( 1 ) + ListItem ( 2 ) + + diff --git a/k-distribution/tests/regression-new/list-set/22.test b/k-distribution/tests/regression-new/list-set/22.test new file mode 100644 index 00000000000..29c170d2bf1 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/22.test @@ -0,0 +1 @@ +l(2, 2) diff --git a/k-distribution/tests/regression-new/list-set/22.test.out b/k-distribution/tests/regression-new/list-set/22.test.out new file mode 100644 index 00000000000..100c9ef574d --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/22.test.out @@ -0,0 +1,10 @@ + + + .K + + + ListItem ( 0 ) + ListItem ( 1 ) + ListItem ( 2 ) + + diff --git a/k-distribution/tests/regression-new/list-set/Makefile b/k-distribution/tests/regression-new/list-set/Makefile new file mode 100644 index 00000000000..d48aaade4fd --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/Makefile @@ -0,0 +1,7 @@ +DEF=test +EXT=test +TESTDIR=. +KOMPILE_BACKEND=llvm +KOMPILE_FLAGS=--syntax-module TEST + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/list-set/test.k b/k-distribution/tests/regression-new/list-set/test.k new file mode 100644 index 00000000000..6129c475fb8 --- /dev/null +++ b/k-distribution/tests/regression-new/list-set/test.k @@ -0,0 +1,11 @@ +module TEST + imports LIST + imports INT + + configuration $PGM:K ListItem(0) ListItem(1) ListItem(2) + + syntax KItem ::= l(Int, Int) + + rule l(I, J) => .K ... + _ [ I <- J ] +endmodule diff --git a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 2ed1e40787d..1e37185f055 100644 --- a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -427,6 +427,10 @@ private void translateSorts( att.add(Att.ELEMENT(), K.class, KApply(KLabel(concatProd.att().get(Att.ELEMENT())))); att = att.add(Att.CONCAT(), K.class, KApply(concatProd.klabel().get())); att = att.add(Att.UNIT(), K.class, KApply(KLabel(concatProd.att().get(Att.UNIT())))); + if (concatProd.att().contains(Att.UPDATE())) { + att = + att.add(Att.UPDATE(), K.class, KApply(KLabel(concatProd.att().get(Att.UPDATE())))); + } sb.append("hooked-"); } else { sb.append("hooked-"); @@ -2102,7 +2106,7 @@ private void convert( convertStringVarList(location, freeVarsMap, strVal, sb); } else { switch (strKey) { - case "unit", "element" -> { + case "unit", "element", "update" -> { Production prod = production(KApply(KLabel(strVal))); convert(prod.klabel().get(), prod.params(), sb); sb.append("()"); diff --git a/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java index 323d290fa61..4770c56117d 100644 --- a/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -56,6 +56,7 @@ && isLHS() && !(hook.equals("LIST.element") || hook.equals("LIST.concat") || hook.equals("LIST.unit") + || hook.equals("LIST.update") || hook.equals("SET.element") || hook.equals("SET.concat") || hook.equals("SET.unit") @@ -79,6 +80,11 @@ && isLHS() apply(k.items().get(1)); return; } + if (hook.equals("LIST.update")) { + apply(k.items().get(0)); + apply(k.items().get(2)); + return; + } super.apply(k); } }.apply(body); diff --git a/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java index b97365c56d0..1ffd756b954 100644 --- a/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java +++ b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java @@ -19,7 +19,7 @@ public class KEMException extends RuntimeException { public final KException exception; - KEMException(KException e) { + public KEMException(KException e) { super(e.toString(), e.getException()); this.exception = e; } diff --git a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala index 040ebcc6265..aedfdda9371 100644 --- a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala +++ b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala @@ -442,6 +442,8 @@ object Att { Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) final val UNUSED = Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val UPDATE = + Key.builtin("update", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) final val WRAP_ELEMENT = Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index 42df5042047..420f6c16761 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -65,22 +65,26 @@ public void accept(Backend.Holder h) { MutableInt warnings = new MutableInt(); boolean optimize = kompileOptions.optimize1 || kompileOptions.optimize2 || kompileOptions.optimize3; - Matching.writeDecisionTreeToFile( - files.resolveKompiled("definition.kore"), - options.heuristic, - files.resolveKompiled("dt"), - Matching.getThreshold(getThreshold()), - !optimize, - globalOptions.includesExceptionType(ExceptionType.USELESS_RULE), - options.enableSearch, - ex -> { - var translated = translateError(ex, hookAtts); - kem.addKException(translated); - if (globalOptions.includesExceptionType(translated.getType())) { - warnings.increment(); - } - return null; - }); + try { + Matching.writeDecisionTreeToFile( + files.resolveKompiled("definition.kore"), + options.heuristic, + files.resolveKompiled("dt"), + Matching.getThreshold(getThreshold()), + !optimize, + globalOptions.includesExceptionType(ExceptionType.USELESS_RULE), + options.enableSearch, + ex -> { + var translated = translateError(ex, hookAtts); + kem.addKException(translated); + if (globalOptions.includesExceptionType(translated.getType())) { + warnings.increment(); + } + return null; + }); + } catch (MatchingException e) { + throw new KEMException(translateError(e, hookAtts)); + } sw.printIntermediate(" Write decision tree"); if (warnings.intValue() > 0 && kem.options.warnings2errors) { throw KEMException.compilerError("Had " + warnings.intValue() + " pattern matching errors."); diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index d730bbd67de..0312e5c436a 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -349,6 +349,7 @@ class Atts: UNIT: Final = AttKey('unit', type=_STR) UNIQUE_ID: Final = AttKey('UNIQUE_ID', type=_ANY) UNPARSE_AVOID: Final = AttKey('unparseAvoid', type=_NONE) + UPDATE: Final = AttKey('update', type=_ANY) USER_LIST: Final = AttKey('userList', type=_ANY) WRAP_ELEMENT: Final = AttKey('wrapElement', type=_ANY) diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index d87ec49e461..8ab509a2501 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -187,14 +187,11 @@ def _parse_special_att_value(key: AttKey, value: Any) -> tuple[tuple[Sort, ...], if key == Atts.FORMAT: assert isinstance(value, Format) return (), (String(value.unparse()),) - if key == Atts.ELEMENT: + if key == Atts.ELEMENT or key == Atts.UNIT or key == Atts.UPDATE: # TODO avoid special casing by pre-processing the attribute into a KApply # This should be handled by the frontend assert isinstance(value, str) return (), (App(_label_name(value)),) - if key == Atts.UNIT: # TODO same here - assert isinstance(value, str) - return (), (App(_label_name(value)),) return None @@ -891,6 +888,7 @@ def _update(syntax_sort: KSyntaxSort, concat_atts: Mapping[KSort, KAtt]) -> KSyn Atts.ELEMENT(concat_att[Atts.ELEMENT]), Atts.UNIT(concat_att[Atts.UNIT]), ] + + ([Atts.UPDATE(concat_att[Atts.UPDATE])] if Atts.UPDATE in concat_att else []) ) )