-
Notifications
You must be signed in to change notification settings - Fork 4
/
class_instances.v
109 lines (91 loc) · 4.53 KB
/
class_instances.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
From iris_simp_lang Require Import notation tactics.
From iris.prelude Require Import options.
(*|
These instances prove that various expressions are atomic or pure.
`Atomic e` is defined generically for languages by saying `e` reduces to a value
(recall: this is defined by `to_val e = Some _`) in a single step.
`PureExec φ n e1 e2` shows that if φ holds (a pure Coq proposition), `e1`
executes to `e2` in `n` steps. This is eventually needed to define a tactic
`wp_pure _` that finds and reasons about pure reductions (this subsumes
`wp_let`, `wp_seq`, `wp_app` and the like, which are just restrictions of
`wp_pure`).
|*)
Global Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Global Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.
(** * Instances of the [Atomic] class *)
Section atomic.
Local Ltac solve_atomic :=
apply strongly_atomic_atomic, ectx_language_atomic;
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Global Instance rec_atomic s f x e : Atomic s (Rec f x e).
Proof. solve_atomic. Qed.
(** The instance below is a more general version of [Skip] *)
Global Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
Proof. destruct f, x; solve_atomic. Qed.
Global Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
Proof. solve_atomic. Qed.
Global Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance if_true_atomic s v1 e2 :
Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
Proof. solve_atomic. Qed.
Global Instance if_false_atomic s e1 v2 :
Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
Proof. solve_atomic. Qed.
Global Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Global Instance heap_op_atomic op s v1 v2 : Atomic s (HeapOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
End atomic.
(** * Instances of the [PureExec] class *)
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:
- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.
To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
as_recv : v = RecV f x erec.
Global Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
apply AsRecV_recv : typeclass_instances.
Section pure_exec.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_base_step.
Local Ltac solve_pure_exec :=
subst; intros ?; apply nsteps_once, pure_base_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_recc f x (erec : expr) :
PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Global Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
Global Instance pure_unop op v v' :
PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
Proof. solve_pure_exec. Qed.
Global Instance pure_binop op v1 v2 v' :
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed.
(* Higher-priority instance for [EqOp]. *)
Global Instance pure_eqop v1 v2 :
PureExec True 1
(BinOp EqOp (Val v1) (Val v2))
(Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof. solve_pure_exec. Qed.
Global Instance pure_if_true e1 e2 :
PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed.
Global Instance pure_if_false e1 e2 :
PureExec True 1 (If (Val $ LitV $ LitBool false) e1 e2) e2.
Proof. solve_pure_exec. Qed.
End pure_exec.