Provide better documentation for concrete and symbolic attributes

[ana-pantilie]

Fixes runtimeverification/haskell-backend#3564

[radumereuta]

@virgil-serbanuta I'm tagging you for review since you are the one that encountered the issue.

[ana-pantilie]

Thanks @radumereuta , I should have taken a better look at Virgil's example and at the actual code! I can confirm it's as you understood, so this is ready for re-review. Also @virgil-serbanuta please review to make sure I didn't get it wrong again :).

[radumereuta]

What happens if you put both concrete and symbolic on the same rule?
I would expect it to be an error.
What if you give them arguments and only half of the variables are concrete and the other half are symbolic. Then I would expect that to work.
Does that make sense? Does the backend support such a behavior?

[ana-pantilie]

@radumereuta Hmm, good questions.

If you add symbolic and concrete at the same time the frontend catches it and emits an error:

[Error] Compiler: Rule cannot be both concrete and symbolic in the same
variable.
        Source(/home/ana/RV/haskell-backend/test/imp/imp.k)
        Location(223,8,223,29)
        223 |     rule X:Int +Int Y:Int => Y [simplification, symbolic, concrete]
            .          ^~~~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 structural errors.

The following, however, isn't caught by the frontend and I think it should be:

rule X:Int +Int Y:Int => Y [simplification, symbolic(X), concrete(X)]

The following works fine, as it should:

rule X:Int +Int Y:Int => Y [simplification, symbolic(X), concrete(Y)]

[ehildenb]

The rules for concrete and symbolic are different for axioms and for simplification rules.

• For axioms: if you have concrete/symbolic on any of the rules for a given production, it must be the same on all the rules for that production. No calling out of individual variables allowed. https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java#L152 (see discussion: [Bug] kompile rejects non-concrete simplification rule in the presence of concrete function rule #1591)
• For simplification: Each rule must be individually sound anyway. So you can have independent concrete(...), symbolic(...) attributes with on cross-checking between rules.

[radumereuta]

I've added a better error message for when a variable is used on both symbolic and concrete attributes.
@ana-pantilie can you please review that part? I'm going to approve it. Add automerge if everything looks good.

[virgil-serbanuta]

Thank you!

Sorry for the late reply, I was on vacation, but this looks good!