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 []) ) )