From 37085f6484f6641be56f72d3254ecaa5fe2318ce Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sun, 18 Dec 2016 15:26:35 +0100
Subject: [PATCH] split old and new definitions in typing.typing

---
 _CoqProject                |  1 +
 theories/typing/function.v |  2 +-
 theories/typing/perm.v     |  2 ++
 theories/typing/programs.v | 34 ++++++++++++++++++++++++++++++++++
 theories/typing/typing.v   | 24 +-----------------------
 5 files changed, 39 insertions(+), 24 deletions(-)
 create mode 100644 theories/typing/programs.v

diff --git a/_CoqProject b/_CoqProject
index be0b3c39..81b76b77 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,4 +39,5 @@ theories/typing/sum.v
 theories/typing/bool.v
 theories/typing/int.v
 theories/typing/function.v
+theories/typing/programs.v
 theories/typing/mem_instructions.v
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 986660f7..5f220417 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing lft_contexts type_context cont_context.
+From lrust.typing Require Import programs lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index c097c0fc..da3c6472 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -3,6 +3,8 @@ From lrust.typing Require Export type.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow.
 
+(* TODO: This is all still using the outdated type system. *)
+
 Section perm.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
new file mode 100644
index 00000000..0034b183
--- /dev/null
+++ b/theories/typing/programs.v
@@ -0,0 +1,34 @@
+From iris.program_logic Require Import hoare.
+From iris.base_logic Require Import big_op.
+From lrust.lang Require Export notation memcpy.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm lft_contexts type_context cont_context.
+From lrust.lang Require Import proofmode.
+From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
+                        (e : expr) : iProp Σ :=
+    (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
+               WP e {{ _, cont_postcondition }})%I.
+
+  Instance typed_body_llctx_permut E :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
+  Proof.
+    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
+  Qed.
+
+  Instance typed_body_mono E L:
+    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
+  Proof.
+    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
+    iIntros (tid qE) "#LFT HE HL HC HT".
+    iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
+    iApply ("H" with "LFT HE HL [HC] HT").
+    iIntros "HE". by iApply (HC with "LFT HC").
+  Qed.
+
+End typing.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index a29d2cc2..3ea3ed1d 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -6,33 +6,11 @@ From lrust.typing Require Import perm lft_contexts type_context cont_context.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 
-(* TODO: Split this file into instructions.v and body.v. *)
+(* TODO: This is all still using the outdated type system. *)
 
 Section typing.
   Context `{typeG Σ}.
 
-  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
-                        (e : expr) : iProp Σ :=
-    (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
-               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
-               WP e {{ _, cont_postcondition }})%I.
-
-  Instance typed_body_llctx_permut E :
-    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
-  Proof.
-    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
-  Qed.
-
-  Instance typed_body_mono E L:
-    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
-  Proof.
-    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
-    iIntros (tid qE) "#LFT HE HL HC HT".
-    iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
-    iApply ("H" with "LFT HE HL [HC] HT").
-    iIntros "HE". by iApply (HC with "LFT HC").
-  Qed.
-
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
     ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e
-- 
GitLab