This development is an experiment with the following goals:
- Adopt smalltt and related techniques into the cubical world.
- Show how various OCaml packages of ours fit together.
- Write natural grammars without neccesarily conforming to LR(k).
- Use lots of Unicode emojis.
opam pin git+https://github.com/RedPRL/bantorra
opam pin git+https://github.com/RedPRL/algaett
cat tests/example.ag
algaett tests/example.agThe last line should not have an output, which means it type checks!
The core NbE algorithm closely follows András Kovács’s smalltt. Here are some notable differences:
- We intentionally do not implement unification.
- The universe itself (as a term) is not inferable, which means that the checking might have to be redone with the type unfolded.
The type inference from the universe 🌌 will fail, and then the type checking will be redone with 😄 unfolded to 🌌 🆙 1️⃣.
📌 😄 : 🌌 🆙 2️⃣ 👉 🌌 🆙 1️⃣ 📌 _ 👉 🌌 : 😄 - The conversion checker is generalized to handle subtyping generated by cumulativity.
- algaeff: reusable effects-based components
- asai: error messages (not actively used yet)
- bantorra: unit resolution (not actively used yet)
- bwd: backward lists
- mugen: universe levels
- yuujinchou: namespaces and name modifier
We are using the Earley’s parsing algorithm which can handle all context-free grammars.