Add polymorphic functions to DDM and Strata.Boogie#321

Merged

shigoel merged 90 commits intomainfrom

josh/ddm-poly-2

Jan 28, 2026

Commits on Nov 25, 2025

Add tester functions and tests
Josh Cohen
committed
Add destructors
Josh Cohen
committed

Commits on Nov 26, 2025

Adding datatypes to Boogie AST, in progress
Josh Cohen
committed
Add datatypes to LContext
Josh Cohen
committed
Add datatype to Boogie typing and merge LContext change
Josh Cohen
committed

Commits on Nov 28, 2025

Add datatypes to SMTContext and thread through LMonoTy.toSMTType
Josh Cohen
committed
Add declare-datatypes and derived functions through verif pipeline
Josh Cohen
committed
Store generated ADT functions in map
Josh Cohen
committed
Fix Boogie datatype tests
Josh Cohen
committed

Commits on Dec 1, 2025

Minor cleanup
Josh Cohen
committed
Improve tests and remove some useless code
Josh Cohen
committed
Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed
A few formatting fixes
Josh Cohen
committed

Commits on Dec 3, 2025

Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed

Commits on Dec 4, 2025

Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed
Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed

Commits on Dec 24, 2025

Allow different names for testers/destructors, change Boogie prelude with datatypes
Josh Cohen
committed
Fix bug with datatypes using sorts or nested types in constructors
Josh Cohen
committed
Add test case for datatype dependencies
Josh Cohen
committed
Add topological sorting for datatype dependencies and tests
Josh Cohen
committed
Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed
Formatting changes from comments
Josh Cohen
committed
Minor formatting fixes
Josh Cohen
committed

Commits on Dec 26, 2025

Formatting fixes and limit comment length in TypeFactory.lean
Josh Cohen
committed
Fix formatting in SMT datatype tests
Josh Cohen
committed

Commits on Dec 30, 2025

Merge branch 'main' into josh/declare-datatype
Josh Cohen
committed
New version of datatypes in Boogie with tests
Josh Cohen
committed
Add Other datatype dialect and fix references to Boogie in Ast.lean
Josh Cohen
committed

Commits on Dec 31, 2025

Change BoogiePrelude to use datatypes
Josh Cohen
committed
Merge branch 'main' into josh/declare-datatype
shigoel
authored
Merge branch 'main' into concrete-ast-ddm-2
Josh Cohen
committed
Add default tester names and better comments for datatype tests
Josh Cohen
committed
Merge branch 'josh/declare-datatype' into concrete-ast-ddm-2
Josh Cohen
committed
Add missing file
Josh Cohen
committed
Add constructor annotations
Josh Cohen
committed
Add field list annotations, remove hard-coded names
Josh Cohen
committed
Clean up some Translate code to reduce duplication
Josh Cohen
committed
Add documentation to new AST declarations
Josh Cohen
committed
Move parts of datatype AST and add datatype docs
Josh Cohen
committed
Remove Boogie Minimal example
Josh Cohen
committed

Commits on Jan 2, 2026

Clean up code and documentation
Josh Cohen
committed
Fix BoogiePrelude destructor names
Josh Cohen
committed
Clean up Boogie Parse.lean
Josh Cohen
committed
Make None datatype in BoogiePrelude for computation
Josh Cohen
committed
Update expected output with newly passing tests
Josh Cohen
committed
Remove perConstructorField and fieldIndex
Josh Cohen
committed

Commits on Jan 6, 2026

Trying again incrementally - add tvar
Josh Cohen
committed
Poly implementation v2
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed

Commits on Jan 7, 2026

Fix minor bugs and add tests for polymorphic DDM definitions
Josh Cohen
committed
Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Add polymorphic datatype support with tests
Josh Cohen
committed
Update Python Boogie prelude with polymorphic type
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Merge branch 'josh/concrete-ast-ddm-2' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 8, 2026

Remove unecessary scope annotations from fields
Josh Cohen
committed
Update datatype documentation, add to DDM manual
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Add small clarification about fields
Josh Cohen
committed

Commits on Jan 9, 2026

Remove special handling for fields, replace with generic Bindings
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed

Commits on Jan 12, 2026

Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Merge branch 'josh/concrete-ast-ddm-2' into josh/ddm-poly-2
Josh Cohen
committed
Fix error message on tests
Josh Cohen
committed
Clean up comments
Josh Cohen
committed
Remove unecessary tests and test comments in polymorphic tests
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Merge branch 'josh/concrete-ast-ddm-2' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 13, 2026

Update Verso documentation
Josh Cohen
committed
Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Update Python expected README
Josh Cohen
committed
Merge branch 'main' into josh/concrete-ast-ddm-2
Josh Cohen
committed
Merge branch 'josh/concrete-ast-ddm-2' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 14, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Uncomment test
Josh Cohen
committed
Merge branch 'main' into josh/ddm-poly-2
joscoh
authored
Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 15, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Update test output
Josh Cohen
committed

Commits on Jan 22, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed
Remove @[scopeTypeVars], change to separate @[declareTypeVars] and @[scope]
Josh Cohen
committed
Add minimal dialect with type variables
Josh Cohen
committed
Handle type variables one-by-one (like Binding), not at once
Josh Cohen
committed
Fix some things that shouldn't have changed
Josh Cohen
committed

Commits on Jan 23, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 24, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed

Commits on Jan 27, 2026

Merge branch 'main' into josh/ddm-poly-2
Josh Cohen
committed