chore: refactor Comb parser and remove unnecessary types

[luisacicolini]

This PR refactors the Comb parser according to #1208, removes unnecessary types (so that everything is a bitvector operation) and removes support for concat, since it can't be supported without HVector/hList/similar.

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and leanSAT failed theorem 3 in file gexact_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 5 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 51 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 53 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file gsremhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 4 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 9 in file gapinthsub_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 1 in file gapinthrem2_proof.lean
bitwuzla proved and leanSAT failed theorem 15 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 38 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 2 in file gsdivhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 1 in file gadd4_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2008h02h23hMulSub_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2010h11h23hDistributed_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 3 in file gapinthdiv2_proof.lean
bitwuzla proved and leanSAT failed theorem 14 in file gshlhfactor_proof.lean
bitwuzla proved and leanSAT failed theorem 21 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 22 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 23 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 24 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 13 in file gsubhxorhcmp_proof.lean
leanSAT and Bitwuzla solved: 7930
leanSAT and Bitwuzla provided 8 counterexamples
leanSAT and Bitwuzla both failed on 15 theorems
leanSAT failed and Bitwuzla succeeded on 21 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 78
ran rg 'Bitwuzla failed' | wc -l, expected 15, found 0, FAIL
ran rg 'LeanSAT failed' | wc -l, expected 36, found 0, FAIL
ran rg 'LeanSAT provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'Bitwuzla provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'LeanSAT proved' | wc -l, expected 7930, found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, expected 7951, found 0, FAIL
error (kernel) deep recursion detected was raised 25 times
error The SAT solver timed out while solving the problem. was raised 38 times
error The SMT solver timed out while solving the problem. was raised 15 times

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and leanSAT failed theorem 3 in file gexact_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 5 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 51 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 53 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file gsremhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 4 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 9 in file gapinthsub_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 1 in file gapinthrem2_proof.lean
bitwuzla proved and leanSAT failed theorem 15 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 38 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 2 in file gsdivhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 1 in file gadd4_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2008h02h23hMulSub_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2010h11h23hDistributed_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 3 in file gapinthdiv2_proof.lean
bitwuzla proved and leanSAT failed theorem 14 in file gshlhfactor_proof.lean
bitwuzla proved and leanSAT failed theorem 21 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 22 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 23 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 24 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 13 in file gsubhxorhcmp_proof.lean
leanSAT and Bitwuzla solved: 7930
leanSAT and Bitwuzla provided 8 counterexamples
leanSAT and Bitwuzla both failed on 15 theorems
leanSAT failed and Bitwuzla succeeded on 21 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 78
ran rg 'Bitwuzla failed' | wc -l, expected 15, found 0, FAIL
ran rg 'LeanSAT failed' | wc -l, expected 36, found 0, FAIL
ran rg 'LeanSAT provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'Bitwuzla provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'LeanSAT proved' | wc -l, expected 7930, found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, expected 7951, found 0, FAIL
error (kernel) deep recursion detected was raised 25 times
error The SAT solver timed out while solving the problem. was raised 38 times
error The SMT solver timed out while solving the problem. was raised 15 times

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and leanSAT failed theorem 3 in file gexact_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 5 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 51 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 53 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file gsremhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 4 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 9 in file gapinthsub_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 1 in file gapinthrem2_proof.lean
bitwuzla proved and leanSAT failed theorem 15 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 38 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 2 in file gsdivhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 1 in file gadd4_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2008h02h23hMulSub_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2010h11h23hDistributed_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 3 in file gapinthdiv2_proof.lean
bitwuzla proved and leanSAT failed theorem 14 in file gshlhfactor_proof.lean
bitwuzla proved and leanSAT failed theorem 21 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 22 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 23 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 24 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 13 in file gsubhxorhcmp_proof.lean
leanSAT and Bitwuzla solved: 7930
leanSAT and Bitwuzla provided 8 counterexamples
leanSAT and Bitwuzla both failed on 15 theorems
leanSAT failed and Bitwuzla succeeded on 21 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 78
ran rg 'Bitwuzla failed' | wc -l, expected 15, found 0, FAIL
ran rg 'LeanSAT failed' | wc -l, expected 36, found 0, FAIL
ran rg 'LeanSAT provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'Bitwuzla provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'LeanSAT proved' | wc -l, expected 7930, found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, expected 7951, found 0, FAIL
error (kernel) deep recursion detected was raised 25 times
error The SAT solver timed out while solving the problem. was raised 38 times
error The SMT solver timed out while solving the problem. was raised 15 times

[alexkeizer]

despite setting ϕ to 0, I can't seem to remove the check on the mvar in MkTy, what am I missing?

Not sure, the code look like it'd ought to work. What error or you seeing?

I hacked a bit the arguments management for n-ary ops - I believe there are smoother ways to do that, could you please suggest how to do it better?

I left a suggestion

I would like to throw a more informative error for Comb.mux when the third arg is not .bitvec 1 (condition), since as of now a very generic type error is raised. My solution would be to nest a further match in the parser, which I believe is what we're trying to avoid with the new infrastructure. What's the best way to proceed?

Adding an extra match would be fine, I think. I left a suggestion with a rough outline of what I'd write!

[alexkeizer]

LGTM, modulo a error message phrasing

[github-actions]

Alive Statistics: 90 / 93 (3 failed)