Add mutually recursive types to Core concrete syntax #360
Conversation
No polymorphism yet Add forward declarations to DDM Add name to fvar to keep track within block Change Translate to translate to mutual blocks Add rose tree test
Fix poly+destructor names+mutual rec Add some more tests Temp - fix bug in SMT poly encoding
Make datatypes handle type arguments appropriately in parser Remove scoping workaroudn with local/declared Some formatting fixes
Factor out common functionality with mutual/single datatypes Require that mutual datatypes are forward declared
There was a problem hiding this comment.
These changes remind me that we should have a version number for the Strata encoding in Ion. There's already a version number for the Ion version used, but not for Strata itself. But that's not for this PR.
Strata/DDM/AST.lean
Outdated
| well-typed. The name field stores the original type name for lookup in | ||
| mutual blocks. -/ | ||
| | fvar (ann : α) (fvar : FreeVarIndex) (name : Option String) | ||
| (args : Array (TypeExprF α)) |
There was a problem hiding this comment.
I'd like to understand the name field better. What's the semantics? Can FreeVarIndex refer to multiple distinct constants that are identified by names now?
There was a problem hiding this comment.
The name field is used only for mutual blocks and should be ignored in all other cases. So for the case of a mutual block, the same fvar index refers to each element in the block, and they are distinguished by their names. For all other elements, a FreeVarIndex should refer to only a single constant, as before. If you have other recommendations I am open to them, this is a method to resolve the tricky issue that a single declaration needs to introduce multiple constants (that then need to be looked up) for mutual blocks.
There was a problem hiding this comment.
Could a declaration just introduce multiple free variables?
There was a problem hiding this comment.
I did try that, but ran into some problems. IIRC, I think the issue was that in Translate.lean, the mutual block needs to remain a single block (rather than multiple declarations) so there were some indices out of sync which caused problems. But I can try to make another attempt.
There was a problem hiding this comment.
I have pushed an alternate approach, keep track of the GlobalContext in TransState and using that for the name lookup. This avoids the need for names in free variables.
| mutual | ||
| datatype Tree { Node(val: int, children: Forest) }; | ||
| datatype Forest { FNil(), FCons(head: Tree, tail: Forest) }; | ||
| end; |
There was a problem hiding this comment.
I just want to confirm my intuition. Is the mutual block here just some syntax to show we can do something like this? If I understand correctly, don't think there are any checks that forward types are actually defined.
There was a problem hiding this comment.
Yes. There are no explicit checks that the forward types are defined, but since they do not introduce AST nodes, if they are declared without being defined, they cannot be used.
4 participants
Description of changes:
This PR adds a mechanism for mutually recursive types to the DDM and uses that to implement mutually recursive datatypes in Strata Core's concrete syntax.
This mechanism involves two changes to the DDM:
namefield to.fvar. This arises from the fact that there is no longer a 1-1 mapping between decls and global names, since a mutual block decl defines multiple names. This name field is used to look up the specific datatype in the mutual block inCore/DDM/Translate.lean.This PR also refactors some of the datatype handling in
Core/DDM/Translate.leanto abstract common functionality for single datatypes and mutual blocks, fixes an issue where datatype names were added to the context as type variables, and includes tests demonstrating the new DDM features inStrataTest/DDM/MutualDatatypes.leanand tests implementing the full verification pipeline inStrataTest/Languages/Core/Examples/MutualDatatypes.lean.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.