-
Notifications
You must be signed in to change notification settings - Fork 17
/
Copy pathTypedExpr.lean
156 lines (138 loc) · 6.91 KB
/
TypedExpr.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
/-
Copyright Cedar Contributors
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Cedar.Spec
import Cedar.Validation.Types
/-!
This file defines a type annotated version of the Cedar AST
-/
namespace Cedar.Validation
open Cedar.Data
open Cedar.Spec
/--
A type annotated Cedar AST. This should have exactly the same variants as the
unannotated `Expr` data type, but each variant carries an additional `ty` that
stores the type of the expression.
-/
inductive TypedExpr where
| lit (p : Prim) (ty : CedarType)
| var (v : Var) (ty : CedarType)
| ite (cond : TypedExpr) (thenExpr : TypedExpr) (elseExpr : TypedExpr) (ty : CedarType)
| and (a : TypedExpr) (b : TypedExpr) (ty : CedarType)
| or (a : TypedExpr) (b : TypedExpr) (ty : CedarType)
| unaryApp (op : UnaryOp) (expr : TypedExpr) (ty : CedarType)
| binaryApp (op : BinaryOp) (a : TypedExpr) (b : TypedExpr) (ty : CedarType)
| getAttr (expr : TypedExpr) (attr : Attr) (ty : CedarType)
| hasAttr (expr : TypedExpr) (attr : Attr) (ty : CedarType)
| set (ls : List TypedExpr) (ty : CedarType)
| record (map : List (Attr × TypedExpr)) (ty : CedarType)
| call (xfn : ExtFun) (args : List TypedExpr) (ty : CedarType)
deriving instance Repr, Inhabited for TypedExpr
mutual
def decTypedExpr (x y : TypedExpr) : Decidable (x = y) := by
cases x <;> cases y <;>
try { apply isFalse ; intro h ; injection h }
case lit.lit x₁ tx y₁ ty | var.var x₁ tx y₁ ty =>
exact match decEq x₁ y₁, decEq tx ty with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁, h₂])
| isFalse _, _ | _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case ite.ite x₁ x₂ x₃ tx y₁ y₂ y₃ ty =>
exact match decTypedExpr x₁ y₁, decTypedExpr x₂ y₂, decTypedExpr x₃ y₃, decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃, isTrue h₄ => isTrue (by rw [h₁, h₂, h₃, h₄])
| isFalse _, _, _, _ | _, isFalse _, _, _ | _, _, isFalse _, _ | _, _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case and.and x₁ x₂ tx y₁ y₂ ty | or.or x₁ x₂ tx y₁ y₂ ty =>
exact match decTypedExpr x₁ y₁, decTypedExpr x₂ y₂, decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃ => isTrue (by rw [h₁, h₂, h₃])
| isFalse _, _, _ | _, isFalse _, _ | _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case unaryApp.unaryApp o x₁ tx o' y₁ ty =>
exact match decEq o o', decTypedExpr x₁ y₁, decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃ => isTrue (by rw [h₁, h₂, h₃])
| isFalse _, _, _ | _, isFalse _, _ | _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case binaryApp.binaryApp o x₁ x₂ tx o' y₁ y₂ ty =>
exact match decEq o o', decTypedExpr x₁ y₁, decTypedExpr x₂ y₂, decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃, isTrue h₄ => isTrue (by rw [h₁, h₂, h₃, h₄])
| isFalse _, _, _, _ | _, isFalse _, _, _ | _, _, isFalse _, _ | _, _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case getAttr.getAttr x₁ a tx y₁ a' ty | hasAttr.hasAttr x₁ a tx y₁ a' ty =>
exact match decTypedExpr x₁ y₁, decEq a a', decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃ => isTrue (by rw [h₁, h₂, h₃])
| isFalse _, _, _ | _, isFalse _, _ | _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case set.set xs tx ys ty =>
exact match decExprList xs ys, decEq tx ty with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁, h₂])
| isFalse _, _ | _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case record.record axs tx ays ty =>
exact match decProdAttrExprList axs ays, decEq tx ty with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁, h₂])
| isFalse _, _ | _, isFalse _ => isFalse (by intro h; injection h; contradiction)
case call.call f xs tx f' ys ty =>
exact match decEq f f', decExprList xs ys, decEq tx ty with
| isTrue h₁, isTrue h₂, isTrue h₃ => isTrue (by rw [h₁, h₂, h₃])
| isFalse _, _, _ | _, isFalse _, _ | _, _, isFalse _ => isFalse (by intro h; injection h; contradiction)
def decProdAttrExprList (axs ays : List (Prod Attr TypedExpr)) : Decidable (axs = ays) :=
match axs, ays with
| [], [] => isTrue rfl
| _::_, [] | [], _::_ => isFalse (by intro; contradiction)
| (a, x)::axs, (a', y)::ays =>
match decEq a a', decTypedExpr x y, decProdAttrExprList axs ays with
| isTrue h₁, isTrue h₂, isTrue h₃ => isTrue (by rw [h₁, h₂, h₃])
| isFalse _, _, _ | _, isFalse _, _ | _, _, isFalse _ =>
isFalse (by simp; intros; first | contradiction | assumption)
def decExprList (xs ys : List TypedExpr) : Decidable (xs = ys) :=
match xs, ys with
| [], [] => isTrue rfl
| _::_, [] | [], _::_ => isFalse (by intro; contradiction)
| x::xs, y::ys =>
match decTypedExpr x y, decExprList xs ys with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁, h₂])
| isFalse _, _ | _, isFalse _ => isFalse (by intro h; injection h; contradiction)
end
instance : DecidableEq TypedExpr := decTypedExpr
def TypedExpr.typeOf : TypedExpr → CedarType
| lit _ ty
| var _ ty
| ite _ _ _ ty
| and _ _ ty
| or _ _ ty
| unaryApp _ _ ty
| binaryApp _ _ _ ty
| getAttr _ _ ty
| hasAttr _ _ ty
| set _ ty
| record _ ty
| call _ _ ty => ty
def TypedExpr.toExpr : TypedExpr → Expr
| lit p _ => Expr.lit p
| var v _ => Expr.var v
| ite cond thenExpr elseExpr _ => Expr.ite cond.toExpr thenExpr.toExpr elseExpr.toExpr
| and a b _ => Expr.and a.toExpr b.toExpr
| or a b _ => Expr.or a.toExpr b.toExpr
| unaryApp op expr _ => Expr.unaryApp op expr.toExpr
| binaryApp op a b _ => Expr.binaryApp op a.toExpr b.toExpr
| getAttr expr attr _ => Expr.getAttr expr.toExpr attr
| hasAttr expr attr _ => Expr.hasAttr expr.toExpr attr
| set ls ty => Expr.set $ ls.map₁ (λ ⟨e, h₁⟩ =>
have _ : sizeOf e < 1 + sizeOf ls + sizeOf ty := by
have := List.sizeOf_lt_of_mem h₁
omega
e.toExpr)
| record ls ty => Expr.record $ ls.map₁ (λ ⟨(a, e), h₁⟩ =>
have _ : sizeOf e < 1 + sizeOf ls + sizeOf ty := by
have := Map.sizeOf_lt_of_value h₁
simp only [Map.mk.sizeOf_spec] at this
omega
(a, e.toExpr))
| call xfn args ty => Expr.call xfn $ args.map₁ (λ ⟨e, h₁⟩ =>
have _ : sizeOf e < 1 + sizeOf args + sizeOf ty := by
have := List.sizeOf_lt_of_mem h₁
omega
e.toExpr)
end Cedar.Validation