Provide better documentation for concrete and symbolic attributes (#3324

)

* Provide better documentation for concrete and symbolic attributes

* Fix

* Fix 2

* Add error for concrete-symbolic variable clashes

---------

Co-authored-by: Radu Mereuta <headness13@gmail.com>

docs/user_manual.md

@@ -1344,20 +1344,39 @@ warning if it encounters such a claim.
 
 ### `concrete` and `symbolic` attributes (Haskell backend)
 
-Sometimes you only want a rule to apply if some or all arguments are concrete
-(not symbolic). This is done with the `concrete` attribute. Conversely, the
-`symbolic` attribute will allow a rule to apply only when some arguments are not
-concrete. These attributes should only be given with the `simplification`
-attribute.
-
-For example, the following will only re-associate terms when all arguments
+Users can control the application of `simplification` rules using the `concrete`
+and the `symbolic` attributes by specifying the type of patterns the rule's
+arguments are to match.
+
+A concrete pattern is a pattern which does not contain variables or unevaluated
+functions, otherwise the pattern is symbolic.
+
+The semantics of the two attributes is defined as follows:
+- If a simplification rule is marked `concrete`, then _all_ arguments must be
+concrete for the rule to match.
+- If a simplification rule is marked `symbolic`, then _all_ arguments must be
+symbolic for the rule to match.
+- The following syntax `concrete(<variables>)` (resp. `symbolic(<variables>)`),
+where `<variables>` is a list of variable names separated by commas, can be used
+to specify the exact arguments the user expects to match concrete (resp. symbolic)
+patterns.
+
+For example, the following will only match when all arguments
 are concrete:
 
 ```k
 rule X +Int (Y +Int Z) => (X +Int Y) +Int Z [simplification, concrete]
 ```
 
-These rules will re-associate and commute terms to combine concrete arguments:
+Conversely, the following will only match when all arguments
+are symbolic:
+
+```k
+rule X +Int (Y +Int Z) => (X +Int Y) +Int Z [simplification, symbolic]
+```
+
+In practice, the following rules will re-associate and commute terms to combine
+concrete arguments:
 
 ```k
 rule (A +Int Y) +Int Z => A +Int (Y +Int Z)

k-distribution/tests/regression-new/checks/concrete.k

@@ -28,4 +28,9 @@ module CONCRETE
 
   syntax Int ::= baz3(Int) [function]
   rule baz3(X) => 0 [concrete(X)]
+
+  syntax Int ::= baz4(Int, Int) [function]
+  rule baz4(A, B) => baz4(B, A) [concrete(A), symbolic(A, B), simplification]
+  rule baz4(A, B) => baz4(B, A) [concrete(A), symbolic, simplification]
+  rule baz4(C, D) => baz4(D, C) [concrete(C), symbolic(D), simplification]
 endmodule

k-distribution/tests/regression-new/checks/concrete.k.out

@@ -28,4 +28,14 @@
 	Location(30,8,30,20)
 	30 |	  rule baz3(X) => 0 [concrete(X)]
 	   .	       ^~~~~~~~~~~~
-[Error] Compiler: Had 6 structural errors.
+[Error] Compiler: Rule cannot be both concrete and symbolic in the same variable: [A]
+	Source(concrete.k)
+	Location(33,8,33,32)
+	33 |	  rule baz4(A, B) => baz4(B, A) [concrete(A), symbolic(A, B), simplification]
+	   .	       ^~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Rule cannot be both concrete and symbolic in the same variable.
+	Source(concrete.k)
+	Location(34,8,34,32)
+	34 |	  rule baz4(A, B) => baz4(B, A) [concrete(A), symbolic, simplification]
+	   .	       ^~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 8 structural errors.

kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java

@@ -2,6 +2,7 @@
 package org.kframework.compile.checks;
 
 import com.google.common.collect.ImmutableSet;
+import org.apache.commons.collections4.CollectionUtils;
 import org.kframework.Collections;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.Source;
@@ -26,11 +27,7 @@
 
 import java.io.File;
 import java.io.IOException;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Map;
-import java.util.Optional;
-import java.util.Set;
+import java.util.*;
 import java.util.stream.Collectors;
 import scala.Tuple2;
 
@@ -166,6 +163,9 @@ public void check(Module mainMod) {
                     allSymbolic = false;
                 }
             }
+            // If concrete or symbolic is used on the rule for a function, force all of them to have the same attribute
+            // to keep the soundness of the definition. Exception are simplification rules which need to be sound by themselves.
+            // https://github.com/runtimeverification/k/issues/1591
             for (Rule rule : iterable(mainMod.rulesFor().get(function).getOrElse(() -> Collections.<Rule>Set()))) {
                 if (rule.att().contains(Att.CONCRETE()) && !allConcrete && !rule.att().contains(Att.SIMPLIFICATION())) {
                     errors.add(KEMException.compilerError("Found concrete attribute without simplification attribute on function with one or more non-concrete rules.", rule));
@@ -175,6 +175,20 @@ public void check(Module mainMod) {
                 }
             }
         }
+        for (Rule rule : iterable(mainMod.rules())) {
+            Att att = rule.att();
+            if (att.contains(Att.SIMPLIFICATION()) && att.contains(Att.CONCRETE()) && att.contains(Att.SYMBOLIC())) {
+                Collection<String> concreteVars = Arrays.stream(att.get(Att.CONCRETE()).split(","))
+                        .map(String::trim).collect(Collectors.toList());
+                Collection<String> symbolicVars = Arrays.stream(att.get(Att.SYMBOLIC()).split(","))
+                        .map(String::trim).collect(Collectors.toList());
+                if (concreteVars.isEmpty() || symbolicVars.isEmpty())
+                    errors.add(KEMException.compilerError("Rule cannot be both concrete and symbolic in the same variable.", rule));
+                Collection<String> intersection = CollectionUtils.intersection(concreteVars, symbolicVars);
+                if (!intersection.isEmpty())
+                    errors.add(KEMException.compilerError("Rule cannot be both concrete and symbolic in the same variable: " + intersection, rule));
+            }
+        }
     }
 
     private static final ImmutableSet<String> internalDuplicates = ImmutableSet.of("#EmptyKList", "#EmptyK", "#ruleRequires", "#ruleRequiresEnsures", "#Top", "#Bottom");