omelkonian/agda2rust

Rust backend for Agda.

[WIP] A new Agda backend for compiling to Rust

• The backend is defined in src/Main.hs.
• A custom pipeline for translating internal syntax to the treeless representation is in src/AgdaInternals.hs.
• The test/ directory contains a golden-testing suite (c.f. test/AllTests.agda).

How to run

Assuming a working Haskell installation with ghc and cabal (e.g. using ghcup):

• $ make build builds the project
• $ make install installs the agda2rust executable
• $ make test runs the test suite
• $ make repl starts an interactive session with the agda2rust library loaded
• $ make html renders the Github website where you can navigate through the Agda test cases alongside the corresponding generated Rust code

TODO

• Switch to treeless syntax
• identifiers
  • transcribe to valid Rust identifiers (e.g. remove Unicode somehow)
  • ensure qualification/scopes are OK
• primitive/builtin types
  • Nat
    • avoid overflow
  • Char
  • String
  • Bool
  • Int
  • primitive functions
• functions
  • function type signatures
  • termrs (e.g. function bodys)
  • Let bindings
  • Case expresssions
  • higher-order functions
• type aliases
  • simple aliases without arguments
  • parameterized aliases
• datatypes
  • polymorphic types / type variables
  • constructors/variants
  • PhantomData for unused type variables
    • add Phantom constructor only if needed
  • Infinite types (e.g. List)
  • more dependent/indexed types
• records
  • simple records
  • complex records
• imports (module-related)
  • private definitions (i.e. not pub for everything)
• Postulates
• FOREIGN pragmas
  • FFI with postulates
• Erasure (a.k.a. run-time irrelevance)
• Compile-time irrelevance
  • Prop universe
• test suite
  • golden files
  • CI
• Compiler instructions
  • COMPILE ignore
  • COMPILE const/static
  • COMPILE rename
  • COMPILE derive
  • Inlining
• interface
  • emacs mode?
  • TUI?
• Optional features
  • IO
  • Procedural code