Add algorithmic backend

[f52985]

This pull request adds algorithmic backends (prose, interpreter):

• src/al directory contains the syntax and other utility functions for the intermediate representation algorithmic language AL.
• src/backend-prose, src/backend-interpreter contains the code for generating prose and (meta-level) interpreter from the input spec.
• Targets Prose and Interpreter can be selected as the target by command argument.
• test-prose and test-interpreter contains the test code for these backends.

It also contains a few changes to other part of the code:

• spec/wasm-3.0 now contains syntax, validation rules, and reduction rules for SIMD instructions. (which is planned to be copied to spec/wasm-2.0 after testing with official test-suite)
• The splicing is now done via the separated target Splice instead of Latex, and splicing now creates a new file instead of modifying the input file in-place.
• There's a new print function, structured_string_of for el and il, which prints the AST in a "structured" manner, mainly used during debugging.

[f52985]

Thanks for the review! We'll soon address each issue. Here are the thoughts on the review in the main comments.

The one structural change I'd request is to remove the duplicate of the reference_interpreter inside backend-interpreter. Obviously, we do not want to maintain two copies of this code. The original code is in the same repo, so it should be possible to set things up such that we can import it from there.

Yes, that was what we also wanted to do, but we couldn't figure out how to do. Although they are in the same repository, they are separated dune-project, and we could not find a way to import reference interpreter in spectec.

However, there is another problem: reference_interpreter should be able to parse wasm3 proposals in order to parse wasm3 tests. (In fact, current reference_interpreter is actually copied from gc proposal's repo, not this repo). Even if we (somehow figure out how to) use interpreter in the same repo, it won't be able to parse wasm3 tests.

One other change I'm not sure I like is the way how splice output files are given. While I sympathise with the desire to avoid destructive file update, a separate list of file names is at odds with Unix conventions. I was following the sed model, which is easier to use directly – e.g., I envisioned that one can do something as simple as cp -R src out; watsup src/*/.watsup to transform an entire document tree. In contrast, the new command syntax essentially necessitates a Makefile to produce all the output file paths economically. If we wanted a non-mutable model, then the Unix way would be to derive output file names automatically from input names, e.g., by appending an extension. Or allow only one file at a time. Not sure either is better, though, when the goal is to run over entire directory trees.

I see, so the main point here is that we do need in-place file mutation, especially because we want to mutate the entire directory. In that case, I would like to suggest to add a command option that flags in-place mutation. That is what sed is also doing. sed prints the result to the stdout by default and do the mutation when -i option is given, so we can take the similar approach.

[f52985]

Most comments are now resolved, and there are 2 remaining:

1. Pretty printer using sexpr Considering the effort to convert each AST into sexpr, I think the pretty printer should be merged with a separated pull request.

2. Copying reference interpreter I tried to do some workaround for using reference interpreter in gc proposal without copying it, but it makes the compiling process rather clumsy. Considering the fact that

   • the sole reason for using reference interpreter is its parser,
   • the changes in the actual reference interpreter need not be reflected to the copied reference interpreter for the purpose of parsing,
   • and the parser would also be (hopefully) automatically generated using SpecTec, I think using the fixed, copied version of reference interpreter would be OK for now.

[f52985]

All comments are resolved now.

Re 2: Does just git cloning it into a subdirectory not work? That could be performed by something as simple as an explicit setup target in the Makefile (though doing it automatically would of course be nicer). I'd really like to avoid having copied code, as that always becomes a liability quickly.

I modified the Makefile in a way that it clones the repository for gc-proposal before building with a fixed commit hash (so that it can prevent the situation where new commits to gc-proposal's interpreter break the compilation). This cloned repository is git-ignored, and removed upon make clean.