From 7726a27bb6ee6b89e1f4333bef098357ca0b8cf0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Jan 2017 15:30:48 +0100
Subject: [PATCH] Trying to clarify priorities of mergeing and splitting
 lemmas. Clearly, this is still not optimal.

---
 opam.pins                       |  2 +-
 theories/typing/lft_contexts.v  | 11 ++++++++++-
 theories/typing/product_split.v | 27 ++++++++++++++++++++++-----
 theories/typing/tests/unbox.v   |  2 +-
 theories/typing/type_context.v  |  2 +-
 5 files changed, 35 insertions(+), 9 deletions(-)

diff --git a/opam.pins b/opam.pins
index 16be4581..cbfb3aa0 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 587cde167492b4b25f1d11ca7797c2087527abd6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq be81fb92a76f31ca656f8dad37122843f58884cf
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index eec88edf..aab3d1c2 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -437,7 +437,16 @@ End elctx_incl.
 
 Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 
-Ltac solve_typing := eauto 100 with lrust_typing typeclass_instances || fail.
+(* We first try to solve everything without the merging rules, and
+   then start from scratch with them.
+
+   The reason is that we want we want the search proof search for
+   [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; 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.
 Hint Resolve
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a6a3262f..154dca9f 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -388,14 +388,31 @@ Section product_split.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
 End product_split.
 
-(* We make sure that splitting and merging are applied after everything else. *)
+(* We make sure that splitting is tried before borrowing, so that not
+   the entire product is borrowed when only a part is needed. *)
 Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
              tctx_extract_split_shr_prod2 tctx_extract_split_own_prod
              tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
-             tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2
-             tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod
-             tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
-     | 100 : lrust_typing.
+    | 5 : lrust_typing.
+
+(* Merging is also tried after everything, except
+   [tctx_extract_hasty_further]. Moreover, it is placed in a
+   difference hint db. The reason is that it can make the proof search
+   diverge if the type is an evar. *)
+(* We declare them as [Hint Extern] instead of [Hint Resolve],
+   otherwise unification with unrelated goals takes forever to fail... *)
+Hint Extern 40 (tctx_extract_hasty _ _ _ (own _ (product2 _ _)) _ _) =>
+  eapply tctx_extract_merge_own_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&uniq{_}product2 _ _) _ _) =>
+  eapply tctx_extract_merge_uniq_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&shr{_}product2 _ _) _ _) =>
+  eapply tctx_extract_merge_shr_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (own _ (Π _)) _ _) =>
+  eapply tctx_extract_merge_own_prod : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&uniq{_}Π _) _ _) =>
+  eapply tctx_extract_merge_uniq_prod : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&shr{_}Π _) _ _) =>
+  eapply tctx_extract_merge_shr_prod : lrust_typing_merge.
 
 Hint Extern 0
      (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index 73a22b1a..aca132b1 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -22,7 +22,7 @@ Section unbox.
     eapply type_deref; try 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 (&uniq{α}int)); (try solve_typing)=>r. simpl_subst.
+    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.
     eapply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index d9844bd9..d0ac76e0 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -364,4 +364,4 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
    cannot enforce this using [Hint Resolve]. Cf:
        https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
 Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
-  eapply tctx_extract_hasty_here_eq.
+  eapply tctx_extract_hasty_here_eq : lrust_typing.
-- 
GitLab