girafe
v1.1.0
Published
Term Rewriting Systems infrastructure
Downloads
22
Readme
Girafe
Term Rewriting Systems infrastructure
Girafe provides a set of tools based on a minimal term rewriting systems language that can be interpreted or compiled to various targets.
See the examples/ folder for small demos.
Multiple preprocessors and transformations can be applied to support laziness, imports, currying, non-linearity etc.. see src/Compiler/Passes/
Installing
$ npm install -g girafe
Compiling
Girafe programs can be compiled to javascript, ocaml or haskell using:
$ grf src.grf out.ext js/ocaml/haskell
Or interpreted using:
$ grf src.grf [query]
Use Cases
- Target language for functional (lazy or eager) programming languages (see croco)
- Symbolic computation
- Automated theorem proving
- Abstract data type specifications
Todo
- [x] Use a necessity heuristic when building decision-trees
- [x] Simulate lazy rewriting correctly
- [ ] Add targets (c/rust/wasm)
- [ ] Confluence checks
- [x] Tail call elimination
- [ ] Simple optimizations
References
- Maranget, Luc (2008) Compiling Pattern Matching to Good Decision Trees
- Martelli & Montanari (1982) An Efficient Unification Algorithm
- Fokkink, Wan & Kamperman, Jasper & Walters, Pum. (1999). Lazy Rewriting on Eager Machinery. ACM Transactions on Programming Languages and Systems. 22. 10.1145/345099.345102.
- Klop, jan willem. (2000). Term Rewriting Systems.