Conversation
…to remy/pureProcedures
| -- Collect ALL errors from both functions and procedures before deciding whether to fail | ||
| let allErrors := pureErrors ++ procDiags ++ constantsState.diagnostics | ||
| -- Collect ALL errors from both functions, procedures, and resolution before deciding whether to fail | ||
| let allErrors := -- resolutionDiags.toList ++ |
There was a problem hiding this comment.
_resolutionDiags is not included here — the addition is commented out. Is that intentional?
There was a problem hiding this comment.
Added a clarifying comment
joscoh
left a comment
joscoh
left a comment
There was a problem hiding this comment.
Do you have any tests for these changes (e.g. ensuring resolution works, Laurel programs with datatypes)?
Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
Outdated
Show resolved
Hide resolved
| op composite (name: Ident, extending: Option OptionalExtends, fields: Seq Field): Composite => "composite " name extending "{" fields "}"; | ||
|
|
||
| // Datatype definitions | ||
| category DatatypeConstructorArg; |
There was a problem hiding this comment.
This will not allow recursive type definitions, right?
There was a problem hiding this comment.
Grammar wise I think it would be allowed, but it might fail later in the pipeline, depending on whether Core datatypes support this or not.
There was a problem hiding this comment.
Core datatypes support this. The Laurel grammar does not right now I believe because the type definition is not in scope in the constructor types. We use the @[scopeDatatype] annotation for this in the Core grammar to handle this. I am not saying that Laurel should or not support this, just wanted to let you know that I do not believe this is supported right now.
There was a problem hiding this comment.
I see, thanks.
|
|
||
|
|
||
|
|
||
| datatype Workaround {} |
There was a problem hiding this comment.
The Workaround datatype can be deleted — I removed it locally and lake build strata:exe completed successfully (368/368 jobs, no errors).strata:exe` completed successfully (368/368 jobs, no errors).
Scratch that I see the test failure. I'll investigate further for a fix, but don't consider this blocking obviously.
4 participants
Changes
Instead of redefining how to do name resolution in each phase in the translation from Laurel to Core, define resolution once in a single phase. Currently resolution is done again after each phase. This introduces partially duplicated work but we expect to reduce that in the future using caching.
The Python through Laurel pipeline currently can not resolve each reference because it adds some prelude definitions, that are referenced by the generated code, only at the Core level instead of at the Laurel level. To still enable the Python through Laurel pipeline to work, I had to turn off reporting of resolution errors. I'll resolve that in a follow-up PR.
For Laurel tests, this PR includes changes to ensure that the program resolves without errors after each phase:
typeTag: TypeTagfield of the composite datatype is only added to that datatype during the typeHierarchy phase, since that's the phase whereTypeTagis defined.const,selectandupdateare now added as part ofCoreDefinitionsForLaurel.lean, as Laurel functions with an "External" body, meaning they're ignored during the translation to Core. This way, references to them can be resolved during resolution.HeapParameterization, fields for composite type definitions are deleted, so their names don't conflict with the constructors of the generatedFielddatatypeTesting
Refactoring. No changes to existing tests. I will follow-up with first removing the hacks, and then adding tests containing name conflicts that'll make use of this new resolution phase.