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

1. Maranget, Luc (2008) Compiling Pattern Matching to Good Decision Trees
2. Martelli & Montanari (1982) An Efficient Unification Algorithm
3. Fokkink, Wan & Kamperman, Jasper & Walters, Pum. (1999). Lazy Rewriting on Eager Machinery. ACM Transactions on Programming Languages and Systems. 22. 10.1145/345099.345102.
4. Klop, jan willem. (2000). Term Rewriting Systems.