Update typechecking to construct type annoted AST #504
Conversation
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
john-h-kastner-aws
force-pushed
the
type_annot_ast
branch
from
f795321 to
be6459f
Compare
Signed-off-by: John Kastner <jkastner@amazon.com>
john-h-kastner-aws
force-pushed
the
type_annot_ast
branch
from
be6459f to
8e97a19
Compare
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
john-h-kastner-aws
force-pushed
the
type_annot_ast
branch
from
8e97a19 to
d94871c
Compare
| @@ -167,7 +178,7 @@ def typeOfInₛ (ety₁ ety₂ : EntityType) (x₁ x₂ : Expr) (env : Environme | |||
| then .anyBool | |||
| else .ff | |||
|
|
|||
| def typeOfHasTag (ety : EntityType) (x : Expr) (t : Expr) (c : Capabilities) (env : Environment) : ResultType := | |||
| def typeOfHasTag (ety : EntityType) (x : Expr) (t : Expr) (c : Capabilities) (env : Environment) : Except TypeError (CedarType × Capabilities) := | |||
There was a problem hiding this comment.
I'm sad that typeOfHasTag and typeOfGetTag don't return ResultType like other typeOf functions :D
(I see below why it's done, but the asymmetry makes me sad.)
There was a problem hiding this comment.
I was thinking about doing some renaming later. Maybe changing the alias for Except TypeError (CedarType × Capabilities) to ResultTypedExpr and keeping ResultType as Except TypeError (CedarType × Capabilities) so things look a bit more symmetric at these definitions. I like small diffs though, and that kind of blows it up.
| | .entity ety => | ||
| match env.ets.attrs? ety with | ||
| | .some rty => hasAttrInRecord rty x a c false | ||
| | .some rty => do | ||
| let (ty', c) ← hasAttrInRecord rty x a c false |
There was a problem hiding this comment.
This pattern repeats a lot in the code:
do
let (ty, c) ← ...
ok ty c
I might be tempted to hide it in a helper function. If we had a variant for ok that accepts a pair rather than two arguments, we could rewrite these as just one line, e.g.:
do ok (← hasAttrInRecord rty x a c false)
There was a problem hiding this comment.
I tried to do something clever here but Lean's handling of default arguments was getting in the way. Might take another look
There was a problem hiding this comment.
Yeah, that's fair. We can do a second pass after this one is merged.
(It all looks good / correct to me. These are just nits.)
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
Signed-off-by: John Kastner <jkastner@amazon.com>
|
Merging this in it's current state. I'll follow up with at least another smaller PR to tidy some things up |
Issue #, if available:
Adds a new
TypedExprtype which is constructed by the updated typechecking procedure and updates the soundness proof for these changes.Description of changes: