Commit d55f8339 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/big-op-scopes' into 'master'

fix scopes for big-ops

See merge request iris/iris!652
parents bb53251f 3f1a95d1
......@@ -7,29 +7,29 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
(** Notations for unary variants *)
Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_sep (λ k x, P) l) : bi_scope.
(big_opL bi_sep (λ k x, P%I) l) : bi_scope.
Notation "'[∗' 'list]' x ∈ l , P" :=
(big_opL bi_sep (λ _ x, P) l) : bi_scope.
Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
(big_opL bi_sep (λ _ x, P%I) l) : bi_scope.
Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps%I) : bi_scope.
Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_and (λ k x, P) l) : bi_scope.
(big_opL bi_and (λ k x, P%I) l) : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" :=
(big_opL bi_and (λ _ x, P) l) : bi_scope.
Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
(big_opL bi_and (λ _ x, P%I) l) : bi_scope.
Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps%I) : bi_scope.
Notation "'[∨' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_or (λ k x, P) l) : bi_scope.
(big_opL bi_or (λ k x, P%I) l) : bi_scope.
Notation "'[∨' 'list]' x ∈ l , P" :=
(big_opL bi_or (λ _ x, P) l) : bi_scope.
Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps) : bi_scope.
(big_opL bi_or (λ _ x, P%I) l) : bi_scope.
Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps%I) : bi_scope.
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P%I) m) : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P%I) m) : bi_scope.
Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P%I) X) : bi_scope.
Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P%I) X) : bi_scope.
(** Definitions and notations for binary variants *)
(** A version of the separating big operator that ranges over two lists. This
......@@ -47,9 +47,9 @@ Global Instance: Params (@big_sepL2) 3 := {}.
Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
Typeclasses Opaque big_sepL2.
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
(big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
(big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope.
Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
(big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
(big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope.
Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
(Φ : K A B PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
......@@ -61,9 +61,9 @@ Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
Global Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
(big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
(big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope.
Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
(big_sepM2 (λ _ x1 x2, P) m1 m2) : bi_scope.
(big_sepM2 (λ _ x1 x2, P%I) m1 m2) : bi_scope.
(** * Properties *)
Section big_op.
......
......@@ -249,9 +249,9 @@ Infix "∗" := bi_sep : bi_scope.
Notation "(∗)" := bi_sep (only parsing) : bi_scope.
Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
Notation "∀ x .. y , P" :=
(bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
(bi_forall (λ x, .. (bi_forall (λ y, P%I)) ..)) : bi_scope.
Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
(bi_exist (λ x, .. (bi_exist (λ y, P%I)) ..)) : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Notation "▷ P" := (bi_later P) : bi_scope.
......
From iris.algebra Require Import frac.
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic lib.fancy_updates.
Section base_logic_tests.
Context {M : ucmra}.
Implicit Types P Q R : uPred M.
(* Test scopes for bupd *)
Definition use_bupd_uPred (n : nat) : uPred M :=
|==> m : nat , n = 2 .
Definition use_plainly_uPred (n : nat) : uPred M :=
|==> m : nat , n = 2 .
(* Test scopes inside big-ops *)
Definition big_op_scope_uPred_1 (xs : list nat) : uPred M :=
[ list] _ x xs, True.
Definition big_op_scope_uPred_2 (xs : list nat) : uPred M :=
[ list] x; y xs; xs, True.
Definition big_op_scope_uPred_3 (m : gmap nat nat) : uPred M :=
[ map] _ x m, True.
Definition big_op_scope_uPred_4 (m : gmap nat nat) : uPred M :=
[ map] x; y m; m, True.
End base_logic_tests.
Section iris_tests.
Context `{!invG Σ}.
Implicit Types P Q R : iProp Σ.
(* Test scopes for bupd and fupd *)
Definition use_bupd_iProp (n : nat) : iProp Σ :=
|==> m : nat , n = 2 .
Definition use_fupd_iProp (n : nat) : iProp Σ :=
|={}=> m : nat , n = 2 .
(* Test scopes inside big-ops *)
Definition big_op_scope_iProp_1 (xs : list nat) : iProp Σ :=
[ list] _ x xs, True.
Definition big_op_scope_iProp_2 (xs : list nat) : iProp Σ :=
[ list] x; y xs; xs, True.
Definition big_op_scope_iProp_3 (m : gmap nat nat) : iProp Σ :=
[ map] _ x m, True.
Definition big_op_scope_iProp_4 (m : gmap nat nat) : iProp Σ :=
[ map] x; y m; m, True.
End iris_tests.
......@@ -9,12 +9,6 @@ Section base_logic_tests.
Context {M : ucmra}.
Implicit Types P Q R : uPred M.
(* Test scopes for bupd *)
Definition use_bupd_uPred (n : nat) : uPred M :=
|==> m : nat , n = 2 .
Definition use_plainly_uPred (n : nat) : uPred M :=
|==> m : nat , n = 2 .
Lemma test_random_stuff (P1 P2 P3 : nat uPred M) :
(x y : nat) a b,
x y
......@@ -61,12 +55,6 @@ Section iris_tests.
Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
Implicit Types P Q R : iProp Σ.
(* Test scopes for bupd and fupd *)
Definition use_bupd_iProp (n : nat) : iProp Σ :=
|==> m : nat , n = 2 .
Definition use_fupd_iProp (n : nat) : iProp Σ :=
|={}=> m : nat , n = 2 .
Lemma test_masks N E P Q R :
N E
(True - P - inv N Q - True - R) - P - Q ={E}= R.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment