-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathwpc_notation.v
More file actions
114 lines (106 loc) · 7.11 KB
/
Copy pathwpc_notation.v
File metadata and controls
114 lines (106 loc) · 7.11 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
From iris.algebra Require Import gmap auth agree gset coPset excl csum.
From Perennial.program_logic Require Import staged_invariant post_expr crash_weakestpre.
From Perennial.base_logic.lib Require Import saved_prop.
From Perennial.Helpers Require Import Qextra.
(* Notation: copied from iris bi/weakestpre.v *)
Class Wpc (Λ : language) (PROP A : Type) :=
wpc : A → coPset → expr Λ → (val Λ → PROP) → PROP → PROP.
Arguments wpc {_ _ _ _} _ _ _%E _%I _%I.
Instance: Params (@wpc) 9 := {}.
(* Instance wpc' `{!irisGS Λ Σ, !generationGS Λ Σ} : Wpc Λ (iProp Σ) stuckness := wpc_aux.(unseal). *)
Instance wpc' `{!irisGS Λ Σ, !generationGS Λ Σ} : Wpc Λ (iProp Σ) stuckness :=
crash_weakestpre.wpc.
(** Notations for partial crash weakest preconditions *)
(** Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WPC' e @ s ; E1 {{ Φ } } {{ Φc } }" := (wpc s E1 e%E Φ Φc)
(at level 20, e, Φ, Φc at level 200, only parsing) : bi_scope.
Notation "'WPC' e @ E1 {{ Φ } } {{ Φc } }" := (wpc NotStuck E1 e%E Φ Φc)
(at level 20, e, Φ, Φc at level 200, only parsing) : bi_scope.
Notation "'WPC' e {{ Φ } } {{ Φc } }" := (wpc NotStuck ⊤ e%E Φ Φc)
(at level 20, e, Φ, Φc at level 200, only parsing) : bi_scope.
(** Notations with binder. *)
Notation "'WPC' e @ s ; E1 {{ v , Q } } {{ R } }" := (wpc s E1 e%E (λ v, Q) R)
(at level 20, e, Q, R at level 200,
format "'[hv' 'WPC' e '/' @ '[' s ; E1 ']' '/' {{ '[' v , '/' Q ']' } } '/' {{ '[' R ']' } } ']'") : bi_scope.
Notation "'WPC' e @ E1 {{ v , Q } } {{ R } }" := (wpc NotStuck E1 e%E (λ v, Q) R)
(at level 20, e, Q, R at level 200,
format "'[hv' 'WPC' e '/' @ '[' E1 ']' '/' {{ '[' v , '/' Q ']' } } '/' {{ '[' R ']' } } ']'") : bi_scope.
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E1 {{{ x .. y , 'RET' pat ; Q } } } {{{ Qc } } }" :=
(□ ∀ Φ Φc,
P -∗ (Qc -∗ Φc) ∧ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WPC e @ s; E1 {{ Φ }} {{ Φc }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' s ; E1 ']' '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } '/' {{{ '[' Qc ']' } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E1 {{{ x .. y , 'RET' pat ; Q } } } {{{ Qc } } }" :=
(□ ∀ Φ Φc,
P -∗ (Qc -∗ Φc) ∧ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WPC e @ E1 {{ Φ }} {{ Φc }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' E1 ']' '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } '/' {{{ '[' Qc ']' } } } ']'") : bi_scope.
(*
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
*)
Notation "'{{{' P } } } e @ s ; E1 {{{ 'RET' pat ; Q } } } {{{ Qc } } }" :=
(□ ∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (Q -∗ Φ pat%V) -∗ WPC e @ s; E1 {{ Φ }} {{ Φc }})%I
(at level 20,
format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' s ; E1 ']' '/' {{{ '[' RET pat ; '/' Q ']' } } } '/' {{{ '[' Qc ']' } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E1 {{{ 'RET' pat ; Q } } } {{{ Qc } } }" :=
(□ ∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (Q -∗ Φ pat%V) -∗ WPC e @ E1 {{ Φ }} {{ Φc }})%I
(at level 20,
format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' E1 ']' '/' {{{ '[' RET pat ; '/' Q ']' } } } '/' {{{ '[' Qc ']' } } } ']'") : bi_scope.
(*
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ RET pat ; Q } } } ']'") : bi_scope.
*)
(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
Notation "'{{{' P } } } e @ s ; E1 {{{ x .. y , 'RET' pat ; Q } } } {{{ Qc } } }" :=
(∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WPC e @ s; E1 {{ Φ }} {{ Φc }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E1 {{{ x .. y , 'RET' pat ; Q } } } {{{ Qc } } }" :=
(∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WPC e @ E1 {{ Φ }} {{ Φc }}) : stdpp_scope.
(*
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
*)
Notation "'{{{' P } } } e @ s ; E1 {{{ 'RET' pat ; Q } } } {{{ Qc } } }" :=
(∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (Q -∗ Φ pat%V) -∗ WPC e @ s; E1 {{ Φ }} {{ Φc }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E1 {{{ 'RET' pat ; Q } } } {{{ Qc } } }" :=
(∀ Φ Φc, P -∗ (Qc -∗ Φc) ∧ ▷ (Q -∗ Φ pat%V) -∗ WPC e @ E1 {{ Φ }} {{ Φc }}) : stdpp_scope.