Typechecking unwrap_or.

_CoqProject

@@ -48,4 +48,5 @@ theories/typing/tests/rebor.v
 theories/typing/tests/unbox.v
 theories/typing/tests/init_prod.v
 theories/typing/tests/option_as_mut.v
+theories/typing/tests/unwrap_or.v
 theories/typing/unsafe/cell.v

theories/typing/lft_contexts.v

@@ -444,8 +444,8 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
    [tctx_extract_hasty] to suceed even if the type is an evar, and
    merging makes it diverge in this case. *)
 Ltac solve_typing :=
-  (eauto 100 with lrust_typing typeclass_instances lia; fail) ||
-  (eauto 100 with lrust_typing lrust_typing_merge typeclass_instances lia; fail).
+  (eauto 100 with lrust_typing typeclass_instances; fail) ||
+  (eauto 100 with lrust_typing lrust_typing_merge typeclass_instances; fail).
 Create HintDb lrust_typing_merge.
 
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.

theories/typing/own.v

@@ -240,7 +240,7 @@ Section typing.
     rewrite freeable_sz_full. by iFrame.
   Qed.
 
-  Lemma type_delete E L C T T' (n' : nat) ty (n : Z)  p e :
+  Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
     Closed [] e →
     tctx_extract_hasty E L p (own n' ty) T T' →
     n = n' → Z.of_nat (ty.(ty_size)) = n →
@@ -307,3 +307,7 @@ Section typing.
 End typing.
 
 Hint Resolve own_mono' own_proper' : lrust_typing.
+
+Hint Extern 100 (_ ≤ _) => simpl; lia : lrust_typing.
+Hint Extern 100 (@eq Z _ _) => simpl; lia : lrust_typing.
+Hint Extern 100 (@eq nat _ _) => simpl; lia : lrust_typing.
\ No newline at end of file

theories/typing/tests/get_x.v

@@ -15,14 +15,13 @@ Section get_x.
 
   Lemma get_x_type :
     typed_instruction_ty [] [] [] get_x
-        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Π[int; int])])
-            (λ α, own 1 (&shr{α} int))).
+        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}Π[int; int])]) (λ α, box (&shr{α} int))).
   Proof.
     apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
-    eapply type_deref; try solve_typing. by apply read_own_move. done.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
       intros p'; simpl_subst.
-    eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
-    eapply type_delete; try solve_typing.
+    eapply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]=>r. simpl_subst.
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
 End get_x.

theories/typing/tests/init_prod.v

@@ -16,19 +16,18 @@ Section rebor.
 
   Lemma init_prod_type :
     typed_instruction_ty [] [] [] init_prod
