Commit 738b0353 authored by Adam's avatar Adam
Browse files

Extract dfrac notations

This fixes the fixme introduced in !554.
Coq issue #13654 was fixed by coq pr #14183.
parent f6dd81bc
......@@ -32,6 +32,16 @@ Inductive dfrac :=
| DfracDiscarded : 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.
Canonical Structure dfracO := leibnizO dfrac.
......
......@@ -123,16 +123,8 @@ Section definitions.
End definitions.
Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Local Notation "l ↦{ dq } v" := (mapsto l dq v)
(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.
Local Notation "l ↦ dq v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
Section gen_heap.
Context {L V} `{Countable L, !gen_heapGS L V Σ}.
......
......@@ -17,16 +17,8 @@ with lists of values. *)
Definition array `{!heapGS Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
[ list] i v vs, (l + i) {dq} v.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "l ↦∗{ dq } vs" := (array l dq vs)
(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.
Notation "l ↦∗ dq vs" := (array l dq vs)
(at level 20, dq custom dfrac at level 1, format "l ↦∗ dq vs") : bi_scope.
(** We have [FromSep] and [IntoSep] instances to split the fraction (via the
[AsFractional] instance below), but not for splitting the list, as that would
......
......@@ -48,17 +48,9 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
Global Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *)
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Module notation.
Notation "l ↦{ dq } v" := (mapsto l dq v)
(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 "l ↦ dq v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
......
......@@ -28,16 +28,8 @@ Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
(** Since we use an [option val] instance of [gen_heap], we need to overwrite
the notations. That also helps for scopes and coercions. *)
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
(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.
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.
(** 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
......
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