From 6f46c73c6227ef5674efa4a75019088e491cceb0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 7 Jan 2017 21:06:38 +0100
Subject: [PATCH] Fix build : forgot a file. Also, some tweaks to simplify the
 proofs.

---
 theories/typing/cont.v        |  2 +-
 theories/typing/own.v         |  2 +-
 theories/typing/tests/get_x.v |  2 +-
 theories/typing/tests/rebor.v | 41 +++++++++++++++++++++++++++++++++++
 4 files changed, 44 insertions(+), 3 deletions(-)
 create mode 100644 theories/typing/tests/rebor.v

diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 3d4398a3..c2826427 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -8,7 +8,7 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  Lemma type_jump E L C T k args T' :
+  Lemma type_jump args E L C T k T' :
     (k ◁cont(L, T'))%CC ∈ C →
     tctx_incl E L T (T' (list_to_vec args)) →
     typed_body E L C T (k (of_val <$> args)).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 7211456e..22a3cd27 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -235,9 +235,9 @@ Section typing.
   Qed.
 
   Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
-    ty.(ty_size) = 1%nat →
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
+    ty.(ty_size) = 1%nat →
     (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x := p in e).
   Proof.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index 61ba2c29..cc8982e4 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -23,6 +23,6 @@ Section get_x.
       intros p'; simpl_subst.
     eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.
-    eapply type_jump with (args := [r]); solve_typing.
+    eapply (type_jump [_]); solve_typing.
   Qed.
 End get_x.
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
new file mode 100644
index 00000000..cae48c5a
--- /dev/null
+++ b/theories/typing/tests/rebor.v
@@ -0,0 +1,41 @@
+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.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition rebor :=
+    (funrec: <> ["t1"; "t2"] :=
+       Newlft;;
+       letalloc: "x" := "t1" in
+       let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
+       "x" <- "t2";;
+       let: "y'" := !"y" in
+       letalloc: "r" := "y'" in
+       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
+                 delete [ #1; "x"] ;; "return" ["r":expr])%E.
+
+  Lemma rebor_type :
+    typed_instruction_ty [] [] [] rebor
+        (fn (λ _, []) (λ _, [# own 2 (Π[int; int]); own 2 (Π[int; int])])
+            (λ (_ : ()), own 1 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_jump [_]); solve_typing.
+  Qed.
+End rebor.
-- 
GitLab