-        (fn (λ _, []) (λ _, [# own 1 int; own 1 int])
-            (λ (_ : ()), own 2 (Π[int;int]))).
+        (fn (λ _, []) (λ _, [# box int; box int]) (λ (_ : ()), box (Π[int;int]))).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
-    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
-    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>y'. simpl_subst.
+    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
+    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
     eapply (type_new_subtype (Π[uninit 1; uninit 1])); [apply _|done| |].
       { apply (uninit_product_subtype [] [] [1;1]%nat). }
       intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
-    eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own.
-    eapply type_assign; try solve_typing. by apply write_own.
-    eapply type_delete; try solve_typing.
-    eapply type_delete; try solve_typing.
+    eapply (type_assign (own 2 (uninit 1))); [solve_typing..|by apply write_own|].
+    eapply type_assign; [solve_typing..|by apply write_own|].
+    eapply type_delete; [solve_typing..|].
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
 End rebor.

theories/typing/tests/option_as_mut.v

@@ -7,34 +7,31 @@ Set Default Proof Using "Type".
 Section option_as_mut.
   Context `{typeG Σ}.
 
-  Definition option_as_mut :=
-    (funrec: <> ["o"] :=
-       let: "o'" := !"o" in case: !"o'" of
-       [ let: "r" := new [ #2 ] in "r" <-{0} ☇;;
-         "k" ["r"];
-         let: "r" := new [ #2 ] in "r" <-{1} "o'" +ₗ #1;;
-         "k" ["r"] ]
-       cont: "k" ["r"] :=
-         delete [ #1; "o"];; "return" ["r"])%E.
+  Definition option_as_mut : val :=
+    funrec: <> ["o"] :=
+      let: "o'" := !"o" in case: !"o'" of
+        [ let: "r" := new [ #2 ] in "r" <-{0} ☇;; "k" ["r"];
+          let: "r" := new [ #2 ] in "r" <-{1} "o'" +ₗ #1;; "k" ["r"] ]
+      cont: "k" ["r"] :=
+        delete [ #1; "o"];; "return" ["r"].
 
   Lemma option_as_mut_type τ :
     typed_instruction_ty [] [] [] option_as_mut
-        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Σ[unit; τ])])
-            (λ α, own 2 (Σ[unit; &uniq{α}τ]))).
+        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}Σ[unit; τ])]) (λ α, box (Σ[unit; &uniq{α}τ]))).
   Proof.
     apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; try solve_typing.
+    eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
     - intros k. simpl_subst.
-      eapply type_deref; try solve_typing; [apply read_own_move|done|]=>o'. simpl_subst.
-      eapply type_case_uniq; try solve_typing. constructor; last constructor; last constructor.
-      + left. eapply type_new; try solve_typing. intros r. simpl_subst.
-        eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
+      eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
+      eapply type_case_uniq; [solve_typing..|]. constructor; last constructor; last constructor.
+      + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
+        eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
         eapply (type_jump [_]); solve_typing.
-      + left. eapply type_new; try solve_typing. intros r. simpl_subst.
-        eapply (type_sum_assign [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
+      + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
+        eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
         eapply (type_jump [_]); solve_typing.
     - move=>/= k r. inv_vec r=>r. simpl_subst.
-      eapply type_delete; try solve_typing.
+      eapply type_delete; [solve_typing..|].
       eapply (type_jump [_]); solve_typing.
   Qed.
 End option_as_mut.

theories/typing/tests/rebor.v

@@ -20,22 +20,21 @@ Section rebor.
 
   Lemma rebor_type :
     typed_instruction_ty [] [] [] rebor
-        (fn (λ _, []) (λ _, [# own 2 (Π[int; int]); own 2 (Π[int; int])])
-            (λ (_ : ()), own 1 int)).
+        (fn (λ _, []) (λ _, [# box (Π[int; int]); box (Π[int; int])])
+            (λ (_ : ()), box int)).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
     eapply (type_newlft []). apply _. move=> α.
-    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); (try solve_typing)=>x. simpl_subst.
-    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
-    eapply (type_letpath (&uniq{α}int)); (try solve_typing)=>y. simpl_subst.
-    eapply (type_assign _ (&uniq{α}Π [int; int])); try solve_typing. by apply write_own.
-    eapply type_deref; try solve_typing; [apply: read_uniq; solve_typing|done|]=>y'.
-      simpl_subst.
-    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
-    eapply type_endlft; try solve_typing.
-    eapply type_delete; try solve_typing.
-    eapply type_delete; try solve_typing.
-    eapply type_delete; try solve_typing.
+    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]=>x. simpl_subst.
+    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
+    eapply (type_letpath (&uniq{α}int)); [solve_typing..|]=>y. simpl_subst.
+    eapply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|by apply write_own|].
+    eapply type_deref; [solve_typing..|apply: read_uniq; solve_typing|done|]=>y'. simpl_subst.
+    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
+    eapply type_endlft; [solve_typing..|].
+    eapply type_delete; [solve_typing..|].
+    eapply type_delete; [solve_typing..|].
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
 End rebor.

theories/typing/tests/unbox.v

@@ -15,15 +15,14 @@ Section unbox.
 
   Lemma ubox_type :
     typed_instruction_ty [] [] [] unbox
-        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}own 2 (Π[int; int]))])
-            (λ α, own 1 (&uniq{α} int))).
+        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}box (Π[int; int]))]) (λ α, box (&uniq{α} int))).
   Proof.
     apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
-    eapply type_deref; try solve_typing. by apply read_own_move. done.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
     intros b'; simpl_subst.
-    eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
-    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
-    eapply type_delete; try solve_typing.
+    eapply type_deref_uniq_own; [solve_typing..|]=>bx; simpl_subst.
+    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
 End unbox.

theories/typing/tests/unwrap_or.v

+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+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 (λ _, [])%EL (λ _, [# box (Σ[unit; τ]); box τ]) (λ _:(), box τ)).
+  Proof.
+    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
+    eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
+    + right. eapply type_delete; [solve_typing..|].
+      eapply (type_jump [_]); solve_typing.
+    + left. eapply type_letalloc_n; [solve_typing..|by apply read_own_move|solve_typing|]=>r.
+        simpl_subst.
+      eapply (type_delete (Π[_;_;_])); [solve_typing..|].
+      eapply type_delete; [solve_typing..|].
+      eapply (type_jump [_]); solve_typing.
+  Qed.
+End unwrap_or.

theories/typing/type_context.v

@@ -363,5 +363,6 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
    the environment if the type is copy. But due to a bug in Coq, we
    cannot enforce this using [Hint Resolve]. Cf:
        https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
-Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
+Hint Extern 2 (tctx_extract_hasty _ _ ?p1 _ ((?p2 ◁ _) :: _) _) =>
+  unify p1 p2;
   eapply tctx_extract_hasty_here_eq : lrust_typing.

theories/typing/unsafe/cell.v

@@ -77,7 +77,7 @@ Section typing.
   Lemma read_cell E L κ ty :
     Copy ty → lctx_lft_alive E L κ →
     typed_read E L (&shr{κ} cell ty) ty (&shr{κ} cell ty).
-  Proof. intros ??. exact: read_shr. Qed. 
+  Proof. intros ??. exact: read_shr. Qed.
 
   (* Writing actually needs code; typed_write can't have thread tokens. *)
   Definition cell_write ty : val :=
@@ -93,7 +93,7 @@ Section typing.
             (λ α, box unit)).
   Proof.
     apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
-    eapply type_deref; try solve_typing. by apply read_own_move. done.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
     intros c'. simpl_subst.
     eapply type_let with (T1 := [c' ◁ _; x ◁ _]%TC)
                          (T2 := λ _, [c' ◁ &shr{α} cell ty;
@@ -121,8 +121,7 @@ Section typing.
       - iExists _. iSplit; first done. iFrame. iExists _. iFrame.
         rewrite uninit_own. auto. }
     intros v. simpl_subst. clear v.
-    eapply (type_new_subtype unit); try solve_typing. try done.
-    { apply uninit_unit. }
+    eapply (type_new_subtype unit); [solve_typing..|apply uninit_unit|].
     intros r. simpl_subst.
     eapply type_delete; [solve_typing..|].
     eapply type_delete; [solve_typing..|].