Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/develop'
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Sep 17, 2024
2 parents 6e23a83 + 861cda4 commit 732aa25
Show file tree
Hide file tree
Showing 19 changed files with 107 additions and 26 deletions.
10 changes: 7 additions & 3 deletions docs/user_manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/domains.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/list-set/00.test
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
l(0, 0)
10 changes: 10 additions & 0 deletions k-distribution/tests/regression-new/list-set/00.test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
<generatedTop>
<k>
.K
</k>
<list>
ListItem ( 0 )
ListItem ( 1 )
ListItem ( 2 )
</list>
</generatedTop>
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/list-set/01.test
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
l(0, 1)
10 changes: 10 additions & 0 deletions k-distribution/tests/regression-new/list-set/01.test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
<generatedTop>
<k>
l ( 0 , 1 ) ~> .K
</k>
<list>
ListItem ( 0 )
ListItem ( 1 )
ListItem ( 2 )
</list>
</generatedTop>
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/list-set/11.test
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
l(1, 1)
10 changes: 10 additions & 0 deletions k-distribution/tests/regression-new/list-set/11.test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
<generatedTop>
<k>
.K
</k>
<list>
ListItem ( 0 )
ListItem ( 1 )
ListItem ( 2 )
</list>
</generatedTop>
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/list-set/22.test
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
l(2, 2)
10 changes: 10 additions & 0 deletions k-distribution/tests/regression-new/list-set/22.test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
<generatedTop>
<k>
.K
</k>
<list>
ListItem ( 0 )
ListItem ( 1 )
ListItem ( 2 )
</list>
</generatedTop>
7 changes: 7 additions & 0 deletions k-distribution/tests/regression-new/list-set/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
DEF=test
EXT=test
TESTDIR=.
KOMPILE_BACKEND=llvm
KOMPILE_FLAGS=--syntax-module TEST

include ../../../include/kframework/ktest.mak
11 changes: 11 additions & 0 deletions k-distribution/tests/regression-new/list-set/test.k
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module TEST
imports LIST
imports INT

configuration <k> $PGM:K </k> <list> ListItem(0) ListItem(1) ListItem(2) </list>

syntax KItem ::= l(Int, Int)

rule <k> l(I, J) => .K ...</k>
<list> _ [ I <- J ] </list>
endmodule
Original file line number Diff line number Diff line change
Expand Up @@ -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-");
Expand Down Expand Up @@ -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("()");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
2 changes: 2 additions & 0 deletions k-frontend/src/main/scala/org/kframework/attributes/Att.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.");
Expand Down
1 change: 1 addition & 0 deletions pyk/src/pyk/kast/att.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
6 changes: 2 additions & 4 deletions pyk/src/pyk/konvert/_module_to_kore.py
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down Expand Up @@ -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 [])
)
)

Expand Down

0 comments on commit 732aa25

Please sign in to comment.