Skip to content

GitLab

Commit 2ccfdaaa authored by Michael Sammler's avatar Michael Sammler Committed by Michael Sammler
Browse files

update to coq 8.13.2

parent 971ef3f2
Pipeline #51547 passed with stage
in 37 minutes and 56 seconds
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
View file @ 2ccfdaaa
......@@ -31,10 +31,10 @@ variables:
## Build jobs
# TODO: remove z3 version 4.8.9-1 once https://github.com/Z3Prover/z3/issues/5405 and https://github.com/rems-project/cerberus/issues/180 are fixed
build-coq.8.12.0-timing:
build-coq.8.13.2-timing:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
only:
......@@ -44,10 +44,10 @@ build-coq.8.12.0-timing:
tags:
- fp-timing
build-coq.8.12.0:
build-coq.8.13.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
DENY_WARNINGS: "1"
only:
- /^ci/@iris/refinedc
......@@ -55,7 +55,7 @@ build-coq.8.12.0:
trigger-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
except:
only:
- triggers
......
linux/casestudies/proofs/page_alloc/page_alloc_def.v
View file @ 2ccfdaaa
......@@ -22,8 +22,8 @@ Section type.
SubsumePlace l β (list_node n1) (list_node n2) :=
λ T, i2p (subsume_list_node n1 n2 l β T).
Global Instance inj_hyp_page_map {A B C D E F} : Inj (=) (=) (λ '(ref_count, order, next), (pool, vmemmap, npages, ref_count, order, next) : (A * B * C * D * E * F)).
Proof. move => ??? [[??]?] [[??]?]. naive_solver. Qed.
Global Instance inj_hyp_page_map {A B C D E F} pool vmemmap npages : Inj (=) (=) (λ '(ref_count, order, next), (pool, vmemmap, npages, ref_count, order, next) : (A * B * C * D * E * F)).
Proof. move => [[??]?] [[??]?]. naive_solver. Qed.
Global Instance assume_inj_list_node vmemmap len : AssumeInj (=) (=) (λ h, list_node (idx_to_node vmemmap len h)).
Proof. done. Qed.
......
refinedc.opam
View file @ 2ccfdaaa
......@@ -16,7 +16,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.12.0" & < "8.13~") }
"coq" { (>= "8.13.2" & < "8.14~") }
"coq-iris" { (= "dev.2021-07-26.8.eb05e835") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
......
theories/lang/layout.v
View file @ 2ccfdaaa
......@@ -12,24 +12,24 @@ Record layout :=
Definition sizeof (ly : layout) : nat := ly.(ly_size).
Definition ly_align (ly : layout) : nat := 2 ^ ly.(ly_align_log).
Instance layout_dec_eq : EqDecision layout.
Global Instance layout_dec_eq : EqDecision layout.
Proof. solve_decision. Defined.
Instance layout_inhabited : Inhabited layout :=
Global Instance layout_inhabited : Inhabited layout :=
populate (Layout 0 0).
Instance layout_countable : Countable layout.
Global Instance layout_countable : Countable layout.
Proof.
refine (inj_countable'
(λ ly, (ly.(ly_size), ly.(ly_align_log)))
(λ '(sz, a), Layout sz a) _); by intros [].
Qed.
Instance layout_le : SqSubsetEq layout := λ ly1 ly2,
Global Instance layout_le : SqSubsetEq layout := λ ly1 ly2,
(ly1.(ly_size) ≤ ly2.(ly_size))%nat ∧
(ly1.(ly_align_log) ≤ ly2.(ly_align_log))%nat.
Instance layout_le_po : PreOrder layout_le.
Global Instance layout_le_po : PreOrder layout_le.
Proof.
split => ?; rewrite /layout_le => *; repeat case_bool_decide => //; lia.
Qed.
......@@ -78,9 +78,9 @@ Arguments ly_align : simpl never.
Typeclasses Opaque layout_le ly_offset ly_set_size ly_mult ly_with_align.
Hint Extern 0 (LayoutWf _) => refine (layout_wf_mod _ _); done : typeclass_instances.
Hint Extern 0 (LayoutWf _) => unfold LayoutWf; done : typeclass_instances.
Hint Extern 0 (LayoutEq _ _) => exact: eq_refl : typeclass_instances.
Global Hint Extern 0 (LayoutWf _) => refine (layout_wf_mod _ _); done : typeclass_instances.
Global Hint Extern 0 (LayoutWf _) => unfold LayoutWf; done : typeclass_instances.
Global Hint Extern 0 (LayoutEq _ _) => exact: eq_refl : typeclass_instances.
(*** Notations for specific layouts *)
Definition void_layout : layout := {| ly_size := 0; ly_align_log := 0 |}.
......
theories/lithium/base.v
View file @ 2ccfdaaa
......@@ -11,8 +11,12 @@ From stdpp Require Import natmap.
From refinedc.lithium Require Import Z_bitblast.
Set Default Proof Using "Type".
Global Unset Program Cases.
Global Set Keyed Unification.
Export Unset Program Cases.
Export Set Keyed Unification.
(* We always annotate hints with locality ([Global] or [Local]). This enforces
that at least global hints are annotated. *)
Export Set Warnings "+deprecated-hint-without-locality".
Typeclasses Opaque is_Some.
(* This is necessary since otherwise keyed unification unfolds these definitions *)
......
theories/lithium/classes.v
View file @ 2ccfdaaa
......@@ -24,7 +24,7 @@ Definition find_in_context {Σ} (fic : find_in_context_info) (T : fic.(fic_A)
Class FindInContext {Σ} (fic : find_in_context_info) (n : nat) (key : Set) : Type :=
find_in_context_proof T: iProp_to_Prop (Σ:=Σ) (find_in_context fic T)
.
Hint Mode FindInContext + + + - : typeclass_instances.
Global Hint Mode FindInContext + + + - : typeclass_instances.
Inductive FICSyntactic : Set :=.
(** ** Instances *)
......@@ -41,7 +41,7 @@ Global Instance find_in_context_direct_inst {Σ B} (P : _ → iProp Σ) :
(** ** [FindHypEqual] *)
Class FindHypEqual {Σ} (key : Type) (Q P P' : iProp Σ) := find_hyp_equal_equal: P = P'.
Hint Mode FindHypEqual + + + ! - : typeclass_instances.
Global Hint Mode FindHypEqual + + + ! - : typeclass_instances.
(** * [destruct_hint] *)
Inductive destruct_hint_info :=
......@@ -56,7 +56,7 @@ Arguments destruct_hint : simpl never.
Class RelatedTo {Σ} (pat : iProp Σ) : Type := {
rt_fic : find_in_context_info (Σ:=Σ);
}.
Hint Mode RelatedTo + + : typeclass_instances.
Global Hint Mode RelatedTo + + : typeclass_instances.
Arguments rt_fic {_ _} _.
(** * [IntroPersistent] *)
......@@ -64,7 +64,7 @@ Arguments rt_fic {_ _} _.
Class IntroPersistent {Σ} (P P' : iProp Σ) := {
ip_persistent : P -∗ □ P'
}.
Hint Mode IntroPersistent + + - : typeclass_instances.
Global Hint Mode IntroPersistent + + - : typeclass_instances.
(** ** Instances *)
Global Instance intro_persistent_intuit Σ (P : iProp Σ) : IntroPersistent (□ P) P.
Proof. constructor. iIntros "$". Qed.
......@@ -92,8 +92,8 @@ Definition simplify_goal {Σ} (P : iProp Σ) (T : iProp Σ → iProp Σ) : iProp
Class SimplifyGoal {Σ} (P : iProp Σ) (n : option N) : Type :=
simplify_goal_proof T : iProp_to_Prop (simplify_goal P T).
Hint Mode SimplifyHyp + + - : typeclass_instances.
Hint Mode SimplifyGoal + ! - : typeclass_instances.
Global Hint Mode SimplifyHyp + + - : typeclass_instances.
Global Hint Mode SimplifyGoal + ! - : typeclass_instances.
(** ** Instances *)
Lemma simplify_hyp_id {Σ} (P : iProp Σ) T:
......@@ -144,8 +144,8 @@ Definition subsume_list {Σ} A (ig : list nat) (l1 l2 : list A) (f : nat → A
Class SubsumeList {Σ} A (ig : list nat) (l1 l2 : list A) (f : nat → A → iProp Σ) : Type :=
subsume_list_proof T : iProp_to_Prop (subsume_list A ig l1 l2 f T).
Hint Mode Subsume + + ! : typeclass_instances.
Hint Mode SubsumeList + + + + + ! : typeclass_instances.
Global Hint Mode Subsume + + ! : typeclass_instances.
Global Hint Mode SubsumeList + + + + + ! : typeclass_instances.
(** ** Instances *)
Lemma subsume_id {Σ} (P : iProp Σ) T:
......
theories/lithium/infrastructure.v
View file @ 2ccfdaaa
......@@ -10,12 +10,12 @@ Definition protected_eq {A} (a : A) : protected a = a := (protected_aux a).(seal
Class ContainsProtected {A} (x : A) : Set := contains_protected: ().
Class IsProtected {A} (x : A) : Set := is_protected: ().
Hint Extern 0 (ContainsProtected ?x) => (match x with | context [protected _] => exact: tt end) : typeclass_instances.
Hint Extern 0 (IsProtected (protected _) ) => (exact: tt) : typeclass_instances.
Global Hint Extern 0 (ContainsProtected ?x) => (match x with | context [protected _] => exact: tt end) : typeclass_instances.
Global Hint Extern 0 (IsProtected (protected _) ) => (exact: tt) : typeclass_instances.
(** * [IsVar] *)
Class IsVar {A} (x : A) : Prop := is_var: True.
Hint Extern 0 (IsVar ?x) => (is_var x; exact: I) : typeclass_instances.
Global Hint Extern 0 (IsVar ?x) => (is_var x; exact: I) : typeclass_instances.
(** * [AssumeInj] *)
Class AssumeInj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop := assume_inj : True.
......@@ -26,7 +26,7 @@ Proof. done. Qed.
Ltac check_hyp_not_exists P :=
assert_fails (assert (P) as _;[fast_done|]).
Class CheckHypNotExists (P : Prop) : Prop := check_hyp_not_exists : True.
Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change True; fast_done) : typeclass_instances.
Global Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change True; fast_done) : typeclass_instances.
(** * Checking if a hyp in the context
The implementation can be found in interpreter.v *)
......@@ -36,7 +36,7 @@ Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : T
(** ** [FastDone]
Should be used if it is expected that the property shows up directly as a hypothesis. *)
Class FastDone (P : Prop) : Prop := fast_done_proof : P.
Hint Extern 1 (FastDone ?P) => (change P; fast_done) : typeclass_instances.
Global Hint Extern 1 (FastDone ?P) => (change P; fast_done) : typeclass_instances.
(** ** [CanSolve]
Requires the user to provide a general purpose [can_solve_tac] (see tactics.v)
......
theories/lithium/interpreter.v
View file @ 2ccfdaaa
......@@ -390,7 +390,7 @@ Ltac unfold_instantiated_evars :=
end.
Create HintDb solve_protected_eq_db discriminated.
Hint Constants Opaque : solve_protected_eq_db.
Global Hint Constants Opaque : solve_protected_eq_db.
Ltac solve_protected_eq_unfold_tac := idtac.
Ltac solve_protected_eq :=
......@@ -421,7 +421,7 @@ Ltac liCheckOwnInContext P :=
lazymatch (type of H) with | IPM_STATE _ => idtac end;
first [ go Δs | go Δi ]
end.
Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; constructor; exact: I) : typeclass_instances.
Global Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; constructor; exact: I) : typeclass_instances.
(** * Main lithium tactics *)
Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
......
theories/lithium/normalize.v
View file @ 2ccfdaaa
......@@ -35,8 +35,8 @@ Hint Rewrite lookup_insert_gmap : lithium_rewrite.
(** * Second version of normalization based on typeclasses *)
Class NormalizeWalk {A} (progress : bool) (a b : A) : Prop := normalize_walk: a = b.
Class Normalize {A} (progress : bool) (a b : A) : Prop := normalize: a = b.
Hint Mode NormalizeWalk + - + - : typeclass_instances.
Hint Mode Normalize + - + - : typeclass_instances.
Global Hint Mode NormalizeWalk + - + - : typeclass_instances.
Global Hint Mode Normalize + - + - : typeclass_instances.
Global Instance normalize_walk_protected A (x : A) :
NormalizeWalk false (protected x) (protected x) | 10.
Proof. done. Qed.
......@@ -47,7 +47,7 @@ Lemma normalize_walk_app A B (f f' : A → B) x x' r p1 p2 p3
`{!Normalize p3 (f' x') r}:
NormalizeWalk true (f x) r.
Proof. unfold NormalizeWalk, Normalize in *. naive_solver. Qed.
Hint Extern 50 (NormalizeWalk _ (?f ?x) _) => class_apply normalize_walk_app : typeclass_instances.
Global Hint Extern 50 (NormalizeWalk _ (?f ?x) _) => class_apply normalize_walk_app : typeclass_instances.
Global Instance normalize_walk_end_progress A (x x' : A) `{!Normalize true x x'} :
NormalizeWalk true x x' | 100.
Proof. done. Qed.
......@@ -60,48 +60,48 @@ Proof. done. Qed.
Lemma normalize_fmap_length A B (f : A → B) l r p `{!Normalize p (length l) r} :
Normalize true (length (f <$> l)) r.
Proof. by rewrite fmap_length. Qed.
Hint Extern 5 (Normalize _ (length (_ <$> _)) _) => class_apply normalize_fmap_length : typeclass_instances.
Global Hint Extern 5 (Normalize _ (length (_ <$> _)) _) => class_apply normalize_fmap_length : typeclass_instances.
Lemma normalize_insert_length A i (x : A) l r p `{!Normalize p (length l) r} :
Normalize true (length (<[i:=x]> l)) r.
Proof. by rewrite insert_length. Qed.
Hint Extern 5 (Normalize _ (length (<[_:=_]> _)) _) => class_apply normalize_insert_length : typeclass_instances.
Global Hint Extern 5 (Normalize _ (length (<[_:=_]> _)) _) => class_apply normalize_insert_length : typeclass_instances.
Lemma normalize_app_length A (l1 l2 : list A) r1 r2 r3 p1 p2 p3
`{!Normalize p1 (length l1) r1} `{!Normalize p2 (length l2) r2} `{!Normalize p3 (r1 + r2)%nat r3}:
Normalize true (length (l1 ++ l2)) r3.
Proof. unfold Normalize in *; subst. by rewrite app_length. Qed.
Hint Extern 5 (Normalize _ (length (_ ++ _)) _) => class_apply normalize_app_length : typeclass_instances.
Global Hint Extern 5 (Normalize _ (length (_ ++ _)) _) => class_apply normalize_app_length : typeclass_instances.
Lemma normalize_app_assoc A (l1 l2 l3 : list A) r1 r2 p1 p2
`{!Normalize p1 (l2 ++ l3) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true ((l1 ++ l2) ++ l3) r2.
Proof. unfold Normalize in *; subst. by rewrite -app_assoc. Qed.
Hint Extern 5 (Normalize _ (((_ ++ _) ++ _)) _) => class_apply normalize_app_assoc : typeclass_instances.
Global Hint Extern 5 (Normalize _ (((_ ++ _) ++ _)) _) => class_apply normalize_app_assoc : typeclass_instances.
Lemma normalize_cons_middle A x (l1 l2 : list A) r1 r2 p1 p2
`{!Normalize p1 (x :: l2) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true (l1 ++ [x] ++ l2) r2.
Proof. unfold Normalize in *; subst. by rewrite -cons_middle. Qed.
(* The hint extern is especially imporant for this lemma as otherwise
tc search loops on goal of form l ++ [_]. *)
Hint Extern 5 (Normalize _ (_ ++ [_] ++ _) _) => class_apply normalize_cons_middle : typeclass_instances.
Global Hint Extern 5 (Normalize _ (_ ++ [_] ++ _) _) => class_apply normalize_cons_middle : typeclass_instances.
Lemma normalize_app_nil_r A (l : list A):
Normalize true (l ++ []) l.
Proof. unfold Normalize in *; subst. by rewrite app_nil_r. Qed.
Hint Extern 5 (Normalize _ (_ ++ []) _) => class_apply normalize_app_nil_r : typeclass_instances.
Global Hint Extern 5 (Normalize _ (_ ++ []) _) => class_apply normalize_app_nil_r : typeclass_instances.
Lemma normalize_rev_involutive A (l : list A):
Normalize true (rev (rev l)) l.
Proof. unfold Normalize in *; subst. by rewrite rev_involutive. Qed.
Hint Extern 5 (Normalize _ (rev (rev _)) _) => class_apply normalize_rev_involutive : typeclass_instances.
Global Hint Extern 5 (Normalize _ (rev (rev _)) _) => class_apply normalize_rev_involutive : typeclass_instances.
Lemma normalize_minus_n_O n:
Normalize true (n - 0)%nat n.
Proof. unfold Normalize in *; subst. by rewrite -minus_n_O. Qed.
Hint Extern 5 (Normalize _ (_ - 0)%nat _) => class_apply normalize_minus_n_O : typeclass_instances.
Global Hint Extern 5 (Normalize _ (_ - 0)%nat _) => class_apply normalize_minus_n_O : typeclass_instances.
Lemma normalize_rotate_length A n (l : list A) r p `{!Normalize p (length l) r} :
Normalize true (length (rotate n l)) r.
Proof. by rewrite rotate_length. Qed.
Hint Extern 5 (Normalize _ (length (rotate _ _)) _) => class_apply normalize_rotate_length : typeclass_instances.
Global Hint Extern 5 (Normalize _ (length (rotate _ _)) _) => class_apply normalize_rotate_length : typeclass_instances.
Lemma normalize_replicate_length A n (l : list A) :
Normalize true (length (replicate n l)) n.
Proof. by rewrite replicate_length. Qed.
Hint Extern 5 (Normalize _ (length (replicate _ _)) _) => class_apply normalize_replicate_length : typeclass_instances.
Global Hint Extern 5 (Normalize _ (length (replicate _ _)) _) => class_apply normalize_replicate_length : typeclass_instances.
Ltac normalize_tc :=
first [
......
theories/lithium/simpl_instances.v
View file @ 2ccfdaaa
......@@ -322,10 +322,10 @@ Qed.
Global Instance simpl_fmap_nil {A B} (l : list A) (f : A → B) : SimplBothRel (=) (f <$> l) [] (l = []).
Proof. split; destruct l; naive_solver. Qed.
Global Instance simpl_fmap_cons_and {A B} (l : list A) l2 (f : A → B):
Global Instance simpl_fmap_cons_and {A B} x (l : list A) l2 (f : A → B):
SimplAndRel (=) (f <$> l) (x :: l2) (λ T, ∃ x' l2', l = x' :: l2' ∧ f x' = x ∧ f <$> l2' = l2 ∧ T).
Proof. split; first naive_solver. intros [?%fmap_cons_inv ?]. naive_solver. Qed.
Global Instance simpl_fmap_cons_impl {A B} (l : list A) l2 (f : A → B):
Global Instance simpl_fmap_cons_impl {A B} x (l : list A) l2 (f : A → B):
SimplImplRel (=) true (f <$> l) (x :: l2) (λ T, ∀ x' l2', l = x' :: l2' → f x' = x → f <$> l2' = l2 → T).
Proof. split; last naive_solver. intros ? ?%fmap_cons_inv. naive_solver. Qed.
Global Instance simpl_fmap_app_and {A B} (l : list A) l1 l2 (f : A → B):
......
theories/lithium/tactics_extend.v
View file @ 2ccfdaaa
From refinedc.lithium Require Import base infrastructure.
Ltac can_solve_tac := fail "provide a can_solve_tac!".
Hint Extern 10 (CanSolve ?P) => (change P; can_solve_tac) : typeclass_instances.
Global Hint Extern 10 (CanSolve ?P) => (change P; can_solve_tac) : typeclass_instances.
Ltac sidecond_hook := idtac.
Ltac unsolved_sidecond_hook := idtac.
......
theories/typing/automation.v
View file @ 2ccfdaaa
......@@ -32,7 +32,7 @@ Ltac custom_exist_tac A protect ::=
| Movable _ => eexists _
end.
Hint Transparent ly_size : solve_protected_eq_db.
Global Hint Transparent ly_size : solve_protected_eq_db.
Ltac solve_protected_eq_unfold_tac ::=
lazymatch goal with
(* unfold constants for function types *)
......
theories/typing/automation/loc_eq.v
View file @ 2ccfdaaa
......@@ -66,7 +66,7 @@ Lemma tac_solve_loc_eq `{!typeG Σ} l1 β1 ty1 l2 β2 ty2:
FindHypEqual FICLocSemantic (l1 ◁ₗ{β1} ty1) (l2 ◁ₗ{β2} ty2) (l1 ◁ₗ{β2} ty2).
Proof. by move => ->. Qed.
Hint Extern 10 (FindHypEqual FICLocSemantic (_ ◁ₗ{_} _) (_ ◁ₗ{_} _) _) =>
Global Hint Extern 10 (FindHypEqual FICLocSemantic (_ ◁ₗ{_} _) (_ ◁ₗ{_} _) _) =>
(notypeclasses refine (tac_solve_loc_eq _ _ _ _ _ _ _); solve_loc_eq) : typeclass_instances.
Lemma tac_loc_in_bounds_solve_loc_eq `{!typeG Σ} l1 l2 n1 n2:
......@@ -74,7 +74,7 @@ Lemma tac_loc_in_bounds_solve_loc_eq `{!typeG Σ} l1 l2 n1 n2:
FindHypEqual FICLocSemantic (loc_in_bounds l1 n1) (loc_in_bounds l2 n2) (loc_in_bounds l1 n2).
Proof. by move => ->. Qed.
Hint Extern 10 (FindHypEqual FICLocSemantic (loc_in_bounds _ _) (loc_in_bounds _ _) _) =>
Global Hint Extern 10 (FindHypEqual FICLocSemantic (loc_in_bounds _ _) (loc_in_bounds _ _) _) =>
(notypeclasses refine (tac_loc_in_bounds_solve_loc_eq _ _ _ _ _); solve_loc_eq) : typeclass_instances.
Section test.
......
theories/typing/base.v
View file @ 2ccfdaaa
From refinedc.lithium Require Export lithium.
From refinedc.lang Require Export proofmode.
Create HintDb refinedc_typing.
Ltac solve_typing :=
(typeclasses eauto with refinedc_typing typeclass_instances core).
Hint Constructors Forall Forall2 elem_of_list : refinedc_typing.
Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
: refinedc_typing.
Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
(etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : refinedc_typing.
Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
(etrans; [exact: Nat2Z.id | reflexivity]) : refinedc_typing.
Hint Resolve <- elem_of_app : refinedc_typing.
(* done is there to handle equalities with constants *)
Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : refinedc_typing.
Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : refinedc_typing.
Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : refinedc_typing.
Class CoPsetFact (P : Prop) : Prop := copset_fact : P.
(* clear for performance reasons as there can be many hypothesis and they should not be needed for the goals which occur *)
Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset).
Local Definition coPset_disjoint_empty_l := disjoint_empty_l (C:=coPset).
Hint Extern 1 (CoPsetFact ?P) => (change P; clear; eauto using coPset_disjoint_empty_r, coPset_disjoint_empty_r with solve_ndisj) : typeclass_instances.
Global Hint Extern 1 (CoPsetFact ?P) => (change P; clear; eauto using coPset_disjoint_empty_r, coPset_disjoint_empty_r with solve_ndisj) : typeclass_instances.
theories/typing/bytes.v
View file @ 2ccfdaaa
......@@ -254,7 +254,7 @@ Notation "uninit< ly >" := (uninit ly) (only printing, format "'uninit<' ly '>'"
(* See the definition of [uninit_mono_inst].
This hint should only apply ty is not uninit as this case is covered by the rules for bytes. *)
Hint Extern 5 (SubsumePlace _ Own ?ty (uninit _)) =>
Global Hint Extern 5 (SubsumePlace _ Own ?ty (uninit _)) =>
lazymatch ty with
| uninit _ => fail
| _ => unshelve notypeclasses refine (uninit_mono_inst _ _ _)
......
theories/typing/programs.v
View file @ 2ccfdaaa
......@@ -316,38 +316,38 @@ Ltac solve_into_place_ctx :=
change_no_check (IntoPlaceCtx (W.to_expr e') T);
refine (find_place_ctx_correct _ _ _); rewrite/=/W.to_expr/=; done
end.
Hint Extern 0 (IntoPlaceCtx _ _) => solve_into_place_ctx : typeclass_instances.
Hint Mode Learnable + + : typeclass_instances.
Hint Mode LearnAlignment + + + + - : typeclass_instances.
Hint Mode SimplifyHypPlace + + + + + - : typeclass_instances.
Hint Mode SimplifyHypVal + + + + + - : typeclass_instances.
Hint Mode SimplifyGoalPlace + + + + ! - : typeclass_instances.
Hint Mode SimplifyGoalVal + + + ! ! - : typeclass_instances.
Hint Mode CopyAs + + + + + : typeclass_instances.
Hint Mode SubsumePlace + + + + + ! : typeclass_instances.
Hint Mode SubsumeVal + + + + ! + ! : typeclass_instances.
Hint Mode SimpleSubsumePlace + + + ! - : typeclass_instances.
Hint Mode SimpleSubsumePlaceR + + + ! + ! - : typeclass_instances.
Hint Mode SimpleSubsumeVal + + + ! + ! - : typeclass_instances.
Hint Mode TypedIf + + + + : typeclass_instances.
Hint Mode TypedAssert + + + + + : typeclass_instances.
Hint Mode TypedValue + + + : typeclass_instances.
Hint Mode TypedBinOp + + + + + + + + + : typeclass_instances.
Hint Mode TypedBinOpVal + + + + + + + + + + + : typeclass_instances.
Hint Mode TypedUnOp + + + + + + : typeclass_instances.
Hint Mode TypedUnOpVal + + + + + + + : typeclass_instances.
Hint Mode TypedCall + + + + + + : typeclass_instances.
Hint Mode TypedCallVal + + + + + + + : typeclass_instances.
Hint Mode TypedCopyAllocId + + + + + + + : typeclass_instances.
Hint Mode TypedCopyAllocIdVal + + + + + + + + + : typeclass_instances.
Hint Mode TypedReadEnd + + + + + + + : typeclass_instances.
Hint Mode TypedWriteEnd + + + + + + + + + + : typeclass_instances.
Hint Mode TypedAddrOfEnd + + + + + : typeclass_instances.
Hint Mode TypedPlace + + + + + + : typeclass_instances.
Hint Mode TypedAnnotExpr + + + + + + + : typeclass_instances.
Hint Mode TypedAnnotStmt + + + + + + : typeclass_instances.
Hint Mode TypedMacroExpr + + + + : typeclass_instances.
Global Hint Extern 0 (IntoPlaceCtx _ _) => solve_into_place_ctx : typeclass_instances.
Global Hint Mode Learnable + + : typeclass_instances.
Global Hint Mode LearnAlignment + + + + - : typeclass_instances.
Global Hint Mode SimplifyHypPlace + + + + + - : typeclass_instances.
Global Hint Mode SimplifyHypVal + + + + + - : typeclass_instances.
Global Hint Mode SimplifyGoalPlace + + + + ! - : typeclass_instances.
Global Hint Mode SimplifyGoalVal + + + ! ! - : typeclass_instances.
Global Hint Mode CopyAs + + + + + : typeclass_instances.
Global Hint Mode SubsumePlace + + + + + ! : typeclass_instances.
Global Hint Mode SubsumeVal + + + + ! + ! : typeclass_instances.
Global Hint Mode SimpleSubsumePlace + + + ! - : typeclass_instances.
Global Hint Mode SimpleSubsumePlaceR + + + ! + ! - : typeclass_instances.
Global Hint Mode SimpleSubsumeVal + + + ! + ! - : typeclass_instances.
Global Hint Mode TypedIf + + + + : typeclass_instances.
Global Hint Mode TypedAssert + + + + + : typeclass_instances.
Global Hint Mode TypedValue + + + : typeclass_instances.
Global Hint Mode TypedBinOp + + + + + + + + + : typeclass_instances.
Global Hint Mode TypedBinOpVal + + + + + + + + + + + : typeclass_instances.
Global Hint Mode TypedUnOp + + + + + + : typeclass_instances.
Global Hint Mode TypedUnOpVal + + + + + + + : typeclass_instances.
Global Hint Mode TypedCall + + + + + + : typeclass_instances.
Global Hint Mode TypedCallVal + + + + + + + : typeclass_instances.
Global Hint Mode TypedCopyAllocId + + + + + + + : typeclass_instances.
Global Hint Mode TypedCopyAllocIdVal + + + + + + + + + : typeclass_instances.
Global Hint Mode TypedReadEnd + + + + + + + : typeclass_instances.
Global Hint Mode TypedWriteEnd + + + + + + + + + + : typeclass_instances.
Global Hint Mode TypedAddrOfEnd + + + + + : typeclass_instances.
Global Hint Mode TypedPlace + + + + + + : typeclass_instances.
Global Hint Mode TypedAnnotExpr + + + + + + + : typeclass_instances.
Global Hint Mode TypedAnnotStmt + + + + + + : typeclass_instances.
Global Hint Mode TypedMacroExpr + + + + : typeclass_instances.
Arguments typed_annot_expr : simpl never.
Arguments typed_annot_stmt : simpl never.
Arguments typed_macro_expr : simpl never.
......@@ -1400,7 +1400,7 @@ Section typing.
End typing.
(* This must be an hint extern because an instance would be a big slowdown . *)
Hint Extern 1 (SubsumePlace _ _ (?ty _) (?ty2 _)) =>
Global Hint Extern 1 (SubsumePlace _ _ (?ty _) (?ty2 _)) =>
match ty with | ty2 => is_var ty; class_apply subtype_var_inst end : typeclass_instances.
(*** guarded *)
......@@ -1529,12 +1529,12 @@ Section guarded.
End guarded.
Hint Mode StripGuarded + + + - - + - : typeclass_instances.
Hint Mode DoStripGuarded + + + - - + - : typeclass_instances.
Hint Mode StripGuardedLst + + + - - + - : typeclass_instances.
Global Hint Mode StripGuarded + + + - - + - : typeclass_instances.
Global Hint Mode DoStripGuarded + + + - - + - : typeclass_instances.
Global Hint Mode StripGuardedLst + + + - - + - : typeclass_instances.
Typeclasses Opaque typed_block.
Hint Extern 0 (DoStripGuarded ?β ?E1 ?E2 ?ty1 ?ty2) =>
Global Hint Extern 0 (DoStripGuarded ?β ?E1 ?E2 ?ty1 ?ty2) =>
change (StripGuarded β E1 E2 ty1 ty2);
lazymatch ty1 with
| context [guarded _ _] => idtac
......@@ -1547,21 +1547,21 @@ Hint Extern 0 (DoStripGuarded ?β ?E1 ?E2 ?ty1 ?ty2) =>
sometimes creates the subgoal in a different order. We need to try
eq first since x1 and x2 in (x1 @ _) and (x2 @ _) might not be
bound in the scope of P. *)
Hint Extern 99 (SimpleSubsumePlace (_ @ _) (_ @ _) _) =>
Global Hint Extern 99 (SimpleSubsumePlace (_ @ _) (_ @ _) _) =>
simple notypeclasses refine (simple_subsume_place_refinement_eq _ _ _ _ _ _ _);
lazymatch goal with
| |- iProp _ => shelve
| |- _ = _ => exact : eq_refl
| |- _ => cbn[eq_rect]
end : typeclass_instances.
Hint Extern 100 (SimpleSubsumePlace (_ @ _) (_ @ _) _) =>
Global Hint Extern 100 (SimpleSubsumePlace (_ @ _) (_ @ _) _) =>
simple notypeclasses refine (simple_subsume_place_refinement _ _ _ _ _);
lazymatch goal with
| |- iProp _ => shelve
| |- _ = _ => exact : eq_refl
| |- _ => cbn[eq_rect]
end : typeclass_instances.
Hint Extern 100 (SimpleSubsumePlace (_ @ _) (ty_of_rty _) _) =>
Global Hint Extern 100 (SimpleSubsumePlace (_ @ _) (ty_of_rty _) _) =>
simple notypeclasses refine (simple_subsume_place_rty_to_ty_r _ _ _ _); lazymatch goal with