diff --git a/_CoqProject b/_CoqProject
index 2a2e2fbfc014816e63870e54bc92640b7dae8958..d25c14ab402b17a7bfcc097392e40b753158cdf1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -49,4 +49,5 @@ theories/typing/tests/unbox.v
theories/typing/tests/init_prod.v
theories/typing/tests/option_as_mut.v
theories/typing/tests/unwrap_or.v
+theories/typing/tests/lazy_lft.v
theories/typing/unsafe/cell.v
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index c627aa1a8139f06dcaca025c12c005940fa164fa..1277ca81954e3c75892403a9623dc010a470c717 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -25,7 +25,7 @@ Section typing.
rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
Qed.
- Lemma typed_bool (b : Datatypes.bool) E L C T x e :
+ Lemma type_bool (b : Datatypes.bool) E L C T x e :
Closed (x :b: []) e →
(∀ (v : val), typed_body E L C ((v ◠bool) :: T) (subst' x v e)) →
typed_body E L C T (let: x := #b in e).
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 30ad25cddaae4af527e66fb55ab3325e295b5b0e..637fb1e5c00b42ffdde58f71f1a9fb497105f532 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -24,7 +24,7 @@ Section typing.
rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
Qed.
- Lemma typed_int (z : Z) E L C T x e :
+ Lemma type_int (z : Z) E L C T x e :
Closed (x :b: []) e →
(∀ (v : val), typed_body E L C ((v ◠int) :: T) (subst' x v e)) →
typed_body E L C T (let: x := #z in e).
@@ -45,7 +45,7 @@ Section typing.
iExists _. done.
Qed.
- Lemma typed_plus E L C T T' p1 p2 x e :
+ Lemma type_plus E L C T T' p1 p2 x e :
Closed (x :b: []) e →
tctx_extract_ctx E L [p1 ◠int; p2 ◠int] T T' →
(∀ (v : val), typed_body E L C ((v ◠int) :: T') (subst' x v e)) →
@@ -67,7 +67,7 @@ Section typing.
iExists _. done.
Qed.
- Lemma typed_minus E L C T T' p1 p2 x e :
+ Lemma type_minus E L C T T' p1 p2 x e :
Closed (x :b: []) e →
tctx_extract_ctx E L [p1 ◠int; p2 ◠int] T T' →
(∀ (v : val), typed_body E L C ((v ◠int) :: T') (subst' x v e)) →
@@ -89,7 +89,7 @@ Section typing.
iExists _; done.
Qed.
- Lemma typed_le E L C T T' p1 p2 x e :
+ Lemma type_le E L C T T' p1 p2 x e :
Closed (x :b: []) e →
tctx_extract_ctx E L [p1 ◠int; p2 ◠int] T T' →
(∀ (v : val), typed_body E L C ((v ◠bool) :: T') (subst' x v e)) →
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index aab3d1c2f56e98c5a1d3845c8af2f1593d0ae739..23c75dd3416173f08fafeae0f24f4f92f7c6c428 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -444,9 +444,10 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
[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.
+ (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
+ (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
+Create HintDb lrust_typing discriminated.
+Create HintDb lrust_typing_merge discriminated.
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve
@@ -456,9 +457,10 @@ Hint Resolve
elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl
elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
: lrust_typing.
-
Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
+Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
+
Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index dce282b4072ed5075cd5bac4c9e8f6b310d8c405..320943b20fe45ad3bb2d4aa260663658dc961591 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -389,6 +389,10 @@ Section product_split.
Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
End product_split.
+(* We do not want unification to try to unify the definition of these
+ types with anything in order to try splitting or merging. *)
+Hint Opaque own uniq_bor shr_bor product product2 tctx_extract_hasty : lrust_typing lrust_typing_merge.
+
(* 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
@@ -399,26 +403,15 @@ Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
(* 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 _ _ _ _) _) =>
- cbn[hasty_ptr_offsets].
-
-Hint Extern 0 (tctx_extract_hasty _ _ _ _ (_ ++ _) _) => cbn[app].
-
-Hint Unfold extract_tyl : lrust_typing.
+ diverge if the type is an evar.
+
+ Unfortunately, priorities are not taken into account accross hint
+ databases with [typeclasses eauto], so this is useless, and some
+ solve_typing get slow because of that. See:
+ https://coq.inria.fr/bugs/show_bug.cgi?id=5304
+*)
+Hint Resolve 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
+ | 40 : lrust_typing_merge.
+Hint Unfold extract_tyl.
\ No newline at end of file
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 4b80f653f17a1fd8c92d225d2807770a7ae25705..4e971178e059201ba3112933db13a62112bedae3 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -22,7 +22,7 @@ Section rebor.
eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
eapply (type_new_subtype (Î [uninit 1; uninit 1])); [apply _|done| |].
- { apply (uninit_product_subtype [] [] [1;1]%nat). }
+ { apply (uninit_product_subtype [1;1]%nat). }
intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
eapply (type_assign (own 2 (uninit 1))); [solve_typing..|by apply write_own|].
eapply type_assign; [solve_typing..|by apply write_own|].
diff --git a/theories/typing/tests/unwrap_or.v b/theories/typing/tests/unwrap_or.v
index 0cad6ef1baa95130d5f9b81be4536bf9d4f3aa11..b1c2724c6587c7285cb0fefd7ece87454c9eb209 100644
--- a/theories/typing/tests/unwrap_or.v
+++ b/theories/typing/tests/unwrap_or.v
@@ -24,7 +24,7 @@ Section unwrap_or.
eapply (type_jump [_]); solve_typing.
+ left. eapply type_letalloc_n; [solve_typing..|by apply read_own_move|solve_typing|]=>r.
simpl_subst.
- eapply (type_delete (Î [_;_;_])); [solve_typing..|].
+ eapply (type_delete (Î [uninit _;uninit _;uninit _])); [solve_typing..|].
eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing.
Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 31c53a2ba69ac68706f8e9afea4cd88d16030cca..2d93fdd78bafbbd77d97ee41b3d2bdc60c97bdc5 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -452,3 +452,4 @@ Section weakening.
End weakening.
Hint Resolve subtype_refl eqtype_refl : lrust_typing.
+Hint Opaque subtype eqtype : lrust_typing.
\ No newline at end of file
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 884473c3dba9a1774bf08b62a1913a979b795881..6989b31e27137a248385d103a3e54a269c899e57 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -259,22 +259,22 @@ Section type_context.
tctx_extract_hasty E L p ty T T' →
tctx_extract_hasty E L p ty (x::T) (x::T').
Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, submseteq_swap. Qed.
- Lemma tctx_extract_hasty_here_copy E L p ty ty' T `{!Copy ty} :
- subtype E L ty ty' →
- tctx_extract_hasty E L p ty' ((p â— ty)::T) ((p â— ty)::T).
+ Lemma tctx_extract_hasty_here_copy E L p1 p2 ty ty' T :
+ p1 = p2 → Copy ty → subtype E L ty ty' →
+ tctx_extract_hasty E L p1 ty' ((p2 â— ty)::T) ((p2 â— ty)::T).
Proof.
- intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+ intros -> ??. apply (tctx_incl_frame_r _ [_] [_;_]).
etrans; first by apply copy_tctx_incl, _.
by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
Qed.
- Lemma tctx_extract_hasty_here E L p ty ty' T :
- subtype E L ty ty' → tctx_extract_hasty E L p ty' ((p ◠ty)::T) T.
+ Lemma tctx_extract_hasty_here E L p1 p2 ty ty' T :
+ p1 = p2 → subtype E L ty ty' → tctx_extract_hasty E L p1 ty' ((p2 ◠ty)::T) T.
Proof.
- intros. by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
+ intros -> ?. by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
Qed.
- Lemma tctx_extract_hasty_here_eq E L p ty T :
- tctx_extract_hasty E L p ty ((p â— ty)::T) T.
- Proof. by apply tctx_extract_hasty_here. Qed.
+ Lemma tctx_extract_hasty_here_eq E L p1 p2 ty T :
+ p1 = p2 → tctx_extract_hasty E L p1 ty ((p2 ◠ty)::T) T.
+ Proof. intros ->. by apply tctx_extract_hasty_here. Qed.
Definition tctx_extract_blocked E L p κ ty T T' : Prop :=
tctx_incl E L T ((p â—{κ} ty)::T').
@@ -345,24 +345,17 @@ Section type_context.
Qed.
End type_context.
-Global Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked.
-Hint Resolve tctx_extract_hasty_here_copy 1 : lrust_typing.
+Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
tctx_extract_ctx_nil tctx_extract_ctx_hasty
tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing.
+Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
+ tctx_incl : lrust_typing.
(* In general, we want reborrowing to be tried before subtyping, so
that we get the extraction. However, in the case the types match
exactly, we want to NOT use reborrowing. Therefore, we add
- [tctx_extract_hasty_here_eq] as a hint with a very low cost.
-
- However, we want this hint to be used after
- [tctx_extract_hasty_here_copy], so that we keep the typing it in
- the environment if the type is copy. But due to a bug in Coq, we
- cannot enforce this using [Hint Resolve]. Cf:
- https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
-Hint Extern 2 (tctx_extract_hasty _ _ ?p1 _ ((?p2 â— _) :: _) _) =>
- unify p1 p2;
- eapply tctx_extract_hasty_here_eq : lrust_typing.
+ [tctx_extract_hasty_here_eq] as a hint with a very low cost. *)
+Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 132c55f0d195e3f5e21c014b781f4f5a247213e1..fdf54fe406a566172b76a2fc1e265370d8080ae7 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -45,7 +45,9 @@ Section uninit.
eqtype E L (uninit0 n) (uninit n).
Proof. apply equiv_eqtype; (split; first split)=>//=. apply uninit0_sz. Qed.
- Lemma uninit_product_eqtype E L ns :
+ (* TODO : these lemmas cannot be used by [solve_typing], because
+ unification cannot infer the [ns] parameter. *)
+ Lemma uninit_product_eqtype {E L} ns :
eqtype E L (uninit (foldr plus 0%nat ns)) (Î (uninit <$> ns)).
Proof.
rewrite -uninit_uninit0_eqtype. etrans; last first.
@@ -54,19 +56,28 @@ Section uninit.
induction ns as [|n ns IH]=>//=. revert IH.
by rewrite /= /uninit0 replicate_plus prod_flatten_l -!prod_app=>->.
Qed.
- Lemma uninit_product_eqtype' E L ns :
+ Lemma uninit_product_eqtype' {E L} ns :
eqtype E L (Î (uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
Proof. symmetry; apply uninit_product_eqtype. Qed.
- Lemma uninit_product_subtype E L ns :
+ Lemma uninit_product_subtype {E L} ns :
subtype E L (uninit (foldr plus 0%nat ns)) (Î (uninit <$> ns)).
Proof. apply uninit_product_eqtype'. Qed.
- Lemma uninit_product_subtype' E L ns :
+ Lemma uninit_product_subtype' {E L} ns :
subtype E L (Î (uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
Proof. apply uninit_product_eqtype. Qed.
- Lemma uninit_unit E L :
- eqtype E L unit (uninit 0%nat).
- Proof. apply (uninit_product_eqtype _ _ []). Qed.
+ Lemma uninit_unit_eqtype E L :
+ eqtype E L (uninit 0) unit.
+ Proof. apply (uninit_product_eqtype []). Qed.
+ Lemma uninit_unit_eqtype' E L :
+ subtype E L unit (uninit 0).
+ Proof. apply (uninit_product_eqtype' []). Qed.
+ Lemma uninit_unit_subtype E L :
+ subtype E L (uninit 0) unit.
+ Proof. apply (uninit_product_subtype []). Qed.
+ Lemma uninit_unit_subtype' E L :
+ subtype E L unit (uninit 0).
+ Proof. apply (uninit_product_subtype []). Qed.
Lemma uninit_own n tid vl :
(uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = nâŒ.
@@ -82,4 +93,6 @@ Section uninit.
End uninit.
Hint Resolve uninit_product_eqtype uninit_product_eqtype'
- uninit_product_subtype uninit_product_subtype' : lrust_typing.
+ uninit_product_subtype uninit_product_subtype'
+ uninit_unit_eqtype uninit_unit_eqtype'
+ uninit_unit_subtype uninit_unit_subtype' : lrust_typing.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 92fcd931f6c9efd49d1d9e0e032c64211acfd540..8e0642e1bdb44f7311005d6eb26f632679de4909 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -121,7 +121,7 @@ Section typing.
- iExists _. iSplit; first done. iFrame. iExists _. iFrame.
rewrite uninit_own. auto. }
intros v. simpl_subst. clear v.
- eapply (type_new_subtype unit); [solve_typing..|apply uninit_unit|].
+ eapply type_new; [solve_typing..|].
intros r. simpl_subst.
eapply type_delete; [solve_typing..|].
eapply type_delete; [solve_typing..|].