From 9e8004f8b88f55bde5e70f3c881913995d224bc7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Aug 2019 13:13:22 +0200
Subject: [PATCH] prepare for having fractional arrays in the future

---
 tests/heap_lang.ref        | 10 ++++++++++
 tests/heap_lang.v          |  5 ++++-
 theories/heap_lang/array.v | 22 ++++------------------
 3 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index eaaa3c963..5c56f67f3 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
+The command has indeed failed with message:
+In nested Ltac calls to "iIntros (constr)", "iIntros_go",
+"iDestructHyp (constr) as (constr)",
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
+"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
+"iAndDestruct (constr) as (constr) (constr)", last call failed.
+Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 9d7f906bb..ace305987 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -158,7 +158,10 @@ Section tests.
   Lemma test_array_app l vs1 vs2 :
     l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
   Proof.
-    iIntros "[H1 H2]". iSplitL "H1"; done.
+    Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
+    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
+    Fail iSplitL "H1".
+    iApply array_app. iSplitL "H1"; done.
   Qed.
 
 End tests.
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index c7dee7696..32cd79f3b 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -61,24 +61,8 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
-(** Proofmode instances *)
-Global Instance into_sep_array_cons l vs v vs' :
-  IsCons vs v vs' →
-  IntoSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
-Proof. rewrite /IsCons=>->. by rewrite /IntoSep array_cons. Qed.
-Global Instance into_sep_array_app l vs vs1 vs2 :
-  IsApp vs vs1 vs2 →
-  IntoSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
-Proof. rewrite /IsApp=>->. by rewrite /IntoSep array_app. Qed.
-
-Global Instance from_sep_array_cons l vs v vs' :
-  IsCons vs v vs' →
-  FromSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
-Proof. rewrite /IsCons=> ->. by rewrite /FromSep array_cons. Qed.
-Global Instance from_sep_array_app l vs vs1 vs2 :
-  IsApp vs vs1 vs2 →
-  FromSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
-Proof. rewrite /IsApp=> ->. by rewrite /FromSep array_app. Qed.
+(** No [FromSep] or [IntoSep] instances to remain forwards compatible with a
+fractional array assertion, that will split the fraction, not the list. *)
 
 (** Allocation *)
 Lemma mapsto_seq_array l v n :
@@ -240,3 +224,5 @@ Proof.
 Qed.
 
 End lifting.
+
+Typeclasses Opaque array.
-- 
GitLab