add a basic formal definition of the source language

[zerbina]

Summary

Add the first version of a formal definition for the source language, covering the tree grammar and the static semantics. The definition is expressed using a macro DSL.

Details

The source language specification only provides an informal definition of the language, making it inaccessible to programs and formal reasoning.

Having a formal definition of the source language would allow for formal reasoning about programs, which in turn allows for proving that some program has a certain meaning and/or behaviour.

A macro DSL (language) is used for expressing the language definition. This:

• allows re-using NimSkull's syntax, removing the need to write a dedicated lexer/parser
• makes it easy to experiment with / modify the meta-language's syntax
• makes it easy to generated code based on the language definition (by using the macro API)

The macro parses and validates the meta language and translates it into an internal data structure. Planned - but not yet implemented - usages of this data are:

• generating a human-readable definition using mathematical notation common to formal language definitions
• generating syntax checking logic (replacing the passtool functionality)
• generating code for computing the semantics of source language code

At the moment, the language macro is still missing a way to define operational semantics (i.e., a formal definition of how a program written in the source language is evaluated).

The idea is to keep the formal definition and specification side-by-side until everything in the specification can be expressed with the language macro, at which point the specification would be removed.

---

To-Do

• complete the validation logic
• document the meta language
• integrate compiling def.nim into koch and CI

Note For Reviewers

• questions / suggestions regarding the meta language are welcome
• the meta language is not meant to be final
• a major inspiration for the definition was the formal definition of Standard ML

[zerbina]

It's important to note that due to the - not yet implemented - compile-time evaluation and meta programming facilities, a strict separation between static semantics (i.e., types, symbols, etc.) and dynamic semantics (i.e., how a program behaves at run-time) is not going to be possible.