Metatheory.jl is a general purpose term rewriting, metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern matching features. The core features of Metatheory.jl are a powerful rewrite rule definition language, a vast library of functional combinators for classical term rewriting and an e-graph rewriting, a fresh approach to term rewriting achieved through an equality saturation algorithm. Metatheory.jl can manipulate any kind of Julia symbolic expression type, as long as it satisfies the TermInterface.jl.
Features
- An eDSL (domain specific language) to define different kinds of symbolic rewrite rules
- A classical rewriting backend, derived from the SymbolicUtils.jl pattern matcher, supporting associative-commutative rules
- A flexible library of rewriter combinators
- An e-graph rewriting (equality saturation) backend and pattern matcher, based on the egg library
- It is based on the pattern matcher in the SICM book
- Reduce the amount of user effort required to achieve optimization tasks and equational reasoning
Project Samples
