Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
8ca359a5
Commit
8ca359a5
authored
Mar 03, 2016
by
Robbert Krebbers
Browse files
More consistent names for scopes in heap_lang.
parent
5fdfeb82
Changes
4
Hide whitespace changes
Inline
Side-by-side
barrier/proof.v
View file @
8ca359a5
...
...
@@ -206,7 +206,7 @@ Proof.
apply
exist_elim
=>
γ
.
rewrite
!
sep_exist_r
.
apply
exist_elim
=>
P
.
rewrite
!
sep_exist_r
.
apply
exist_elim
=>
Q
.
rewrite
!
sep_exist_r
.
apply
exist_elim
=>
i
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>?.
wp_focus
(!
_
)%
L
.
wp_focus
(!
_
)%
E
.
(* I think some evars here are better than repeating *everything* *)
eapply
(
sts_fsaS
_
(
wp_fsa
_
))
with
(
N0
:
=
N
)
(
γ
0
:
=
γ
)
;
simpl
;
eauto
with
I
ndisj
.
...
...
heap_lang/lang.v
View file @
8ca359a5
...
...
@@ -19,10 +19,6 @@ Inductive binder := BAnon | BNamed : string → binder.
Delimit
Scope
binder_scope
with
binder
.
Bind
Scope
binder_scope
with
binder
.
Delimit
Scope
lang_scope
with
L
.
Bind
Scope
lang_scope
with
base_lit
.
Delimit
Scope
val_scope
with
V
.
Bind
Scope
val_scope
with
base_lit
.
Inductive
expr
:
=
(* Base lambda calculus *)
...
...
@@ -51,6 +47,9 @@ Inductive expr :=
|
Store
(
e1
:
expr
)
(
e2
:
expr
)
|
Cas
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
).
Bind
Scope
expr_scope
with
expr
.
Delimit
Scope
expr_scope
with
E
.
Inductive
val
:
=
|
RecV
(
f
x
:
binder
)
(
e
:
expr
)
(* e should be closed *)
|
LitV
(
l
:
base_lit
)
...
...
@@ -59,9 +58,8 @@ Inductive val :=
|
InjRV
(
v
:
val
)
|
LocV
(
l
:
loc
).
Bind
Scope
binder_scope
with
expr
.
Bind
Scope
lang_scope
with
expr
base_lit
.
Bind
Scope
val_scope
with
val
base_lit
.
Bind
Scope
val_scope
with
val
.
Delimit
Scope
val_scope
with
V
.
Global
Instance
base_lit_dec_eq
(
l1
l2
:
base_lit
)
:
Decision
(
l1
=
l2
).
Proof
.
solve_decision
.
Defined
.
...
...
heap_lang/notation.v
View file @
8ca359a5
From
heap_lang
Require
Export
derived
.
Arguments
wp
{
_
_
}
_
_
%
L
_
.
Notation
"|| e @ E {{ Φ } }"
:
=
(
wp
E
e
%
L
Φ
)
Arguments
wp
{
_
_
}
_
_
%
E
_
.
Notation
"|| e @ E {{ Φ } }"
:
=
(
wp
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"|| e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"|| e {{ Φ } }"
:
=
(
wp
⊤
e
%
L
Φ
)
Notation
"|| e {{ Φ } }"
:
=
(
wp
⊤
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"|| e {{ Φ } }"
)
:
uPred_scope
.
...
...
@@ -19,72 +19,71 @@ Coercion of_val : val >-> expr.
Coercion
BNamed
:
string
>->
binder
.
Notation
"<>"
:
=
BAnon
:
binder_scope
.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* No scope, does not conflict and scope is often not inferred properly. *)
Notation
"# l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"# l"
).
Notation
"% l"
:
=
(
LocV
l
)
(
at
level
8
,
format
"% l"
).
Notation
"( e1 , e2 , .. , en )"
:
=
(
Pair
..
(
Pair
e1
e2
)
..
en
)
:
lang_scope
.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation
"( e1 , e2 , .. , en )"
:
=
(
Pair
..
(
Pair
e1
e2
)
..
en
)
:
expr_scope
.
Notation
"'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'"
:
=
(
Match
e0
x1
e1
x2
e2
)
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
lang
_scope
.
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
expr
_scope
.
Notation
"()"
:
=
LitUnit
:
val_scope
.
Notation
"! e"
:
=
(
Load
e
%
L
)
(
at
level
9
,
right
associativity
)
:
lang
_scope
.
Notation
"'ref' e"
:
=
(
Alloc
e
%
L
)
(
at
level
30
,
right
associativity
)
:
lang
_scope
.
Notation
"- e"
:
=
(
UnOp
MinusUnOp
e
%
L
)
(
at
level
35
,
right
associativity
)
:
lang
_scope
.
Notation
"e1 + e2"
:
=
(
BinOp
PlusOp
e1
%
L
e2
%
L
)
(
at
level
50
,
left
associativity
)
:
lang
_scope
.
Notation
"e1 - e2"
:
=
(
BinOp
MinusOp
e1
%
L
e2
%
L
)
(
at
level
50
,
left
associativity
)
:
lang
_scope
.
Notation
"e1 ≤ e2"
:
=
(
BinOp
LeOp
e1
%
L
e2
%
L
)
(
at
level
70
)
:
lang
_scope
.
Notation
"e1 < e2"
:
=
(
BinOp
LtOp
e1
%
L
e2
%
L
)
(
at
level
70
)
:
lang
_scope
.
Notation
"e1 = e2"
:
=
(
BinOp
EqOp
e1
%
L
e2
%
L
)
(
at
level
70
)
:
lang
_scope
.
Notation
"~ e"
:
=
(
UnOp
NegOp
e
%
L
)
(
at
level
75
,
right
associativity
)
:
lang
_scope
.
Notation
"! e"
:
=
(
Load
e
%
E
)
(
at
level
9
,
right
associativity
)
:
expr
_scope
.
Notation
"'ref' e"
:
=
(
Alloc
e
%
E
)
(
at
level
30
,
right
associativity
)
:
expr
_scope
.
Notation
"- e"
:
=
(
UnOp
MinusUnOp
e
%
E
)
(
at
level
35
,
right
associativity
)
:
expr
_scope
.
Notation
"e1 + e2"
:
=
(
BinOp
PlusOp
e1
%
E
e2
%
E
)
(
at
level
50
,
left
associativity
)
:
expr
_scope
.
Notation
"e1 - e2"
:
=
(
BinOp
MinusOp
e1
%
E
e2
%
E
)
(
at
level
50
,
left
associativity
)
:
expr
_scope
.
Notation
"e1 ≤ e2"
:
=
(
BinOp
LeOp
e1
%
E
e2
%
E
)
(
at
level
70
)
:
expr
_scope
.
Notation
"e1 < e2"
:
=
(
BinOp
LtOp
e1
%
E
e2
%
E
)
(
at
level
70
)
:
expr
_scope
.
Notation
"e1 = e2"
:
=
(
BinOp
EqOp
e1
%
E
e2
%
E
)
(
at
level
70
)
:
expr
_scope
.
Notation
"~ e"
:
=
(
UnOp
NegOp
e
%
E
)
(
at
level
75
,
right
associativity
)
:
expr
_scope
.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation
"e1 <- e2"
:
=
(
Store
e1
%
L
e2
%
L
)
(
at
level
80
)
:
lang
_scope
.
Notation
"'rec:' f x := e"
:
=
(
Rec
f
x
e
%
L
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"'rec:' f x := e"
:
=
(
RecV
f
x
e
%
L
)
Notation
"e1 <- e2"
:
=
(
Store
e1
%
E
e2
%
E
)
(
at
level
80
)
:
expr
_scope
.
Notation
"'rec:' f x := e"
:
=
(
Rec
f
x
e
%
E
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"'rec:' f x := e"
:
=
(
RecV
f
x
e
%
E
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'if:' e1 'then' e2 'else' e3"
:
=
(
If
e1
%
L
e2
%
L
e3
%
L
)
(
at
level
200
,
e1
,
e2
,
e3
at
level
200
)
:
lang
_scope
.
Notation
"'if:' e1 'then' e2 'else' e3"
:
=
(
If
e1
%
E
e2
%
E
e3
%
E
)
(
at
level
200
,
e1
,
e2
,
e3
at
level
200
)
:
expr
_scope
.
(** Derived notions, in order of declaration. The notations for let and seq
are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation
"λ: x , e"
:
=
(
Lam
x
e
%
L
)
(
at
level
102
,
x
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"λ: x , e"
:
=
(
LamV
x
e
%
L
)
Notation
"λ: x , e"
:
=
(
Lam
x
e
%
E
)
(
at
level
102
,
x
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"λ: x , e"
:
=
(
LamV
x
e
%
E
)
(
at
level
102
,
x
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'let:' x := e1 'in' e2"
:
=
(
Lam
x
e2
%
L
e1
%
L
)
(
at
level
102
,
x
at
level
1
,
e1
,
e2
at
level
200
)
:
lang
_scope
.
Notation
"e1 ;; e2"
:
=
(
Lam
BAnon
e2
%
L
e1
%
L
)
(
at
level
100
,
e2
at
level
200
,
format
"e1 ;; e2"
)
:
lang
_scope
.
Notation
"'let:' x := e1 'in' e2"
:
=
(
Lam
x
e2
%
E
e1
%
E
)
(
at
level
102
,
x
at
level
1
,
e1
,
e2
at
level
200
)
:
expr
_scope
.
Notation
"e1 ;; e2"
:
=
(
Lam
BAnon
e2
%
E
e1
%
E
)
(
at
level
100
,
e2
at
level
200
,
format
"e1 ;; e2"
)
:
expr
_scope
.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation
"'let:' x := e1 'in' e2"
:
=
(
LamV
x
e2
%
L
e1
%
L
)
Notation
"'let:' x := e1 'in' e2"
:
=
(
LamV
x
e2
%
E
e1
%
E
)
(
at
level
102
,
x
at
level
1
,
e1
,
e2
at
level
200
)
:
val_scope
.
Notation
"e1 ;; e2"
:
=
(
LamV
BAnon
e2
%
L
e1
%
L
)
Notation
"e1 ;; e2"
:
=
(
LamV
BAnon
e2
%
E
e1
%
E
)
(
at
level
100
,
e2
at
level
200
,
format
"e1 ;; e2"
)
:
val_scope
.
Notation
"'rec:' f x y := e"
:
=
(
Rec
f
x
(
Lam
y
e
%
L
))
(
at
level
102
,
f
,
x
,
y
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"'rec:' f x y := e"
:
=
(
RecV
f
x
(
Lam
y
e
%
L
))
Notation
"'rec:' f x y := e"
:
=
(
Rec
f
x
(
Lam
y
e
%
E
))
(
at
level
102
,
f
,
x
,
y
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"'rec:' f x y := e"
:
=
(
RecV
f
x
(
Lam
y
e
%
E
))
(
at
level
102
,
f
,
x
,
y
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'rec:' f x y z := e"
:
=
(
Rec
f
x
(
Lam
y
(
Lam
z
e
%
L
)))
(
at
level
102
,
f
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"'rec:' f x y z := e"
:
=
(
RecV
f
x
(
Lam
y
(
Lam
z
e
%
L
)))
Notation
"'rec:' f x y z := e"
:
=
(
Rec
f
x
(
Lam
y
(
Lam
z
e
%
E
)))
(
at
level
102
,
f
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"'rec:' f x y z := e"
:
=
(
RecV
f
x
(
Lam
y
(
Lam
z
e
%
E
)))
(
at
level
102
,
f
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"λ: x y , e"
:
=
(
Lam
x
(
Lam
y
e
%
L
))
(
at
level
102
,
x
,
y
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"λ: x y , e"
:
=
(
LamV
x
(
Lam
y
e
%
L
))
Notation
"λ: x y , e"
:
=
(
Lam
x
(
Lam
y
e
%
E
))
(
at
level
102
,
x
,
y
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"λ: x y , e"
:
=
(
LamV
x
(
Lam
y
e
%
E
))
(
at
level
102
,
x
,
y
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"λ: x y z , e"
:
=
(
Lam
x
(
Lam
y
(
Lam
z
e
%
L
)))
(
at
level
102
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
lang
_scope
.
Notation
"λ: x y z , e"
:
=
(
LamV
x
(
Lam
y
(
Lam
z
e
%
L
)))
Notation
"λ: x y z , e"
:
=
(
Lam
x
(
Lam
y
(
Lam
z
e
%
E
)))
(
at
level
102
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
expr
_scope
.
Notation
"λ: x y z , e"
:
=
(
LamV
x
(
Lam
y
(
Lam
z
e
%
E
)))
(
at
level
102
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
val_scope
.
heap_lang/tests.v
View file @
8ca359a5
...
...
@@ -4,7 +4,7 @@ From heap_lang Require Import wp_tactics heap notation.
Import
uPred
.
Section
LangTests
.
Definition
add
:
=
(#
21
+
#
21
)%
L
.
Definition
add
:
=
(#
21
+
#
21
)%
E
.
Goal
∀
σ
,
prim_step
add
σ
(#
42
)
σ
None
.
Proof
.
intros
;
do_step
done
.
Qed
.
Definition
rec_app
:
expr
:
=
((
rec
:
"f"
"x"
:
=
"f"
"x"
)
#
0
).
...
...
@@ -14,7 +14,7 @@ Section LangTests.
by
eapply
(
Ectx_step
_
_
_
_
_
[]),
(
BetaS
_
_
_
_
#
0
).
Qed
.
Definition
lam
:
expr
:
=
λ
:
"x"
,
"x"
+
#
21
.
Goal
∀
σ
,
prim_step
(
lam
#
21
)%
L
σ
add
σ
None
.
Goal
∀
σ
,
prim_step
(
lam
#
21
)%
E
σ
add
σ
None
.
Proof
.
intros
.
rewrite
/
lam
.
(* FIXME: do_step does not work here *)
by
eapply
(
Ectx_step
_
_
_
_
_
[]),
(
BetaS
<>
"x"
(
"x"
+
#
21
)
_
#
21
).
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment