Normalize all n-ary operators in the RARE rewrite engine#125
Open
caotic123 wants to merge 2 commits into
Open
Conversation
added 2 commits
June 9, 2026 13:50
Change `Sort::RareList` from a unit variant to `Sort::RareList(Rc<Term>)` so that a rare list carries the sort of its elements. This lets sort computation, sort comparison, substitution, and the parser correctly look through a rare list to its element sort (e.g. for bitvector width inference, array select/store, polymorphism checks, and `:list` parameters in RARE rules). Also splice many-term reconstruction results into operator arguments in `reconstruct_meta_terms`, which is required to expand `:list` arguments when reconstructing a rewritten term. Adds the `bv-concat-extract-merge` example (rule with bitvector `:list` parameters) as a regression test and fixture.
Extend the meta-term rewrite engine to normalize every n-ary (right-assoc-nil) operator that carcara represents, not just `and`/`or`: arithmetic (`+`, `*`), strings (`str.++`), regular expressions (`re.++`, `re.union`, `re.inter`), and bitvectors (`bvand`, `bvor`, `bvxor`, `bvadd`, `bvmul`, `concat`). For each operator `get_rules` now carries, in this order, a flatten rule `(Op (RareList ..x..)) ~> (Op x)`, a singleton rule `(Op x) ~> x`, and — for operators whose nil terminator is a static term — an empty rule `(Op) ~> <nil>`. Flatten must precede singleton: `check_rewrites` returns the first matching rule and `(Op x)` also matches a single rare-list argument, so flatten-first is what splices a list instead of collapsing it. Bitvector nil terminators are width-dependent and cannot be written as static constants, so they are synthesized in `bv_nil_if_empty`: when an n-ary bitvector operator's argument list becomes empty, recover the operand width and build the nil (0 for bvadd/bvor/bvxor, all-ones for bvand, 1 for bvmul, the zero-width empty bitvector for concat). When the width is genuinely unrecoverable (a bare operator with no operands) the term is left un-normalized rather than guessing. This builds on the parameterized `Sort::RareList` change: without it, constructing a bitvector term that holds a rare-list argument fails sort computation. Adds engine unit tests for the arithmetic/string/regex/bitvector flatten, singleton, empty, and nil-synthesis paths, and end-to-end `rare_rewrite` checker tests for an arithmetic and a bitvector `:list` rule.
bpandreotti
requested changes
Jun 17, 2026
bpandreotti
left a comment
bpandreotti
left a comment
Collaborator
There was a problem hiding this comment.
Again, a few merge conflicts and formatting stuff. Otherwise, looks good to me.
Comment on lines
-12
to
-13
| build_equation!((Or) ~> true), | ||
| build_equation!((And) ~> false), |
Collaborator
There was a problem hiding this comment.
Why were these two nil cases removed? From the comment above, I assumed they were required.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Broadens RARE meta-term normalization from
and/orto every n-ary (right-assoc-nil) operator carcara represents.What
get_rules()now carries, per operator and in this order, a flatten rule(Op (RareList ..x..)) ~> (Op x), a singleton rule(Op x) ~> x, and — where the nil terminator is a static term — an empty rule(Op) ~> <nil>:+(nil0),*(nil1)str.++(nil"")re.++,re.union(nilre.none),re.inter(nilre.all)bvand,bvor,bvxor,bvadd,bvmul,concatFlatten must precede singleton —
check_rewritesreturns the first match and(Op x)also matches a single rare-list argument, so flatten-first is what splices a list instead of collapsing it.Width-dependent bitvector nils
Bitvector nil terminators depend on the operand width and can't be static constants. They're synthesized in
bv_nil_if_empty: when an n-ary bitvector op's argument list becomes empty, recover the width and build the nil (0for bvadd/bvor/bvxor, all-ones for bvand,1for bvmul, the zero-width empty bitvector for concat). When the width is genuinely unrecoverable (a bare operator with no operands), the term is left un-normalized rather than guessing.Known limitations
re.++empty case omitted (its nil(str.to_re "")is not a zero-arg term; flatten + singleton suffice).(+)/(*)empties emit integer0/1; Real-sorted empties would want0.0/1.0(only matters in the all-empty degenerate case).set.*/Tupleare out of scope (absent from carcara'sOperatorenum).