typed.v 6.32 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
From tutorial_popl20 Require Export types.

Inductive ty_unboxed : ty  Prop :=
  | TUnit_unboxed : ty_unboxed TUnit
  | TBool_unboxed : ty_unboxed TBool
  | TInt_unboxed : ty_unboxed TInt
  | TRef_unboxed τ : ty_unboxed (TRef τ).
Existing Class ty_unboxed.
Existing Instances TUnit_unboxed TBool_unboxed TInt_unboxed TRef_unboxed.

11
12
13
14
15
16
Inductive ty_un_op : un_op  ty  ty  Prop :=
  | Ty_un_op_int op : ty_un_op op TInt TInt
  | Ty_un_op_bool : ty_un_op NegOp TBool TBool.
Existing Class ty_un_op.
Existing Instances Ty_un_op_int Ty_un_op_bool.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Inductive ty_bin_op : bin_op  ty  ty  ty  Prop :=
  | Ty_bin_op_eq τ :
     ty_unboxed τ  ty_bin_op EqOp τ τ TBool
  | Ty_bin_op_arith op :
     TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
                  AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] 
     ty_bin_op op TInt TInt TInt
  | Ty_bin_op_compare op :
     TCElemOf op [LeOp; LtOp]  ty_bin_op op TInt TInt TBool
  | Ty_bin_op_bool op :
     TCElemOf op [AndOp; OrOp; XorOp]  ty_bin_op op TBool TBool TBool.
Existing Class ty_bin_op.
Existing Instances Ty_bin_op_eq Ty_bin_op_arith Ty_bin_op_compare Ty_bin_op_bool.

Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
32
33
34
Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).

Inductive typed : gmap string ty  expr  ty  Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  (** Variables *)
36
  | Var_typed Γ x τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
     Γ !! x = Some τ 
     Γ  Var x : τ
39
40
41
42
  (** Values *)
  | Val_typed Γ v τ :
     val_typed v τ 
     Γ  v : τ
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  (** Products and sums *)
44
  | Pair_typed Γ e1 e2 τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
     Γ  e1 : τ1  Γ  e2 : τ2 
     Γ  Pair e1 e2 : TProd τ1 τ2
47
  | Fst_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
     Γ  e : TProd τ1 τ2 
     Γ  Fst e : τ1
50
  | Snd_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
     Γ  e : TProd τ1 τ2 
     Γ  Snd e : τ2
53
  | InjL_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
     Γ  e : τ1 
     Γ  InjL e : TSum τ1 τ2
56
  | InjR_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
     Γ  e : τ2 
     Γ  InjR e : TSum τ1 τ2
59
  | Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
     Γ  e0 : TSum τ1 τ2  Γ  e1 : TArr τ1 τ3  Γ  e2 : TArr τ2 τ3 
     Γ  Case e0 e1 e2 : τ3
62
  (** Functions *)
63
  | Rec_typed Γ f x e τ1 τ2 :
64
65
     binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ)  e : τ2 
     Γ  Rec f x e : TArr τ1 τ2
66
  | App_typed Γ e1 e2 τ1 τ2 :
67
68
     Γ  e1 : TArr τ1 τ2  Γ  e2 : τ1 
     Γ  App e1 e2 : τ2
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  (** Polymorphic functions and existentials *)
70
  | TLam_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
     ty_lift 0 <$> Γ  e : τ 
     Γ  (Λ: e) : TForall τ
73
  | TApp_typed Γ e τ τ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
74
     Γ  e : TForall τ 
75
     Γ  e <_> : ty_subst 0 τ' τ
76
  | Pack_typed Γ e τ τ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
77
     Γ  e : ty_subst 0 τ' τ 
Robbert Krebbers's avatar
Robbert Krebbers committed
78
     Γ  (pack: e) : TExist τ
79
  | Unpack_typed Γ e1 x e2 τ τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
     Γ  e1 : TExist τ 
     binder_insert x τ (ty_lift 0 <$> Γ)  e2 : ty_lift 0 τ2 
     Γ  (unpack: x := e1 in e2) : τ2
  (** Heap operations *)
84
  | Alloc_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
     Γ  e : τ 
     Γ  Alloc e : TRef τ
87
  | Load_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
     Γ  e : TRef τ 
     Γ  Load e : τ
90
  | Store_typed Γ e1 e2 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
     Γ  e1 : TRef τ  Γ  e2 : τ 
     Γ  Store e1 e2 : TUnit
