Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Actris
Commits
80bc8c13
Commit
80bc8c13
authored
May 06, 2020
by
Daniël Louwrink
Committed by
Jonas Kastberg
May 06, 2020
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
rename ref_mut to ref_uniq
parent
607b1342
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
18 additions
and
24 deletions
+18
-24
theories/logrel/operators.v
theories/logrel/operators.v
+1
-1
theories/logrel/subtyping_rules.v
theories/logrel/subtyping_rules.v
+2
-2
theories/logrel/term_types.v
theories/logrel/term_types.v
+7
-8
theories/logrel/term_typing_rules.v
theories/logrel/term_typing_rules.v
+8
-13
No files found.
theories/logrel/operators.v
View file @
80bc8c13
...
...
@@ -28,7 +28,7 @@ Section operators.
Proof
.
iIntros
(
v
).
by
iDestruct
1
as
(
b
)
"->"
.
Qed
.
Global
Instance
lty_int_unboxed
:
LTyUnboxed
(
Σ
:
=
Σ
)
lty_int
.
Proof
.
iIntros
(
v
).
by
iDestruct
1
as
(
i
)
"->"
.
Qed
.
Global
Instance
lty_ref_
mut
_unboxed
`
{
heapG
Σ
}
A
:
LTyUnboxed
(
ref_
mut
A
).
Global
Instance
lty_ref_
uniq
_unboxed
`
{
heapG
Σ
}
A
:
LTyUnboxed
(
ref_
uniq
A
).
Proof
.
iIntros
(
v
).
by
iDestruct
1
as
(
i
w
->)
"?"
.
Qed
.
Global
Instance
lty_ref_shr_unboxed
`
{
heapG
Σ
}
A
:
LTyUnboxed
(
ref_shr
A
).
Proof
.
iIntros
(
v
).
by
iDestruct
1
as
(
l
->)
"?"
.
Qed
.
...
...
theories/logrel/subtyping_rules.v
View file @
80bc8c13
...
...
@@ -215,9 +215,9 @@ Section subtyping_rules.
iApply
"Hcopy"
.
Qed
.
Lemma
lty_le_ref_
mut
A1
A2
:
Lemma
lty_le_ref_
uniq
A1
A2
:
▷
(
A1
<
:
A2
)
-
∗
ref_
mut
A1
<
:
ref_
mut
A2
.
ref_
uniq
A1
<
:
ref_
uniq
A2
.
Proof
.
iIntros
"#H1"
(
v
)
"!>"
.
iDestruct
1
as
(
l
w
->)
"[Hl HA]"
.
iDestruct
(
"H1"
with
"HA"
)
as
"HA"
.
...
...
theories/logrel/term_types.v
View file @
80bc8c13
...
...
@@ -24,11 +24,11 @@ The following types are defined:
operations that might consume a resource, but do not always do so, depending
on whether the type [A] is copyable. Such operations result in a [copy- A],
which can be turned into an [A] using subtyping when [A] is copyable.
- [ref_
mut
A]: the type of
mutable (unique)
references to a value of type [A].
- [ref_
uniq
A]: the type of
uniquely-owned mutable
references to a value of type [A].
Since the reference is guaranteed to be unique, it's possible for the type [A]
contained in the reference to change to a different type [B] by assigning to
the reference.
- [ref_shr A]: the type of mutable
(shared)
references to a value of type [A].
- [ref_shr A]: the type of
shared
mutable references to a value of type [A].
- [chan P]: the type of channels, governed by the session type [P].
In addition, some important properties, such as contractivity and
...
...
@@ -62,7 +62,7 @@ Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Definition
lty_copy
{
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
□
ltty_car
A
w
)%
I
.
Definition
lty_copy_minus
{
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
coreP
(
ltty_car
A
w
)).
Definition
lty_ref_
mut
`
{
heapG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
Definition
lty_ref_
uniq
`
{
heapG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
l
:
loc
)
(
v
:
val
),
⌜
w
=
#
l
⌝
∗
l
↦
v
∗
▷
ltty_car
A
v
)%
I
.
Definition
ref_shrN
:
=
nroot
.@
"shr_ref"
.
Definition
lty_ref_shr
`
{
heapG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
...
...
@@ -78,7 +78,7 @@ Instance: Params (@lty_prod) 1 := {}.
Instance
:
Params
(@
lty_sum
)
1
:
=
{}.
Instance
:
Params
(@
lty_forall
)
2
:
=
{}.
Instance
:
Params
(@
lty_sum
)
1
:
=
{}.
Instance
:
Params
(@
lty_ref_
mut
)
2
:
=
{}.
Instance
:
Params
(@
lty_ref_
uniq
)
2
:
=
{}.
Instance
:
Params
(@
lty_ref_shr
)
2
:
=
{}.
Instance
:
Params
(@
lty_chan
)
3
:
=
{}.
...
...
@@ -98,7 +98,7 @@ Notation "∀ A1 .. An , C" :=
Notation
"∃ A1 .. An , C"
:
=
(
lty_exist
(
λ
A1
,
..
(
lty_exist
(
λ
An
,
C
%
lty
))
..))
:
lty_scope
.
Notation
"'ref_
mut
' A"
:
=
(
lty_ref_
mut
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'ref_
uniq
' A"
:
=
(
lty_ref_
uniq
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'ref_shr' A"
:
=
(
lty_ref_shr
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'chan' A"
:
=
(
lty_chan
A
)
(
at
level
10
)
:
lty_scope
.
...
...
@@ -112,7 +112,6 @@ Section term_types.
Global
Instance
lty_copy_minus_ne
:
NonExpansive
(@
lty_copy_minus
Σ
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_arr_contractive
`
{
heapG
Σ
}
n
:
Proper
(
dist_later
n
==>
dist_later
n
==>
dist
n
)
lty_arr
.
Proof
.
...
...
@@ -150,9 +149,9 @@ Section term_types.
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(@
lty_exist
Σ
k
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_ref_
mut
_contractive
`
{
heapG
Σ
}
:
Contractive
lty_ref_
mut
.
Global
Instance
lty_ref_
uniq
_contractive
`
{
heapG
Σ
}
:
Contractive
lty_ref_
uniq
.
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_ref_
mut
_ne
`
{
heapG
Σ
}
:
NonExpansive
lty_ref_
mut
.
Global
Instance
lty_ref_
uniq
_ne
`
{
heapG
Σ
}
:
NonExpansive
lty_ref_
uniq
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_ref_shr_contractive
`
{
heapG
Σ
}
:
Contractive
lty_ref_shr
.
...
...
theories/logrel/term_typing_rules.v
View file @
80bc8c13
...
...
@@ -258,15 +258,10 @@ Section properties.
iIntros
(
w
)
"[$ HΓ3]"
.
by
iApply
env_ltyped_delete
.
Qed
.
<<<<<<<
HEAD
(** Mutable Reference properties *)
=======
(** Mutable Unique Reference properties *)
>>>>>>>
add
headers
to
files
Lemma
ltyped_alloc
Γ
1
Γ
2
e
A
:
(
Γ
1
⊨
e
:
A
⫤
Γ
2
)
-
∗
(
Γ
1
⊨
ref
e
:
ref_
mut
A
⫤
Γ
2
).
(
Γ
1
⊨
ref
e
:
ref_
uniq
A
⫤
Γ
2
).
Proof
.
iIntros
"#He"
(
vs
)
"!> HΓ1 /="
.
wp_bind
(
subst_map
vs
e
).
...
...
@@ -277,8 +272,8 @@ Section properties.
Qed
.
Lemma
ltyped_load
Γ
(
x
:
string
)
A
:
Γ
!!
x
=
Some
(
ref_
mut
A
)%
lty
→
⊢
Γ
⊨
!
x
:
A
⫤
<[
x
:
=
(
ref_
mut
(
copy
-
A
))%
lty
]>
Γ
.
Γ
!!
x
=
Some
(
ref_
uniq
A
)%
lty
→
⊢
Γ
⊨
!
x
:
A
⫤
<[
x
:
=
(
ref_
uniq
(
copy
-
A
))%
lty
]>
Γ
.
Proof
.
iIntros
(
Hx
vs
)
"!> HΓ"
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HA HΓ]"
;
first
done
.
...
...
@@ -288,7 +283,7 @@ Section properties.
iAssert
(
ltty_car
(
copy
-
A
)
w
)%
lty
as
"#HAm"
.
{
iApply
coreP_intro
.
iApply
"Hw"
.
}
iFrame
"Hw"
.
iAssert
(
ltty_car
(
ref_
mut
(
copy
-
A
))%
lty
#
l
)
with
"[Hl]"
as
"HA"
.
iAssert
(
ltty_car
(
ref_
uniq
(
copy
-
A
))%
lty
#
l
)
with
"[Hl]"
as
"HA"
.
{
iExists
l
,
w
.
iSplit
=>//.
iFrame
"Hl HAm"
.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"HA HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).
...
...
@@ -296,9 +291,9 @@ Section properties.
Qed
.
Lemma
ltyped_store
Γ
Γ
'
(
x
:
string
)
e
A
B
:
Γ
'
!!
x
=
Some
(
ref_
mut
A
)%
lty
→
Γ
'
!!
x
=
Some
(
ref_
uniq
A
)%
lty
→
(
Γ
⊨
e
:
B
⫤
Γ
'
)
-
∗
Γ
⊨
x
<-
e
:
()
⫤
<[
x
:
=
(
ref_
mut
B
)%
lty
]>
Γ
'
.
Γ
⊨
x
<-
e
:
()
⫤
<[
x
:
=
(
ref_
uniq
B
)%
lty
]>
Γ
'
.
Proof
.
iIntros
(
Hx
)
"#He"
.
iIntros
(
vs
)
"!> HΓ /="
.
wp_bind
(
subst_map
vs
e
).
...
...
@@ -307,7 +302,7 @@ Section properties.
rewrite
Hw
.
iDestruct
"HA"
as
(
l
v'
->)
"[Hl HA]"
.
wp_store
.
iSplitR
;
first
done
.
iAssert
(
ltty_car
(
ref_
mut
B
)%
lty
#
l
)
with
"[Hl HB]"
as
"HB"
.
iAssert
(
ltty_car
(
ref_
uniq
B
)%
lty
#
l
)
with
"[Hl HB]"
as
"HB"
.
{
iExists
l
,
v
.
iSplit
=>//.
iFrame
"Hl HB"
.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"HB HΓ'"
)
as
"HΓ'"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hw
).
...
...
@@ -316,7 +311,7 @@ Section properties.
(** Mutable Shared Reference properties *)
Lemma
ltyped_upgrade_shared
Γ
Γ
'
e
A
:
(
Γ
⊨
e
:
ref_
mut
(
copy
A
)
⫤
Γ
'
)
-
∗
(
Γ
⊨
e
:
ref_
uniq
(
copy
A
)
⫤
Γ
'
)
-
∗
Γ
⊨
e
:
ref_shr
A
⫤
Γ
'
.
Proof
.
iIntros
"#He"
(
vs
)
"!> HΓ"
.
iApply
wp_fupd
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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