Skip to content
Snippets Groups Projects
Commit 43c18fa6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge commit '7726a27b'

parents 2d791b59 7726a27b
No related branches found
No related tags found
No related merge requests found
...@@ -437,7 +437,16 @@ End elctx_incl. ...@@ -437,7 +437,16 @@ End elctx_incl.
Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL. 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 Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve Hint Resolve
......
...@@ -388,14 +388,31 @@ Section product_split. ...@@ -388,14 +388,31 @@ Section product_split.
Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed. Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
End product_split. 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 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_shr_prod2 tctx_extract_split_own_prod
tctx_extract_split_uniq_prod tctx_extract_split_shr_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2 | 5 : lrust_typing.
tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod
tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod (* Merging is also tried after everything, except
| 100 : lrust_typing. [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 Hint Extern 0
(tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) => (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
......
...@@ -22,7 +22,7 @@ Section unbox. ...@@ -22,7 +22,7 @@ Section unbox.
eapply type_deref; try solve_typing. by apply read_own_move. done. eapply type_deref; try solve_typing. by apply read_own_move. done.
intros b'; simpl_subst. intros b'; simpl_subst.
eapply type_deref_uniq_own; (try solve_typing)=>bx; 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_delete; try solve_typing.
eapply (type_jump [_]); solve_typing. eapply (type_jump [_]); solve_typing.
Qed. Qed.
......
...@@ -364,4 +364,4 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons ...@@ -364,4 +364,4 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
cannot enforce this using [Hint Resolve]. Cf: cannot enforce this using [Hint Resolve]. Cf:
https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *) https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ _) :: _) _) => Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ _) :: _) _) =>
eapply tctx_extract_hasty_here_eq. eapply tctx_extract_hasty_here_eq : lrust_typing.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment