pureexec.v 2.29 KB
Newer Older
1 2
From iris_logrel.prelude Require Export hax.
From iris_logrel.F_mu_ref_conc Require Export lang subst notation.
3

Dan Frumin's avatar
Dan Frumin committed
4 5 6 7 8
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pureexec :=
  apply hoist_pred_pureexec; intros; destruct_and?;
  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
9

10 11 12 13
Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
  PureExec (binop_eval op v1 v2 = Some v)
           (BinOp op e1 e2)
           (of_val v).
Dan Frumin's avatar
Dan Frumin committed
14
Proof. solve_pureexec. Qed.
15

16
Instance pure_rec f x e1 e2 v2 `{Closed  (Rec f x e1)} `(to_val e2 = Some v2) :
17 18 19
  PureExec True
           (App (Rec f x e1) e2)
           (subst' f (Rec f x e1) (subst' x e2 e1)).
Dan Frumin's avatar
Dan Frumin committed
20
Proof. solve_pureexec. Qed.
21 22 23 24 25 26 27

(* TODO: give this one a correct priority? *)
Instance pure_rec_locked e f x e1 e2 v2 `(to_val e2 = Some v2) `(e = Rec f x e1) `{Closed (x :b: f :b: ) e1} :
  PureExec True
           (App e e2)
           (e $/ v2) | 100.
Proof.
Dan Frumin's avatar
Dan Frumin committed
28 29 30 31
  apply hoist_pred_pureexec; intros; destruct_and?;
  apply det_head_step_pureexec. 
  - solve_exec_safe.
  - destruct f; solve_exec_puredet.
32 33 34
Qed.

Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
35
  PureExec True (Fst (Pair e1 e2)) e1.
Dan Frumin's avatar
Dan Frumin committed
36
Proof. solve_pureexec. Qed.
37 38

Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
39
  PureExec True (Snd (Pair e1 e2)) e2.
Dan Frumin's avatar
Dan Frumin committed
40
Proof. solve_pureexec. Qed.
41 42 43

Instance pure_unfold e1 v1 `(to_val e1 = Some v1) :
  PureExec True (Unfold (Fold e1)) e1.
Dan Frumin's avatar
Dan Frumin committed
44
Proof. solve_pureexec. Qed.
45

46 47
Instance pure_unpack e1 e2 v1 `(to_val e1 = Some v1) :
  PureExec True (Unpack (Pack e1) e2) (e2 e1).
Dan Frumin's avatar
Dan Frumin committed
48
Proof. solve_pureexec. Qed.
49

50
Instance pure_if_true e1 e2 :
51
  PureExec True (If #true e1 e2) e1.
Dan Frumin's avatar
Dan Frumin committed
52
Proof. solve_pureexec. Qed.
53

54
Instance pure_if_false e1 e2 :
55
  PureExec True (If #false e1 e2) e2.
Dan Frumin's avatar
Dan Frumin committed
56
Proof. solve_pureexec. Qed.
57

58
Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2  :
59
  PureExec True (Case (InjL e0) e1 e2) (e1 e0).
Dan Frumin's avatar
Dan Frumin committed
60
Proof. solve_pureexec. Qed.
61

62
Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2  :
63
  PureExec True (Case (InjR e0) e1 e2) (e2 e0).
Dan Frumin's avatar
Dan Frumin committed
64
Proof. solve_pureexec. Qed.
Dan Frumin's avatar
Dan Frumin committed
65 66 67 68 69

Instance pure_tlam e `{Closed  e} :
  PureExec True
           (TApp (TLam e))
           e.
Dan Frumin's avatar
Dan Frumin committed
70
Proof. solve_pureexec. Qed.