add a meta-language for formal definitions (#69)

## Summary

Implement a meta-language for describing languages' abstract syntax and
semantics, using a macro DSL. The source language's textual definition
is replaced with a definition using the new meta-language.

## Details

The current formal definition has a few problems:
* it's not accessible to the computer, preventing mechanization and
  thus testing/validation
* the lack of any form of testing makes it very easy to introduce
  mistakes (both syntactic and semantic)
* the lack of typesetting makes it hard to read for a human reader

Using a dedicated meta-language is meant to address the problems listed
above. A macro DSL is used instead of a fully-custom language, which
has the following benefits:
* interop with NimSkull is easy, if needed
* the syntax can be built on that of NimSkull without needing a
  dedicated parser
* the output of the macro is readily available at compile-time, making
  macro-based code generation possible
* the build process stays simple

The `language` macro only constructs a `Language` instance, which is
meant to be passed to further processing (e.g., queries, code
generation, rendering, etc.).

The textual definition is replaced with a meta-language equivalent.
Some small adjustments/clarification are made where needed:
* the `l` and `ch` non-terminals; they need a concrete definition
* the `E-builtin-readFile` rule uses a placeholder definition, as
  indeterminate values cannot be described with the meta-language at
  the moment

Substituting identifiers with values (previously denoted by `e[x/v]`)
is now fully defined, via the `substitute` meta-function.

---------

Co-authored-by: Saem Ghani <[email protected]>

.github/workflows/build_and_test.yml

@@ -93,6 +93,9 @@ jobs:
       - name: Build koch
         run: nim c -d:nimStrictMode --outdir:bin koch.nim
 
+      - name: Build language definitions
+        run: bin/koch build-defs
+
       - name: Build passtool
         run: bin/koch single passtool -d:nimStrictMode -d:release
 

koch.nim

@@ -15,6 +15,8 @@ Commands:
   all [args]                  builds all programs
   single <name> [args]        builds the single program with the given name
   generate [dir]              generates the various language-related modules
+  build-defs                  verifies the language definitions and generates
+                              the textual representation for them
 """
   Programs: seq[(string, string, bool, bool)] = @[
     ("tester", "tools/tester.nim", true, true),
@@ -56,6 +58,13 @@ proc compile(file: sink string, name: string, extra: varargs[string]): bool =
   args.add file
   result = run(nimExe, args)
 
+proc check(file: sink string, extra: varargs[string]): bool =
+  ## Runs the ``check`` command on the given NimSkull `file`.
+  var args = @["check"]
+  args.add extra
+  args.add file
+  result = run(nimExe, args)
+
 proc saneSplit(s: string): seq[string] =
   ## Compared to the normal split, returns an empty sequence for an empty
   ## string.
@@ -155,6 +164,20 @@ proc generate(args: string): bool =
 
   result = true
 
+proc buildDefs(args: string): bool =
+  ## Handles verifying the language definitions and producing the artifacts
+  ## based on them.
+  if args.len > 0:
+    return false
+
+  # there's nothing to do with the compiled language definition, making sure
+  # the macro succeeds is enough
+  if not check(getCurrentDir() / "languages" / "source.nim"):
+    echo "Failure"
+    quit(1)
+
+  result = true
+
 proc showHelp(): bool =
   ## Shows the help text.
   echo HelpText
@@ -184,6 +207,8 @@ while true:
         buildSingle(opts.cmdLineRest)
       of "generate":
         generate(opts.cmdLineRest)
+      of "build-defs":
+        buildDefs(opts.cmdLineRest)
       of "help":
         showHelp()
       else:

languages/nim.cfg

@@ -0,0 +1 @@
+--path:".."