From ecdbf1313be05ddc56f8ff3ef30f8cfedf412012 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Apr 2018 17:37:52 +0200
Subject: [PATCH] Use AsVal.

---
 theories/lang/lib/spawn.v                 |  2 +-
 theories/lang/races.v                     |  9 ++++-----
 theories/typing/function.v                |  6 +++---
 theories/typing/lib/arc.v                 |  2 +-
 theories/typing/lib/diverging_static.v    |  2 --
 theories/typing/lib/join.v                | 10 +++-------
 theories/typing/lib/rc/rc.v               |  2 +-
 theories/typing/lib/refcell/ref_code.v    |  2 +-
 theories/typing/lib/refcell/refmut_code.v |  3 +--
 theories/typing/lib/spawn.v               |  9 ++++-----
 theories/typing/lib/take_mut.v            |  2 +-
 11 files changed, 20 insertions(+), 29 deletions(-)

diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 81a8fbbe..8e270f00 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -62,7 +62,7 @@ Proof. solve_proper. Qed.
 
 (** The main proofs. *)
 Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
-  to_val e = Some f →
+  IntoVal e f →
   {{{ ∀ c, finish_handle c Ψ -∗ WP f [ #c] {{ _, True }} }}}
     spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
 Proof.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index c508147f..834b8db7 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -12,14 +12,14 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
 | Access_read ord l σ :
     next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
 | Access_write ord l e σ :
-    is_Some (to_val e) →
+    AsVal e →
     next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
 | Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
     lit_neq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
 | Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
     lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
 | Access_free n l σ i :
@@ -106,8 +106,7 @@ Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 a l :
   head_step e1 σ1 e2 σ2 ef →
   next_access_head e2 σ2 (a, Na2Ord) l.
 Proof.
-  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor.
-  by rewrite to_of_val.
+  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; apply _.
 Qed.
 
 Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 23125772..69362f45 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -245,7 +245,7 @@ Section typing.
   Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qL tid
         p (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
-    is_Some (to_val k) →
+    AsVal k →
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L qL -∗
     qκs.[lft_intersect_list κs] -∗
     tctx_elt_interp tid (p ◁ fn fp) -∗
@@ -304,7 +304,7 @@ Section typing.
   Lemma type_call_iris E (κs : list lft) {A} x (ps : list path) qκs tid
         f (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) [] ((fp x).(fp_E) ϝ)) →
-    is_Some (to_val k) →
+    AsVal k →
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
     qκs.[lft_intersect_list κs] -∗
     (fn fp).(ty_own) tid [f] -∗
@@ -333,7 +333,7 @@ Section typing.
   Proof.
     iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
     iMod (lctx_lft_alive_tok_list _ _ κs with "HE HL") as (q) "(Hκs & HL & Hclose)"; [done..|].
-    iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|solve_to_val|].
+    iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|].
     iIntros (r) "Htl HL Hκs Hret". iMod ("Hclose" with "Hκs HL") as "HL".
     iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
     iApply ("HC" $! [#r] with "Htl HL").
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index bb28917b..afbdf5cb 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1078,7 +1078,7 @@ Section arc.
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
       rewrite -[α ⊓ ν](right_id_L).
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_] with
-              "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing|solve_to_val| |].
+              "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
         iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index e34687af..6926982a 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -42,7 +42,6 @@ Section diverging_static.
     wp_let. rewrite tctx_hasty_val.
     iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
     - solve_typing.
-    - solve_to_val.
     - by rewrite /= (right_id static).
     - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
       iApply "Hincl". done.
@@ -55,5 +54,4 @@ Section diverging_static.
       + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
       + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
   Qed.
-
 End diverging_static.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index beb8ebef..b11f27ef 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -49,14 +49,12 @@ Section join.
       [solve_typing..|].
     (* FIXME: using wp_apply here breaks calling solve_to_val. *)
     wp_bind (spawn _).
-    iApply ((spawn_spec joinN (λ v, (box R_A).(ty_own) tid [v] ∗ (qϝ1).[ϝ])%I) with "[HfA HenvA Hϝ1]");
-      first solve_to_val; first simpl_subst.
+    iApply ((spawn_spec joinN (λ v, (box R_A).(ty_own) tid [v] ∗ (qϝ1).[ϝ])%I) with "[HfA HenvA Hϝ1]").
     { (* The new thread. *)
-      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let. unlock.
-      rewrite !tctx_hasty_val.
+      simpl_subst. iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let.
+      wp_let. unlock. rewrite !tctx_hasty_val.
       iApply (type_call_iris _ [ϝ] () [_] with "LFT HE Htl [Hϝ1] HfA [HenvA]").
       - rewrite outlives_product. solve_typing.
-      - solve_to_val.
       - by rewrite /= (right_id static).
       - by rewrite big_sepL_singleton tctx_hasty_val send_change_tid.
       - iIntros (r) "Htl Hϝ1 Hret".
@@ -68,7 +66,6 @@ Section join.
     rewrite !tctx_hasty_val.
     iApply (type_call_iris _ [ϝ] () [_] with "LFT HE Hna [Hϝ2] HfB [HenvB]").
     { rewrite outlives_product. solve_typing. }
-    { solve_to_val. }
     { by rewrite /= (right_id static). }
     { by rewrite big_sepL_singleton tctx_hasty_val. }
     (* The return continuation after calling fB in the main thread. *)
@@ -90,5 +87,4 @@ Section join.
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
-
 End join.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 83548b9c..c798b046 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1084,7 +1084,7 @@ Section code.
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
       rewrite -[α ⊓ ν](right_id_L).
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
-              with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing|solve_to_val| |].
+              with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
         iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 68de6e06..b37cfeb5 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -239,7 +239,7 @@ Section ref_functions.
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
     rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
-       with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|solve_to_val|done| |].
+       with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
       iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index b01bdafd..ccb739e1 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -185,8 +185,7 @@ Section refmut_functions.
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
     rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
-            with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]");
-      [solve_typing|solve_to_val|done| |].
+            with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
       iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index ec47a280..c9a91819 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -94,15 +94,14 @@ Section spawn.
                      (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
       iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]". rewrite !tctx_hasty_val [fn _]lock.
-      iApply (spawn_spec _ (join_inv tid retty) with "[-]");
-                              first solve_to_val; last first; last simpl_subst.
+      iApply (spawn_spec _ (join_inv tid retty) with "[-]"); last first.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
-      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let. unlock.
-      iApply (type_call_iris _ [] () [_] with "LFT HE Htl [] Hf' [Henv]");
+      simpl_subst. iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
+      unlock. iApply (type_call_iris _ [] () [_] with "LFT HE Htl [] Hf' [Henv]");
       (* The `solve_typing` here shows that, because we assume that `fty` and `retty`
          outlive `static`, the implicit requirmeents made by `call_once` are satisifed. *)
-        [solve_typing|solve_to_val|iApply (lft_tok_static 1%Qp)| |].
+        [solve_typing|iApply (lft_tok_static 1%Qp)| |].
       - by rewrite big_sepL_singleton tctx_hasty_val send_change_tid.
       - iIntros (r) "Htl _ Hret".
         wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index af60ddb0..8d9b75a9 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -43,7 +43,7 @@ Section code.
     (* Call the function. *)
     wp_let. unlock.
     iApply (type_call_iris _ [ϝ] () [_; _]
-      with "LFT HE Hna [Hϝ] Hf' [Henv Htl Htl† Hx'vl]"); [solve_typing|solve_to_val| | |].
+      with "LFT HE Hna [Hϝ] Hf' [Henv Htl Htl† Hx'vl]"); [solve_typing| | |].
     { by rewrite /= (right_id static). }
     { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
     (* Prove the continuation of the function call. *)
-- 
GitLab