[K-Improvement] User Manual

Start with the User Manual sections named in the issue, especially Attribute Index, and inspect domains.md for the listed attributes. Review each unchecked item against its documented and standard-library usage, then update the manual or record the necessary frontend cleanup; done means the attribute documentation and classifications are consistent.

Missing attributes in Attribute Index (but used in the K standard library):

• not-lr1
  • Documented in the user manual, used to flag incompatibility with Bison parsers.
• returnsUnit:
  • It seems that this actually isn't used anywhere in either backend, so we should just remove this attribute from the frontend. The only place it shows up is in domains.md.
• unblock
  • Used for internal code generation related to standard input / output streams. Doesn't seem like it should ever appear in user code - internal code generation specifies that the [unblock] rule must be unique.
• unparseAvoid
  • Appears in the standard library, but I'm not 100% sure that the use there is valid to appear in user code. Possibly if constructing KORE by hand?
• defaultBracket
  • Used in one regression test but nowhere else - @dwightguth introduced here
• impure
  • Prevents hooks from participating in constant folding; was used more extensively in the Java backend but we definitely want to keep it. Not sure it should appear in user code any more, though, as constant folding requires internal implementation and we don't do anything with it on Haskell / LLVM.
• index(0)
  • This seems to be defunct; it was added in #643 for Java backend specific changes.
• mlBinder
  • Used in ModuleToKore, probably doesn't seem to be valid for user code.

Addressed below the line:

• stream="_"
• kast, kore (modules)
• symbolic, concrete (modules)

This issue gives a list of improvements for the User Manual.

• In section Parametric productions and bracket attributes, one can read

syntax {Sort} Sort ::= Sort "=>" Sort

and

Rewrites, which can rewrite a value of any sort to a value of the same sort, or to a different sort which is allowed in that context.

It seems that the sentence corresponds to that piece of code:

syntax {Sort1, Sort2} Sort2 ::= Sort1 "=>" Sort2

• It seems that the section Macros and Aliases need to be updated. The unboundVariables attribute section needs to be updated.

• In the section smt-lemma, lemma, and trusted attributes, one can read:

These attributes guide the prover when it tries to apply rules to discharge a proof obligation.

whereas in the section Attribute Index

• trusted = claim haskell

• smt-lemma = rule all

• lemma = rule all
  These three attributes are only available for the Haskell backend, right?

• The section concrete attribute, #isConcrete and #isVariable function (Java backend) is maybe depreciated.

• In the section Attribute Index:

• I surprised that all-path = claim haskell wheras one-path = claim all

• heat, cool and structural are depreciated, right?

• I think this section will be clearer if there are several tables, one for each type.

• The attribute injective seems to have been forgotten.

In https://kframework.org/k-distribution/include/kframework/builtin/domains/, one can read:

syntax Map ::= KItem "|->" KItem   
         [function, functional, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2}), injective]

and

syntax Set ::= SetItem(KItem)  [function, functional, hook(SET.element), klabel(SetItem), symbol, injective]