Make use of the `IntoVal` typeclass

theories/F_mu_ref_conc/pureexec.v

@@ -4,46 +4,51 @@ From iris_logrel.F_mu_ref_conc Require Export lang subst notation.
 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 :=
+  repeat lazymatch goal with
+  | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
+  end;
   apply hoist_pred_pureexec; intros; destruct_and?;
   apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
+Local Hint Resolve to_of_val.
 
-Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
+Instance pure_binop op e1 v1 e2 v2 v `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec (binop_eval op v1 v2 = Some v)
            (BinOp op e1 e2)
            (of_val v).
 Proof. solve_pureexec. Qed.
 
-Instance pure_rec f x e1 e2 v2 `{Closed ∅ (Rec f x e1)} `(to_val e2 = Some v2) :
+Instance pure_rec f x e1 e2 v2 `{Closed ∅ (Rec f x e1)} `{!IntoVal e2 v2} :
   PureExec True
            (App (Rec f x e1) e2)
            (subst' f (Rec f x e1) (subst' x e2 e1)).
 Proof. solve_pureexec. Qed.
 
 (* 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} :
+Instance pure_rec_locked e f x e1 e2 v2 `{!IntoVal e2 v2} `(e = Rec f x e1) `{Closed (x :b: f :b: ∅) e1} :
   PureExec True
            (App e e2)
            (e $/ v2) | 100.
 Proof.
   apply hoist_pred_pureexec; intros; destruct_and?;
-  apply det_head_step_pureexec. 
+  apply det_head_step_pureexec.
   - solve_exec_safe.
-  - destruct f; solve_exec_puredet.
+  - rewrite -(of_to_val e2 _ into_val).
+    destruct f; solve_exec_puredet.
 Qed.
 
-Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
+Instance pure_fst e1 v1 e2 v2 `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pureexec. Qed.
 
-Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
+Instance pure_snd e1 v1 e2 v2 `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pureexec. Qed.
 
-Instance pure_unfold e1 v1 `(to_val e1 = Some v1) :
+Instance pure_unfold e1 v1 `{!IntoVal e1 v1} :
   PureExec True (Unfold (Fold e1)) e1.
 Proof. solve_pureexec. Qed.
 
-Instance pure_unpack e1 e2 v1 `(to_val e1 = Some v1) :
+Instance pure_unpack e1 e2 v1 `{!IntoVal e1 v1} :
   PureExec True (Unpack (Pack e1) e2) (e2 e1).
 Proof. solve_pureexec. Qed.
 
@@ -55,11 +60,11 @@ Instance pure_if_false e1 e2 :
   PureExec True (If #false e1 e2) e2.
 Proof. solve_pureexec. Qed.
 
-Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2  :
+Instance pure_case_inl e0 v `{!IntoVal e0 v} e1 e2  :
   PureExec True (Case (InjL e0) e1 e2) (e1 e0).
 Proof. solve_pureexec. Qed.
 
-Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2  :
+Instance pure_case_inr e0 v `{!IntoVal e0 v} e1 e2  :
   PureExec True (Case (InjR e0) e1 e2) (e2 e0).
 Proof. solve_pureexec. Qed.
 

theories/F_mu_ref_conc/reflection.v

@@ -5,7 +5,7 @@ Import lang.
 Module R.
 Inductive expr :=
   | Val (v : lang.val) (e : lang.expr) (Hev : to_val e = Some v)
-  | ClosedExpr (e : lang.expr) `{Closed ∅ e}  
+  | ClosedExpr (e : lang.expr) `{Closed ∅ e}
   | Var (x : string)
   | Rec (f x : binder) (e : expr)
   | App (e1 e2 : expr)
@@ -101,7 +101,7 @@ Ltac of_expr e :=
   | lang.Fold ?e => let e := of_expr e in constr:(Fold e)
   | lang.Unfold ?e => let e := of_expr e in constr:(Unfold e)
   | lang.Pack ?e => let e := of_expr e in constr:(Pack e)
-  | lang.Unpack ?e ?e' => 
+  | lang.Unpack ?e ?e' =>
      let e := of_expr e in let e' := of_expr e' in constr:(Unpack e e')
   | lang.TLam ?e => let e := of_expr e in constr:(TLam e)
   | lang.TApp ?e => let e := of_expr e in constr:(TApp e)
@@ -127,8 +127,8 @@ Fixpoint is_closed (X : stringset) (e : expr) : bool :=
     is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
-  | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e 
-          | Load e  | Fold e | Unfold e | Pack e 
+  | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e
+          | Load e  | Fold e | Unfold e | Pack e
           | TLam e | TApp e => is_closed X e
   end.
 
@@ -169,7 +169,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
 Proof.
   revert X.
-  induction e; cbn; try naive_solver. 
+  induction e; cbn; try naive_solver.
   - intros. rewrite -(of_to_val _ _ Hev). eapply of_val_closed'.
   - intros. eapply is_closed_weaken; eauto. set_solver.
 Qed.
@@ -236,8 +236,6 @@ Ltac solve_to_val :=
      let e' := R.of_expr e in change (is_Some (to_val (R.to_expr e')));
      apply R.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
-Hint Extern 0 (to_val _ = Some _) => solve_to_val : typeclass_instances.
-Hint Extern 0 (is_Some (to_val _)) => solve_to_val : typeclass_instances.
 Hint Extern 0 (IntoVal _ _) => solve_to_val : typeclass_instances.
 
 Ltac solve_closed :=
@@ -268,7 +266,6 @@ Ltac solve_closed2 :=
   | _ => solve_closed
   end.
 Hint Extern 1 (Closed _ _) => solve_closed2 : typeclass_instances.
-(* Hint Extern 1 (Closed _ _) => solve_closed2. *)
 
 Ltac simpl_subst :=
   cbn[subst'];