Redefine Transformer := Expr → Option Expr as Translator := Expr → Option Term, with different semantics for the Option (see docstring). Translators call applyTranslators! directly instead of choosing to return e or e'. These changes give individual translators more control over their final output, in particular the ability to do type-aware literal emission.
Define BitVec and some operators.
Lowercase Term constructors to fit convention.
Use the new translation flexibility to implement translators for a fragment of the bitvector theory.
Move to a single-pass query builder in QueryBuilderM. This makes it easier to handle recursive translation of let-bindings in the local context, and to unify some of the duplicated defineFun functionality. It also made it easy to add a translation cache.
Closes #23.
Allow defining and declaring sorts.
Correctly handle curried binders.
This PR grew a bit brutally large so I will stop here and continue with more bitvector functionality in another. I will draw your attention to some of the more important changes using comments.
Transformer := Expr → Option ExprasTranslator := Expr → Option Term, with different semantics for theOption(see docstring). Translators callapplyTranslators!directly instead of choosing to returneore'. These changes give individual translators more control over their final output, in particular the ability to do type-aware literal emission.BitVecand some operators.Termconstructors to fit convention.QueryBuilderM. This makes it easier to handle recursive translation of let-bindings in the local context, and to unify some of the duplicated defineFun functionality. It also made it easy to add a translation cache.This PR grew a bit brutally large so I will stop here and continue with more bitvector functionality in another. I will draw your attention to some of the more important changes using comments.