This PR implements some important refactoring. At a high level, this PR gets rid of many legacy code and use a set of generic IRs which allows greater code sharing (thus reduced codebase size).
Fully remove the old NormExpr and NormAction, use the new CoreIR instead.
Generalizes front-end IR (e.g., Rule) and backend-IR (e.g., CoreRule) to be parametric over the head and leaf symbols.
Add type resolution so that typechecking returns a type-annotated expression.
Replace the type checker for actions to use the constraint-based one.
Refactor the backend Action->Program compiler so that it no longer does unnecessary type checking and works with CoreAction instead of Action.
desugar and resugar flags are replaced with a --show desugared-egglog flag, which prints an egglog program produced by the desugaring phase.
The current compilation workflow is
Command -[desugar]-> NCommand: does some lightweight desugaring, e.g., turns a function into a relation
Rule in NCommand -[lower]-> CoreRule: lowering to CoreRule for typechecking
(Rule, CoreRule) -[typecheck]-> ResolvedRule: ResolvedRule is a Rule with all its function symbols and variables type annotated.
Other planned transformations (e.g. proofs) over ResolvedRule
This PR implements some important refactoring. At a high level, this PR gets rid of many legacy code and use a set of generic IRs which allows greater code sharing (thus reduced codebase size).
NormExprandNormAction, use the new CoreIR instead.Rule) and backend-IR (e.g.,CoreRule) to be parametric over the head and leaf symbols.Action->Programcompiler so that it no longer does unnecessary type checking and works withCoreActioninstead ofAction.desugarandresugarflags are replaced with a--show desugared-egglogflag, which prints an egglog program produced by the desugaring phase.The current compilation workflow is
Command -[desugar]-> NCommand: does some lightweight desugaring, e.g., turns a function into a relationRule in NCommand -[lower]-> CoreRule: lowering toCoreRulefor typechecking(Rule, CoreRule) -[typecheck]-> ResolvedRule:ResolvedRuleis aRulewith all its function symbols and variables type annotated.ResolvedRule -[lower]-> ResolvedCoreRuleResolvedCoreRule -[compilation]-> ProgramFixes #80, fixes #113, fixes #196.