Add metadata to more places in Laurel #396
Conversation
keyboardDrummer
requested review from
andrewmwells-amazon,
atomb and
joscoh
and removed request for
atomb
|
@atomb the codebase contains many pieces like |
keyboardDrummer
force-pushed
the
laurelMetadata
branch
from
a2402ca to
cd14832
Compare
keyboardDrummer
requested review from
MikaelMayer
and removed request for
andrewmwells-amazon
Strata/Languages/Laurel/Laurel.lean
Outdated
| md : Imperative.MetaData Core.Expression | ||
| deriving Repr | ||
|
|
||
| structure StmtExprMd where |
There was a problem hiding this comment.
I would recommend creating one structure that adds metadata to any type like the DDM does, i.e.
structure WithMetadata (t: T) where
val: T
md: Imperative.Metadata Core.Expression
deriving Repr
It will make it easier to generalize down the road. You can always make StmtExprMd an abbreviation of it.
I would even have you consider reusing DDM's Ann that is fully parametric in the metadata and has the same purpose. It has also methods to replace the metadata.
There was a problem hiding this comment.
Applied the change
| procedure foo(c: Container, d: Container) returns (r: int) | ||
| requires c != d && d#intValue == 1 | ||
| ensures d#intValue == 3 |
There was a problem hiding this comment.
Interesting, there are no modifies clauses? Nothing to indicate what the procedure can or cannot change?
There was a problem hiding this comment.
in a subsequent PR that adds support for modifies clauses, this generates an error, but only because there is an ensures clause so the procedure is opaque.
Add HighTypeMd.sizeOf_val_lt lemma and use it to prove translateType terminates. The remaining partial defs recurse through List StmtExprMd which requires the same sizeOf bridging pattern that is a known issue across the codebase (see PR #396).
| - `valueUsed`: whether the result value of this expression is used (affects optimization of heap-writing calls) | ||
| -/ | ||
| def heapTransformExpr (heapVar : Identifier) (expr : StmtExpr) (valueUsed : Bool := true) : TransformM StmtExpr := | ||
| partial def heapTransformExpr (heapVar : Identifier) (expr : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := |
There was a problem hiding this comment.
Would prefer not to make things partial unless needed. Is this because it is trickier with the nested record structure for metadata?
|
|
||
| Example 1: | ||
| `composite Some<T> { value: T }` | ||
| `composite SomeT> { value: T }` |
There was a problem hiding this comment.
Not sure why this was changed
|
|
||
| def formatHighType : HighType → Format | ||
| private theorem HighTypeMd.sizeOf_val_lt (e : HighTypeMd) : sizeOf e.val < sizeOf e := by | ||
| cases e |
There was a problem hiding this comment.
Does cases e<;> simp_wf<;> omega work? (the current proof is fine, just suggesting a potentially shorter one)
| -/ | ||
| def translateType (ty : HighType) : LMonoTy := | ||
| match ty with | ||
| partial def translateType (ty : HighTypeMd) : LMonoTy := |
There was a problem hiding this comment.
termination should be provable here
3 participants
Changes
Procedure.CheckTesting
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.