Commit f6df2576 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Inline dfrac notations to work around https://github.com/coq/coq/issues/13654

parent 7499c0fa
...@@ -9,9 +9,7 @@ ...@@ -9,9 +9,7 @@
-Q iris/program_logic iris.program_logic -Q iris/program_logic iris.program_logic
-Q iris_heap_lang iris.heap_lang -Q iris_heap_lang iris.heap_lang
# We sometimes want to locally override notation, and there is no good way to do that with scopes. # We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden -arg -w -arg -notation-overridden
# Coq emits warnings when a custom entry is reimported, this is too noisy.
-arg -w -arg -custom-entry-overriden
# Cannot use non-canonical projections as it causes massive unification failures # Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294). # (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
......
...@@ -32,16 +32,6 @@ Inductive dfrac := ...@@ -32,16 +32,6 @@ Inductive dfrac :=
| DfracDiscarded : dfrac | DfracDiscarded : dfrac
| DfracBoth : Qp dfrac. | DfracBoth : Qp dfrac.
(* This notation is intended to be used as a component in other notations that
include discardable fractions. The notation provides shorthands for the
constructors and the commonly used full fraction. For an example
demonstrating how this can be used see the notation in [gen_heap.v]. *)
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
Notation "□" := DfracDiscarded (in custom dfrac).
Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
Notation "" := (DfracOwn 1) (in custom dfrac).
Section dfrac. Section dfrac.
Canonical Structure dfracO := leibnizO dfrac. Canonical Structure dfracO := leibnizO dfrac.
......
...@@ -123,8 +123,14 @@ Section definitions. ...@@ -123,8 +123,14 @@ Section definitions.
End definitions. End definitions.
Arguments meta {L _ _ V Σ _ A _ _} l N x. Arguments meta {L _ _ V Σ _ A _ _} l N x.
Local Notation "l ↦ dq v" := (mapsto l dq v) Local Notation "l ↦{ dq } v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, format "l ↦{ dq } v") : bi_scope.
Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
(at level 20, format "l ↦□ v") : bi_scope.
Local Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
(at level 20, format "l ↦{# q } v") : bi_scope.
Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
(at level 20, format "l ↦ v") : bi_scope.
Section gen_heap. Section gen_heap.
Context {L V} `{Countable L, !gen_heapG L V Σ}. Context {L V} `{Countable L, !gen_heapG L V Σ}.
......
...@@ -16,8 +16,14 @@ with lists of values. *) ...@@ -16,8 +16,14 @@ with lists of values. *)
Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ := Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) {dq} v)%I. ([ list] i v vs, (l + i) {dq} v)%I.
Notation "l ↦∗ dq vs" := (array l dq vs) Notation "l ↦∗{ dq } vs" := (array l dq vs)
(at level 20, dq custom dfrac at level 1, format "l ↦∗ dq vs") : bi_scope. (at level 20, format "l ↦∗{ dq } vs") : bi_scope.
Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
(at level 20, format "l ↦∗□ vs") : bi_scope.
Notation "l ↦∗{# q } vs" := (array l (DfracOwn q) vs)
(at level 20, format "l ↦∗{# q } vs") : bi_scope.
Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
(** We have [FromSep] and [IntoSep] instances to split the fraction (via the (** We have [FromSep] and [IntoSep] instances to split the fraction (via the
[AsFractional] instance below), but not for splitting the list, as that would [AsFractional] instance below), but not for splitting the list, as that would
......
...@@ -49,8 +49,14 @@ Arguments atomic_heap _ {_}. ...@@ -49,8 +49,14 @@ Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *) (** Notation for heap primitives, in a module so you can import it separately. *)
Module notation. Module notation.
Notation "l ↦ dq v" := (mapsto l dq v) Notation "l ↦{ dq } v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, format "l ↦{ dq } v") : bi_scope.
Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
(at level 20, format "l ↦□ v") : bi_scope.
Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
(at level 20, format "l ↦{# q } v") : bi_scope.
Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
(at level 20, format "l ↦ v") : bi_scope.
Notation "'ref' e" := (alloc e) : expr_scope. Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope. Notation "! e" := (load e) : expr_scope.
......
...@@ -28,8 +28,14 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := { ...@@ -28,8 +28,14 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
(** Since we use an [option val] instance of [gen_heap], we need to overwrite (** Since we use an [option val] instance of [gen_heap], we need to overwrite
the notations. That also helps for scopes and coercions. *) the notations. That also helps for scopes and coercions. *)
Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V)) Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, format "l ↦{ dq } v") : bi_scope.
Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
(at level 20, format "l ↦□ v") : bi_scope.
Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
(at level 20, format "l ↦{# q } v") : bi_scope.
Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
(at level 20, format "l ↦ v") : bi_scope.
(** Same for [gen_inv_heap], except that these are higher-order notations so to (** Same for [gen_inv_heap], except that these are higher-order notations so to
make setoid rewriting in the predicate [I] work we need actual definitions make setoid rewriting in the predicate [I] work we need actual definitions
......
Supports Markdown
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