From e412af587d83c35c2ddf0e86eb19228449e4131b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 23 Feb 2017 15:59:10 +0100
Subject: [PATCH] Define the type option. Merge some examples in this file.

---
 _CoqProject                                   |  2 +-
 theories/typing/examples/get_x.v              |  2 +-
 theories/typing/examples/init_prod.v          |  2 +-
 theories/typing/examples/lazy_lft.v           |  2 +-
 theories/typing/examples/rebor.v              |  2 +-
 theories/typing/examples/unbox.v              |  2 +-
 theories/typing/examples/unwrap_or.v          | 30 ----------------
 .../{examples/option_as_mut.v => option.v}    | 36 ++++++++++++++++---
 theories/typing/unsafe/refcell/refcell_code.v | 26 +++++++-------
 9 files changed, 51 insertions(+), 53 deletions(-)
 delete mode 100644 theories/typing/examples/unwrap_or.v
 rename theories/typing/{examples/option_as_mut.v => option.v} (53%)

diff --git a/_CoqProject b/_CoqProject
index bc8a28e2..828e6d1f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,6 +45,7 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
 theories/typing/soundness.v
+theories/typing/option.v
 theories/typing/unsafe/cell.v
 theories/typing/unsafe/spawn.v
 theories/typing/unsafe/refcell/refcell.v
@@ -57,6 +58,5 @@ theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v
 theories/typing/examples/init_prod.v
-theories/typing/examples/option_as_mut.v
 theories/typing/examples/unwrap_or.v
 theories/typing/examples/lazy_lft.v
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index db14c7eb..e6c440cd 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 1d1eefc0..c307f3a9 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 96c2d0ee..16869ee6 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 99254956..67a7632b 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 0aeb0f71..4c99656e 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
deleted file mode 100644
index dcb45785..00000000
--- a/theories/typing/examples/unwrap_or.v
+++ /dev/null
@@ -1,30 +0,0 @@
-From iris.proofmode Require Export tactics.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unwrap_or.
-  Context `{typeG Σ}.
-
-  Definition unwrap_or Ï„ : val :=
-    funrec: <> ["o"; "def"] :=
-      case: !"o" of
-      [ delete [ #(S Ï„.(ty_size)); "o"];; "return" ["def"];
-        letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
-        delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];; "return" ["r"]].
-
-  Lemma unwrap_or_type Ï„ :
-    typed_instruction_ty [] [] [] (unwrap_or Ï„)
-        (fn([]; Σ[unit; τ], τ) → τ).
-  Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-      inv_vec p=>o def. simpl_subst.
-    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
-    + right. iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
-    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
-        simpl_subst.
-      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
-      iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
-  Qed.
-End unwrap_or.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/option.v
similarity index 53%
rename from theories/typing/examples/option_as_mut.v
rename to theories/typing/option.v
index 652d93ea..86ac155d 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/option.v
@@ -1,10 +1,12 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
-Section option_as_mut.
+Section option.
   Context `{typeG Σ}.
 
+  Definition option (τ : type) := Σ[unit; τ]%T.
+
   Definition option_as_mut : val :=
     funrec: <> ["o"] :=
       let: "o'" := !"o" in
@@ -17,7 +19,7 @@ Section option_as_mut.
 
   Lemma option_as_mut_type Ï„ :
     typed_instruction_ty [] [] [] option_as_mut
-        (fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
+        (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
       inv_vec p=>o. simpl_subst.
@@ -36,4 +38,30 @@ Section option_as_mut.
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
-End option_as_mut.
+
+  Definition option_unwrap_or Ï„ : val :=
+    funrec: <> ["o"; "def"] :=
+      case: !"o" of
+      [ delete [ #(S Ï„.(ty_size)); "o"];;
+        "return" ["def"];
+
+        letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
+        delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
+        "return" ["r"]].
+
+  Lemma option_unwrap_or_type Ï„ :
+    typed_instruction_ty [] [] [] (option_unwrap_or Ï„)
+        (fn([]; option τ, τ) → τ).
+  Proof.
+    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+      inv_vec p=>o def. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
+        simpl_subst.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
+  Qed.
+End option.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 5c7e4844..5a12ad7f 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing option.
 From lrust.typing.unsafe.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
@@ -130,14 +130,14 @@ Section refcell_functions.
       let: "x'" := !"x" in
       let: "n" := !"x'" in
       if: "n" ≤ #-1 then
-        "r" <-{Σ 1} ();;
+        "r" <-{Σ 0} ();;
         "k" ["r"] (* FIXME RJ: this is very confusing, "k" does not even look like it is bound here... *)
       else
         "x'" <- "n" + #1;;
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
+        "r" <-{2,Σ 1} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       cont: "k" ["r"] :=
@@ -145,12 +145,12 @@ Section refcell_functions.
 
   Lemma refcell_try_borrow_type ty :
     typed_instruction_ty [] [] [] refcell_try_borrow
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (ref α ty))%T).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
       inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[ref α ty; unit]])%TC);
+                                    r!!!0 ◁ box (option (ref α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
@@ -171,7 +171,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [ref α ty; unit]);
+      iApply (type_sum_assign_unit [unit; ref α ty]);
         [solve_typing..|by eapply write_own|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
@@ -223,7 +223,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_glb_mono. done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [ref α ty; unit]);
+      iApply (type_sum_memcpy [unit; ref α ty]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
@@ -240,23 +240,23 @@ Section refcell_functions.
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
+        "r" <-{2,Σ 1} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       else
-        "r" <-{Σ 1} ();;
+        "r" <-{Σ 0} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_instruction_ty [] [] [] refcell_try_borrow_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (refmut α ty))%T).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
       inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[refmut α ty; unit]])%TC);
+                                    r!!!0 ◁ box (option (refmut α ty))]%TC));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
@@ -295,7 +295,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_glb_mono; first done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [refmut α ty; unit]);
+      iApply (type_sum_memcpy [unit; refmut α ty]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
@@ -306,7 +306,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [refmut α ty; unit]);
+      iApply (type_sum_assign_unit [unit; refmut α ty]);
         [solve_typing..|by eapply write_own|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
-- 
GitLab