-
Notifications
You must be signed in to change notification settings - Fork 46
/
definterp.v
375 lines (286 loc) · 15.2 KB
/
definterp.v
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
(* begin hide *)
(**********************************************************************)
(* Equations *)
(* Copyright (c) 2009-2021 Matthieu Sozeau <[email protected]> *)
(**********************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(**********************************************************************)
(* end hide *)
(** * Definitional interpreter for STLC extended with references
This is a port of the first part of "Intrinsically-Typed Definitional
Interpreters for Imperative Languages", Poulsen, Rouvoet, Tolmach,
Krebbers and Visser. POPL'18.
It uses well-typed and well-scoped syntax and a monad indexed over an
indexed set of stores to define an interpreter for an imperative
programming language.
This showcases the use of dependent pattern-matching and
pattern-matching lambdas in Equations. We implement a variant where
store extension is resolved using type class resolution as well as the
dependent-passing style version. *)
Require Import Program.Basics Program.Tactics.
Require Import Stdlib.Vectors.VectorDef.
Require Import List.
Import ListNotations.
Require Import Utf8.
From Equations Require Import Equations.
Set Warnings "-notation-overridden".
(** The Σ notation of equations clashes with the Σ's used below,
so we redefine the Σ notation using ∃ instead.
*)
Notation "'∃' x .. y , P" := (sigma (fun x => .. (sigma (fun y => P)) ..))
: type_scope.
Notation "( x , .. , y , z )" :=
(@sigmaI _ _ x .. (@sigmaI _ _ y z) ..)
(right associativity, at level 0,
format "( x , .. , y , z )") : equations_scope.
Notation " x .1 " := (pr1 x) : equations_scope.
Notation " x .2 " := (pr2 x) : equations_scope.
Local Open Scope equations_scope.
Set Equations Transparent.
(** [t] is just [Vector.t] here. *)
Derive Signature NoConfusion NoConfusionHom for t.
(** Types include unit, bool, function types and references *)
Inductive Ty : Set :=
| unit : Ty
| bool : Ty
| arrow (t u : Ty) : Ty
| ref : Ty -> Ty.
Derive NoConfusion for Ty.
Infix "⇒" := arrow (at level 80).
Definition Ctx := list Ty.
Reserved Notation " x ∈ s " (at level 70, s at level 10).
#[universes(template)]
Inductive In {A} (x : A) : list A -> Type :=
| here {xs} : x ∈ (x :: xs)
| there {y xs} : x ∈ xs -> x ∈ (y :: xs)
where " x ∈ s " := (In x s).
Derive Signature NoConfusion for In.
Arguments here {A x xs}.
Arguments there {A x y xs} _.
Inductive Expr : Ctx -> Ty -> Set :=
| tt {Γ} : Expr Γ unit
| true {Γ} : Expr Γ bool
| false {Γ} : Expr Γ bool
| ite {Γ t} : Expr Γ bool -> Expr Γ t -> Expr Γ t -> Expr Γ t
| var {Γ} {t} : In t Γ -> Expr Γ t
| abs {Γ} {t u} : Expr (t :: Γ) u -> Expr Γ (t ⇒ u)
| app {Γ} {t u} : Expr Γ (t ⇒ u) -> Expr Γ t -> Expr Γ u
| new {Γ t} : Expr Γ t -> Expr Γ (ref t)
| deref {Γ t} : Expr Γ (ref t) -> Expr Γ t
| assign {Γ t} : Expr Γ (ref t) -> Expr Γ t -> Expr Γ unit.
(** We derive both [NoConfusion] and [NoConfusionHom] principles here, the later
allows to simplify pattern-matching problems on [Expr] which would otherwise
require K. It relies on an inversion analysis of every constructor, showing
that the context and type indexes in the conclusions of every constructor
are forced arguments. *)
Derive Signature NoConfusion NoConfusionHom for Expr.
#[universes(template)]
Inductive All {A} (P : A -> Type) : list A -> Type :=
| all_nil : All P []
| all_cons {x xs} : P x -> All P xs -> All P (x :: xs).
Arguments all_nil {A} {P}.
Arguments all_cons {A P x xs} _ _.
Derive Signature NoConfusion NoConfusionHom for All.
Section MapAll.
Context {A} {P Q : A -> Type} (f : forall x, P x -> Q x).
Equations map_all {l : list A} : All P l -> All Q l :=
| all_nil := all_nil
| all_cons p ps := all_cons (f _ p) (map_all ps).
Equations map_all_in {l : list A} (f : forall x, x ∈ l -> P x -> Q x) : All P l -> All Q l :=
| f, all_nil := all_nil
| f, all_cons p ps := all_cons (f _ here p) (map_all_in (fun x inl => f x (there inl)) ps).
End MapAll.
Definition StoreTy := list Ty.
Inductive Val : Ty -> StoreTy -> Set :=
| val_unit {Σ} : Val unit Σ
| val_true {Σ} : Val bool Σ
| val_false {Σ} : Val bool Σ
| val_closure {Σ Γ t u} : Expr (t :: Γ) u -> All (fun t => Val t Σ) Γ -> Val (t ⇒ u) Σ
| val_loc {Σ t} : t ∈ Σ -> Val (ref t) Σ.
Derive Signature NoConfusion NoConfusionHom for Val.
Definition Env (Γ : Ctx) (Σ : StoreTy) : Set := All (fun t => Val t Σ) Γ.
Definition Store (Σ : StoreTy) := All (fun t => Val t Σ) Σ.
Equations lookup : forall {A P xs} {x : A}, All P xs -> x ∈ xs -> P x :=
lookup (all_cons p _) here := p;
lookup (all_cons _ ps) (there ins) := lookup ps ins.
Equations update : forall {A P xs} {x : A}, All P xs -> x ∈ xs -> P x -> All P xs :=
update (all_cons p ps) here p' := all_cons p' ps;
update (all_cons p ps) (there ins) p' := all_cons p (update ps ins p').
Equations lookup_store {Σ t} : t ∈ Σ -> Store Σ -> Val t Σ :=
lookup_store l σ := lookup σ l.
Equations update_store {Σ t} : t ∈ Σ -> Val t Σ -> Store Σ -> Store Σ :=
update_store l v σ := update σ l v.
Definition store_incl (Σ Σ' : StoreTy) := sigma (fun Σ'' => Σ' = Σ'' ++ Σ).
Infix "⊑" := store_incl (at level 10).
Equations app_assoc {A} (x y z : list A) : x ++ y ++ z = (x ++ y) ++ z :=
app_assoc nil y z := eq_refl;
app_assoc (cons x xs) y z := f_equal (cons x) (app_assoc xs y z).
Section StoreIncl.
Equations pres_in {Σ Σ'} (incl : Σ ⊑ Σ') t (p : t ∈ Σ) : t ∈ Σ' :=
pres_in (Σ'', eq_refl) t p := aux Σ''
where aux Σ'' : t ∈ (Σ'' ++ Σ) :=
aux nil := p;
aux (cons ty tys) := there (aux tys).
Equations refl_incl {Σ} : Σ ⊑ Σ := refl_incl := ([], eq_refl).
Equations trans_incl {Σ Σ' Σ''} (incl : Σ ⊑ Σ') (incl' : Σ' ⊑ Σ'') : Σ ⊑ Σ'' :=
trans_incl (p, eq_refl) (q, eq_refl) := (q ++ p, app_assoc _ _ _).
Equations store_ext_incl {Σ t} : Σ ⊑ (t :: Σ) :=
store_ext_incl := ([t], eq_refl).
Context {Σ Σ'} (incl : Σ ⊑ Σ').
Equations weaken_val {t} (v : Val t Σ) : Val t Σ' := {
weaken_val (@val_unit ?(Σ)) := val_unit;
weaken_val val_true := val_true;
weaken_val val_false := val_false;
weaken_val (val_closure b e) := val_closure b (weaken_vals e);
weaken_val (val_loc H) := val_loc (pres_in incl _ H) }
where weaken_vals {l} (a : All (fun t => Val t Σ) l) : All (fun t => Val t Σ') l :=
weaken_vals all_nil := all_nil;
weaken_vals (all_cons p ps) := all_cons (weaken_val p) (weaken_vals ps).
Equations weakenv_vals {l} a : @weaken_vals l a = map_all (fun t v => weaken_val v) a :=
weakenv_vals all_nil := eq_refl;
weakenv_vals (all_cons p ps) := f_equal (all_cons (weaken_val p)) (weakenv_vals ps).
Definition weaken_env {Γ} (v : Env Γ Σ) : Env Γ Σ' := map_all (@weaken_val) v.
End StoreIncl.
Infix "⊚" := trans_incl (at level 10).
Equations M : forall (Γ : Ctx) (P : StoreTy -> Type) (Σ : StoreTy), Type :=
M Γ P Σ := forall (E : Env Γ Σ) (μ : Store Σ), option (∃ Σ' (μ' : Store Σ') (_ : P Σ'), Σ ⊑ Σ').
Equations bind {Σ Γ} {P Q : StoreTy -> Type} (f : M Γ P Σ) (g : ∀ {Σ'}, P Σ' -> M Γ Q Σ') : M Γ Q Σ :=
bind f g E μ with f E μ :=
| None := None
| Some (Σ', μ', x, ext) with g _ x (weaken_env ext E) μ' :=
| None := None;
| Some (_, μ'', y, ext') := Some (_, μ'', y, ext ⊚ ext').
Infix ">>=" := bind (at level 20, left associativity).
Definition transp_op {Γ Σ P} (x : Store Σ -> P Σ) : M Γ P Σ :=
fun E μ => Some (Σ, μ, x μ, refl_incl).
Equations ret : ∀ {Γ Σ P}, P Σ → M Γ P Σ :=
ret (Σ:=Σ) a E μ := Some (Σ, μ, a, refl_incl).
Equations getEnv : ∀ {Γ Σ}, M Γ (Env Γ) Σ :=
getEnv (Σ:=Σ) E μ := Some (Σ, μ, E, refl_incl).
Equations usingEnv {Γ Γ' Σ P} (E : Env Γ Σ) (m : M Γ P Σ) : M Γ' P Σ :=
usingEnv E m E' μ := m E μ.
Equations timeout : ∀ {Γ Σ P}, M Γ P Σ :=
timeout _ _ := None.
Section StoreOps.
Context {Σ : StoreTy} {Γ : Ctx} {t : Ty}.
Equations storeM (v : Val t Σ) : M Γ (Val (ref t)) Σ :=
storeM v E μ :=
let v : Val t (t :: Σ) := weaken_val store_ext_incl v in
let μ' := map_all (fun t' => weaken_val store_ext_incl) μ in
Some (t :: Σ, all_cons v μ', val_loc here, store_ext_incl).
Equations derefM (l : t ∈ Σ) : M Γ (Val t) Σ :=
derefM l := transp_op (lookup_store l).
Equations updateM (l : t ∈ Σ) (v : Val t Σ) : M Γ (Val unit) Σ :=
updateM l v E μ := Some (Σ, update_store l v μ, val_unit, refl_incl).
End StoreOps.
Reserved Notation "P ⊛ Q" (at level 10).
Inductive storepred_prod (P Q : StoreTy -> Type) : StoreTy -> Type :=
| storepred_pair {Σ} : P Σ -> Q Σ -> (P ⊛ Q) Σ
where "P ⊛ Q" := (storepred_prod P Q).
Arguments storepred_pair {P Q Σ}.
Class Weakenable (P : StoreTy -> Type) : Type :=
weaken : forall {Σ Σ'}, Σ ⊑ Σ' -> P Σ -> P Σ'.
#[local] Instance val_weaken {t} : Weakenable (Val t) := fun Σ Σ' incl => weaken_val incl.
#[local] Instance env_weaken {Γ} : Weakenable (Env Γ) := fun Σ Σ' incl => weaken_env incl.
#[local] Instance loc_weaken (t : Ty) : Weakenable (In t) := fun Σ Σ' incl => pres_in incl t.
Class IsIncludedOnce (Σ Σ' : StoreTy) : Type := is_included_once : Σ ⊑ Σ'.
#[local] Hint Mode IsIncludedOnce + + : typeclass_instances.
#[local] Instance IsIncludedOnce_ext {T} Σ : IsIncludedOnce Σ (T :: Σ) := store_ext_incl.
Class IsIncluded (Σ Σ' : StoreTy) : Type := is_included : Σ ⊑ Σ'.
#[local] Hint Mode IsIncluded + + : typeclass_instances.
#[local] Instance IsIncluded_refl Σ : IsIncluded Σ Σ := refl_incl.
#[local] Instance IsIncluded_trans Σ Σ' Σ'' : IsIncludedOnce Σ Σ' -> IsIncluded Σ' Σ'' -> IsIncluded Σ Σ'' :=
fun H H' => trans_incl H H'.
Equations wk {Σ Σ' P} {W : Weakenable P} (p : P Σ) {incl : IsIncluded Σ Σ'} : P Σ' :=
wk p := weaken incl p.
Equations bind_ext {Σ Γ} {P Q : StoreTy -> Type} (f : M Γ P Σ) (g : ∀ {Σ'} `{IsIncluded Σ Σ'}, P Σ' -> M Γ Q Σ') : M Γ Q Σ :=
bind_ext f g E μ with f E μ :=
{ | None := None;
| Some (Σ', μ', x, ext) with g _ ext x (weaken_env ext E) μ' :=
{ | None := None;
| Some (_, μ'', y, ext') := Some (_, μ'', y, ext ⊚ ext') } }.
Infix ">>='" := bind_ext (at level 20, left associativity).
Equations eval_ext (n : nat) {Γ Σ t} (e : Expr Γ t) : M Γ (Val t) Σ :=
| 0, _ := timeout
| S k, tt := ret val_unit
| S k, true := ret val_true
| S k, false := ret val_false
| S k, ite b tr fa := eval_ext k b >>=' λ{ | _ | ext | val_true => eval_ext k tr;
| _ | ext | val_false => eval_ext k fa }
| S k, var x := getEnv >>=' fun {Σ ext} E => ret (lookup E x)
| S k, abs x := getEnv >>=' fun {Σ ext} E => ret (val_closure x E)
| S k, @app Γ A B e1 e2 :=
eval_ext k e1 >>=' λ{ | _ | ext | val_closure e' E =>
eval_ext k e2 >>=' fun {Σ' ext'} v => usingEnv (all_cons v (wk (P:=Env _) E)) (eval_ext k e')}
| S k, new e := eval_ext k e >>=' fun {Σ ext} v => storeM v
| S k, deref l := eval_ext k l >>=' λ{ | _ | ext | val_loc l' => derefM l' }
| S k, assign l e := eval_ext k l >>=' λ{ | _ | ext | val_loc l' =>
eval_ext k e >>=' λ{ | _ | ext' | v => updateM (wk l') (wk v) }}.
Equations strength {Σ Γ} {P Q : StoreTy -> Type} {w : Weakenable Q} (m : M Γ P Σ) (q : Q Σ) : M Γ (P ⊛ Q) Σ :=
strength m q E μ with m E μ => {
| None => None
| Some (Σ', μ', p, ext) => Some (Σ', μ', storepred_pair p (weaken ext q), ext) }.
Infix "^" := strength.
(* Issue: improve pattern matching lambda to have implicit arguments implicit.
Hard because Coq does not keep the implicit status of bind's [g] argument. *)
Equations eval (n : nat) {Γ Σ t} (e : Expr Γ t) : M Γ (Val t) Σ :=
eval 0 _ := timeout;
eval (S k) tt := ret val_unit;
eval (S k) true := ret val_true;
eval (S k) false := ret val_false;
eval (S k) (ite b tr fa) := eval k b >>= λ{ | _ | val_true => eval k tr;
| _ | val_false => eval k fa };
eval (S k) (var x) := getEnv >>= fun Σ E => ret (lookup E x);
eval (S k) (abs x) := getEnv >>= fun Σ E => ret (val_closure x E);
eval (S k) (app e1 e2) :=
eval k e1 >>= λ{ | _ | val_closure e' E =>
(eval k e2 ^ E) >>= fun Σ' '(storepred_pair v E) => usingEnv (all_cons v E) (eval k e')};
eval (S k) (new e) := eval k e >>= fun Σ v => storeM v;
eval (S k) (deref l) := eval k l >>= λ{ | _ | val_loc l' => derefM l' };
eval (S k) (assign l e) := eval k l >>= λ{ | _ | val_loc l' =>
(eval k e ^ l') >>= λ{ | _ | storepred_pair v l'' => updateM l'' v }}.
Definition idu : Expr [] (unit ⇒ unit) :=
abs (var here).
Definition idapp : Expr [] unit := app idu tt.
(** All definitions are axiom-free (and actually not even dependent on a provable UIP instance), so
everything computes. *)
Eval vm_compute in eval 100 idapp all_nil all_nil.
Definition neg : Expr [] (bool ⇒ bool) :=
abs (ite (var here) false true).
Definition letref {t u} (v : Expr [] t) (b : Expr [ref t] u) : Expr [] u :=
app (abs b) (new v).
Obligation Tactic := idtac.
Equations in_app_weaken {Σ Σ' Σ'' : StoreTy} {t} (p : t ∈ (Σ ++ Σ'')) : t ∈ (Σ ++ Σ' ++ Σ'') by struct Σ :=
in_app_weaken (Σ:=nil) p := pres_in (Σ', eq_refl) t p;
in_app_weaken (Σ:=cons _ tys) here := here;
in_app_weaken (Σ:=cons _ tys) (there p) := there (in_app_weaken p).
Equations pres_in_prefix {Σ Σ' Σ''} (incl : Σ' ⊑ Σ'') {t} (p : t ∈ (Σ ++ Σ')) : t ∈ (Σ ++ Σ'') :=
pres_in_prefix (Σ'', eq_refl) p := in_app_weaken p.
(** [Equations?] enters refinement mode, which can be used to solve the case of variables in proof mode. *)
Equations? weaken_expr {Γ Γ' t u} (e1 : Expr (Γ ++ Γ') t) : Expr (Γ ++ u :: Γ') t :=
weaken_expr tt := tt;
weaken_expr true := true;
weaken_expr false := false;
weaken_expr (ite b tr fa) := ite (weaken_expr b) (weaken_expr tr) (weaken_expr fa);
weaken_expr (var (t:=ty) x) := var _;
weaken_expr (abs (t:=t) x) := abs (weaken_expr (Γ := t :: Γ) x);
weaken_expr (app e1 e2) := app (weaken_expr e1) (weaken_expr e2);
weaken_expr (new e) := new (weaken_expr e);
weaken_expr (deref l) := deref (weaken_expr l);
weaken_expr (assign l e) := assign (weaken_expr l) (weaken_expr e).
Proof.
clear weaken_expr. apply (pres_in_prefix (Σ' := Γ') ([u], eq_refl) x).
Defined.
Definition seq {Γ u} (e1 : Expr Γ unit) (e2 : Expr Γ u) : Expr Γ u :=
app (abs (weaken_expr (Γ := []) e2)) e1.
(* let x = ref true in
x := false; !x *)
Definition letupdate : Expr [] bool :=
letref true (seq (assign (var here) false) (deref (var here))).
Eval vm_compute in eval 100 letupdate all_nil all_nil.
(** [[
= Some ([bool], all_cons val_false all_nil, val_false, [bool], eq_refl)
: option (∃ (Σ' : StoreTy) (_ : Store Σ') (_ : Val bool Σ'), [] ⊑ Σ')
]]
*)