CPP semantics guidelines and ideas

Temporary stuff. Should be eventually moved into docs/ - when finished. Feel free to edit.

What we know

Modules

The standard

References to the standard

Currently, we are targetting C++20 using the most recent versions of the drafts (see draft/papers). However, previously we were targetting C++14, and so most of the references to the standard that do not explicitly mention the document number refer to N4296. We should make that explicit.

Some references are bound to a single rule, some to group of rules, some to constructor...

Example of a reference:

// N4296 3.2/3
// N4778 6.2/8
// <quote>
// [...] A destructor for a class is odr-used if it is potentially invoked.
// </quote>
rule <k> potentiallyInvokeDestructor(_ :: Class(_, X::CId, _) #as C::Class) => makeOdrUsed(Base) ...</k>
     <curr-tu> Tu::String </curr-tu>
     <tu-id> Tu </tu-id>
     <class-id> C </class-id>
     <cenv>... DestructorId(X) |-> (_ |-> envEntry(... base: Base::SymBase)) ...</cenv>

// N4296 12.4/11
// N4778 10.3.6/12
// <quote>
// A destructor is potentially invoked if it is invoked or as specified in [...]
// </quote>
rule invokeDestructor(C::Class) => potentiallyInvokeDestructor(C)

Formatting

Rules spanning multiple lines need to be surrounded with empty lines.

No trailing spaces.

Order of imports

1. self - for module M, import M-SYNTAX
2. empty line
3. all the remote modules

Some ideas for future

Namespacing

Can we do some namespacing? What about this?

module CLASS-SORTS
  syntax Class
endmodule

module CLASS-SYNTAX
  imports CLASS-SORTS
  syntax KItem ::= Class.generateDestructor(Class)
endmodule

module CLASS
  imports CLASS-SYNTAX
  // just normal code
  rule <k> Class.generateDestructor(C::Class) => doSomething ...</k>
endmodule

module CLASS-IMPORTED-SYNTAX
  imports CLASS-SORTS
  // syntactic sugar
  syntax KItem ::= generateDestructor(Class) [function]
endmodule

module CLASS-IMPORTED
  imports CLASS-IMPORTED-SYNTAX
  imports CLASS-SYNTAX

  // desugaring rules
  rule generateDestructor(C::Class) => Class.generateDestructor(C)
endmodule

This way, modules working only remotely with classes, could simply import CLASS-SYNTAX and use the prefixed variants. But if some module uses classes heavily, it may import CLASS-IMPORTED-SYNTAX and use the shorter variant. The problem with the above implementation is that the CLASS module needs to use the prefixed variants, too. Maybe we can use the same KLabels...?

TODO let Jenkins auto build only PRs that do not have a particular label (do-not-build-yet).