Laurel parsing - #1

Draft

keyboardDrummer wants to merge 78 commits into

moreExamplesfrom

Commits on Dec 1, 2025

Improve elab-time performance of Lean terms generated by DDM. (#221)
joehendrix
authored
a47df62
Refactor SemanticEval to receive only one SemanticStore (#213)
aqjune-aws
authored
7d87684

Commits on Dec 2, 2025

Models for relevant regular expression operations (#218)

authored
dc17f40
Andrewmwells/pyanalyze tests (#249)
andrewmwells-amazon
authored
574e765

Commits on Dec 3, 2025

Add datatypes to `LContext` (#238)
joscoh
authored
7b6a572

Commits on Dec 4, 2025

Commits on Dec 5, 2025

Add all executables to default targets (#237)
vjjocius
authored
e1c5e2b
pyanalyze burndown (#252)
andrewmwells-amazon
authored
f9be351
Change `Imperative.Stmt` to remove `Block` mutual recursion (#216)

joscoh
and
andrewmwells-amazon
authored
6a647e4

Commits on Dec 9, 2025

Add Laurel grammar and transformation
keyboardDrummer
committed
f3bf3a5
refactoring
keyboardDrummer
committed
4589663
Fixes
keyboardDrummer
committed
037a7d1
Moved tests
keyboardDrummer
committed
1c9cfd1
Fix grammar test
keyboardDrummer
committed
3a3809c
Getting there
keyboardDrummer
committed
927b0bb
TestExamples test passes
keyboardDrummer
committed
faa49df
Refactoring
keyboardDrummer
committed
4481959
Fix
keyboardDrummer
committed
c600cf1
Support Datetime (#266)

aqjune-aws
and
andrewmwells-amazon
authored
9cef91e
Generalize reflexive transitive closure (#267)
joscoh
authored
94e1af3

Commits on Dec 10, 2025

Revert AdvancedMaps changes
keyboardDrummer
committed
25df923
Add missing license headers
keyboardDrummer
committed
3c933e5
Revert RealBitVector
keyboardDrummer
committed
f182891
Tweaks
keyboardDrummer
committed
5bc8abd
Save state
keyboardDrummer
committed
fe2a831
Refactoring
keyboardDrummer
committed
2cd178c
Refactoring
keyboardDrummer
committed
12946cf
Cleanup
keyboardDrummer
committed
b12d781
Merge branch 'main' into laurelParsing
keyboardDrummer
authored
75cc85f
Fix Laurel/TestGrammar
keyboardDrummer
committed
84235b4
Merge branch 'laurelParsing' of github.com:keyboardDrummer/Strata into laurelParsing
keyboardDrummer
committed
cffb991
Fix alpha equivalence for Boogie programs (#265)
joscoh
authored
a3e0856

Commits on Dec 11, 2025

Commits on Dec 15, 2025

Merge remote-tracking branch 'origin' into laurelParsing
keyboardDrummer
committed
77aa05a
Move back Boogie examples
keyboardDrummer
committed
fbe4de5
Remove white line
keyboardDrummer
committed
e827d76
Remove duplication
keyboardDrummer
committed
79fbeb9
Fix test
keyboardDrummer
committed
0ea1bbb
Bump lean-toolchain to v4.25.2 (#273)
joehendrix
authored
3160a8c

Commits on Dec 16, 2025

Merge remote-tracking branch 'origin/main' into laurelParsing
keyboardDrummer
committed
a496a14
Fix after merge
keyboardDrummer
committed
245f7ad
Fix
keyboardDrummer
committed
95bb904
Fix oops
keyboardDrummer
committed
1d19b86
Fix warning
keyboardDrummer
committed
125bf17
Add DDM unwrap metadata (#261)

MikaelMayer
and
andrewmwells-amazon
authored
1646019
Turn Strata Python bindings into native namespace package (#276)
ssomayyajula
authored
c27615e
Support for classes (#270)

andrewmwells-amazon
and
aqjune-aws
authored
52c0eb0

Commits on Dec 17, 2025

Fix pyAnalyze CI (#278)
andrewmwells-amazon
authored
872a746
Hide counterexamples when verbose flag is false (#271)

vjjocius
and
shigoel
authored
492cd53
Boogie lexpr gen + generator bug fix (#272)

authored
30d59b1
Undo bad changes
keyboardDrummer
committed
9efa44a
Move examples from `Strata` to `StrataTest` to reduce build time (#274)

keyboardDrummer
and
aqjune-aws
authored
e328a48
feat(DDM): Add Bool support to DDM core (#255)

MikaelMayer
and
andrewmwells-amazon
authored
5ce8f20

Commits on Dec 18, 2025

Merge branch 'main' into laurelParsing
keyboardDrummer
authored
eae1536
Merge remote-tracking branch 'origin/main' into laurelParsing
keyboardDrummer
committed
7e16741
Merge branch 'laurelParsing' of github.com:keyboardDrummer/Strata into laurelParsing
keyboardDrummer
committed
f711bdc
Fix
keyboardDrummer
committed
b3c66a3
Bump to v4.26.0 (#281)
joehendrix
authored
d5d3a57
Switch Z3 timeout from soft to hard (#284)
andrewmwells-amazon
authored
1e1be4c
Add more concrete evaluators for bit-vector operations in Boogie (#275)

authored
197dddb
PyAnalyze While and FloorDiv (#283)
andrewmwells-amazon
authored
ee0f0f9
Strata language definition document (#186)

authored
22e10d7
Z3 -T param takes seconds (#286)

andrewmwells-amazon
and
shigoel
authored
dca53ec

Commits on Dec 19, 2025

Move file
keyboardDrummer
committed
c32a3d5
Merge remote-tracking branch 'origin/main' into laurelParsing
keyboardDrummer
committed
44c4082
Fixes
keyboardDrummer
committed
d803b56
Extend PythonToBoogie to use signatures database (#279)

joehendrix
and
shigoel
authored
b0de596

Commits on Dec 22, 2025

Commits on Dec 23, 2025

Fix TestGrammar
keyboardDrummer
committed
9856651
Merge branch 'main' into laurelParsing
keyboardDrummer
authored
f6dfea9
feat(DDM): Support dots in identifiers (#293)
MikaelMayer
authored
e26c206

Commits on Dec 24, 2025

Merge branch 'main' into laurelParsing
shigoel
authored
f8a9a67