Add polymorphic functions to DDM and Strata.Boogie #321
Conversation
Add new attribute "inline_if_val" that inlines a function only if all its arguments are canonical values
Improve type handling in SMTEncoder, need to recursively check constructor arguments
Test fails for now, need toposort of datatypes
Provides generic function mechanism with datatypes
joscoh
requested review from
a team,
MikaelMayer,
andrewmwells-amazon,
aqjune-aws,
atomb,
joehendrix and
shigoel
as code owners
| @[declareFn(name, b, r)] | ||
| op command_fndecl (name : Ident, | ||
| typeArgs : Option TypeArgs, | ||
| @[scopeTypeVars(typeArgs)] b : Bindings, |
There was a problem hiding this comment.
How does this determine the identifiers that typeArgs introduces? Is every identifier subterm in typeArgs an identifier?
There was a problem hiding this comment.
I'm kind of wondering if we should have declareTypeVars that introduces type variables and then keep the current scope construct for extending the type context. With the current design, it's unclear to me what scopeTypeVars does if typeArgs also declared variables.
| | bvar (ann : α) (index : Nat) | ||
| /-- A polymorphic type variable (universally quantified). | ||
| Used for polymorphic function type parameters -/ | ||
| | tvar (ann : α) (name : String) |
There was a problem hiding this comment.
Why use String for type variable names rather than deBrujin indices as in bvar? It seems like bvar could refer to either a type variable or "expression" variable.
joehendrix
left a comment
joehendrix
left a comment
There was a problem hiding this comment.
This looks like a good start. I left a few comments; I'd also like to see a few DDM tests that used a simple test dialect rather than Boogie.
3 participants
Description of changes:
This PR extends the DDM with a
.tvarconstruct that allows type variables to be used in function declarations. The DDM does not perform typechecking or unification for type variables; it leaves this to the dialect-specific typechecker or type inference algorithm (Lambda in this case). This PR also extends the Boogie DDM with polymorphic definitions and contains Boogie test cases, both for polymorphic functions directly and for polymorphic datatypes which implicitly define functions.@thanhnguyen-aws
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.