Skip to content

Latest commit

 

History

History
19 lines (13 loc) · 2.21 KB

README.md

File metadata and controls

19 lines (13 loc) · 2.21 KB

juniper-rs

This is the set of Rust crates representing the Juniper library. The purpose of each of the crates is as follows:

  • lean_parse: a set of data definitions for core Lean types used for serializing and deserializing Lean type information. (Note that these definitions are not fully correct, but are correct in-scope).
  • juniper_math_expression: the definition for MathExpression (Juniper's egg Language), JuniperBigRational (a simple wrapper for parsing num::BigRational), and ConstantFold (Juniper's egg Analysis for eliminating constants).
  • juniper_lean_to_rewrite: an opinionated LeanExpr to MathExpression transpiler.
  • juniper_lib: the front-facing API for utilizing Juniper. Exposes an automatically generated list of Rewrites obtained from transpiling JuniperLean results, as well as using a build script to automatically re-elaborate JuniperLean when changes are detected.
  • juniper_repl: a simple command line tool for evaluating expressions using juniper_lib.

Big picture, the Rust system works by interpreting the json representing the set of Lean equality types, transpiling those types to rewriting rules, and creating an Egg Runner using those rules.

Transpiling

Going between LeanExprs and MathExpressions happens in 2 stages:

  • LeanExpr to the intermediate representation
  • the intermediate representation to MathExpression

I chose to use an intermediate representation because LeanExpr and MathExpression are very different kinds of syntax tree. Expressions from Lean use a new function application for every level of argument (which creates a much more concise language definition), while MathExpressions use a single node for every operator and atom (which is much more expressive). The intermediate representation I created is basically a tree with single nodes for operators and atoms, but with 1:1 optional fields for LeanExpr, so that the tree can essentially be filled in as-you-go instead of all at once. Then, once the tree is complete, it can be easily converted into a MathExpression in a single shot.