93
  | FAA_typed Γ e1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
     Γ  e1 : TRef TInt  Γ  e2 : TInt 
     Γ  FAA e1 e2 : TInt
96
  | CmpXchg_typed Γ e1 e2 e3 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
99
100
     ty_unboxed τ 
     Γ  e1 : TRef τ  Γ  e2 : τ  Γ  e3 : τ 
     Γ  CmpXchg e1 e2 e3 : TProd τ TBool
  (** Operators *)
101
  | UnOp_typed Γ op e τ σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
     Γ  e : τ 
     ty_un_op op τ σ 
     Γ  UnOp op e : σ
105
  | BinOp_typed Γ op e1 e2 τ1 τ2 σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
     Γ  e1 : τ1  Γ  e2 : τ2 
     ty_bin_op op τ1 τ2 σ 
     Γ  BinOp op e1 e2 : σ
109
  | If_typed Γ e0 e1 e2 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
     Γ  e0 : TBool  Γ  e1 : τ  Γ  e2 : τ 
     Γ  If e0 e1 e2 : τ
  (** Fork *)
113
  | Fork_typed Γ e :
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
     Γ  e : TUnit 
     Γ  Fork e : TUnit
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
with val_typed : val  ty  Prop :=
  (** Base types *)
  | UnitV_typed :
      #() : TUnit
  | BoolV_typed (b : bool) :
      #b : TBool
  | IntV_val_typed (i : Z) :
      #i : TInt
  (** Products and sums *)
  | PairV_typed v1 v2 τ1 τ2 :
      v1 : τ1   v2 : τ2 
      PairV v1 v2 : TProd τ1 τ2
  | InjLV_typed v τ1 τ2 :
      v : τ1 
      InjLV v : TSum τ1 τ2
  | InjRV_typed v τ1 τ2 :
      v : τ2 
      InjRV v : TSum τ1 τ2
  (** Functions *)
  | RecV_typed f x e τ1 τ2 :
     binder_insert f (TArr τ1 τ2) (binder_insert x τ1 )  e : τ2 
      RecV f x e : TArr τ1 τ2
where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ v : τ" := (val_typed v τ).
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141

Lemma Lam_typed Γ x e τ1 τ2 :
142
  binder_insert x τ1 Γ  e : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148
149
150
151
  Γ  (λ: x, e) : TArr τ1 τ2.
Proof.
  intros He.
  apply Rec_typed.
  simpl.
  done.
Qed.

Lemma LamV_typed x e τ1 τ2 :
152
  binder_insert x τ1   e : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
158
159
160
161
   (λ: x, e) : TArr τ1 τ2.
Proof.
  intros He.
  apply RecV_typed.
  simpl.
  done.
Qed.

Lemma Let_typed Γ x e1 e2 τ1 τ2 :
162
163
  Γ  e1 : τ1 
  binder_insert x τ1 Γ  e2 : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
167
168
169
170
171
172
  Γ  (let: x := e1 in e2) : τ2.
Proof.
  intros He1 He2.
  apply App_typed with τ1.
  - by apply Lam_typed.
  - done.
Qed.

Lemma Seq_typed Γ e1 e2 τ1 τ2 :
173
174
  Γ  e1 : τ1 
  Γ  e2 : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
  Γ  (e1;; e2) : τ2.
Proof.
  intros He1 He2.
  by apply Let_typed with τ1.
Qed.

Lemma Skip_typed Γ :
  Γ  Skip : ().
Proof.
  apply App_typed with ()%ty.
  - apply Val_typed, RecV_typed. apply Val_typed, UnitV_typed.
  - apply Val_typed, UnitV_typed.
Qed.

Definition swap : val := λ: "l1" "l2",
  let: "x" := !"l1" in
  "l1" <- !"l2";;
  "l2" <- "x".

Lemma swap_typed τ :  swap : (ref τ  ref τ  ()).
Proof.
  unfold swap.
  apply LamV_typed.
  apply Lam_typed.
  apply Let_typed with τ.
  { apply Load_typed. by apply Var_typed. }
  apply Seq_typed with ()%ty.
  { apply Store_typed with τ.
    - by apply Var_typed.
    - apply Load_typed. by apply Var_typed. }
  apply Store_typed with τ.
  - by apply Var_typed.
  - by apply Var_typed.
Qed.