Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add algorithmic backend #53

Merged
merged 959 commits into from
Jan 24, 2024
Merged

Add algorithmic backend #53

merged 959 commits into from
Jan 24, 2024

Conversation

f52985
Copy link
Collaborator

@f52985 f52985 commented Jan 11, 2024

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
Copy link
Collaborator Author

f52985 commented Jan 23, 2024

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.

Copy link
Collaborator

@rossberg rossberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Excellent, thanks!

Re 1: Yes, that's totally fine with me.

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.

spectec/src/frontend/elab.ml Outdated Show resolved Hide resolved
spectec/src/backend-latex/config.ml Outdated Show resolved Hide resolved
spectec/src/backend-splice/config.ml Show resolved Hide resolved
spectec/src/backend-latex/render.mli Outdated Show resolved Hide resolved
spectec/src/backend-latex/render.mli Outdated Show resolved Hide resolved
spectec/src/backend-splice/splice.ml Outdated Show resolved Hide resolved
spectec/src/backend-splice/splice.mli Outdated Show resolved Hide resolved
spectec/src/il/validation.ml Outdated Show resolved Hide resolved
spectec/README.md Outdated Show resolved Hide resolved
@f52985
Copy link
Collaborator Author

f52985 commented Jan 24, 2024

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.

Copy link
Collaborator

@rossberg rossberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Excellent, thanks!

spectec/src/il/validation.ml Outdated Show resolved Hide resolved
@f52985 f52985 merged commit 55b511a into main Jan 24, 2024
1 check passed
@f52985 f52985 deleted the al-merge branch January 25, 2024 06:26
rossberg added a commit that referenced this pull request Jul 3, 2024
Add missing memory specifier to memory.init execution semantics
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants