Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
iris-coq
Commits
ccf74b05
Commit
ccf74b05
authored
Mar 05, 2016
by
Robbert Krebbers
Browse files
Improve indentation.
parent
86dec2b6
Changes
2
Hide whitespace changes
Inline
Side-by-side
heap_lang/par.v
View file @
ccf74b05
...
...
@@ -3,10 +3,11 @@ From heap_lang Require Import wp_tactics notation.
Import
uPred
.
Definition
par
:
val
:=
λ
:
"fs"
,
let
:
"handle"
:=
^
spawn
(
Fst
'
"fs"
)
in
let:
"v2"
:=
Snd
'
"fs"
#()
in
let:
"v1"
:=
^
join
'
"handle"
in
Pair
'
"v1"
'
"v2"
.
λ
:
"fs"
,
let:
"handle"
:=
^
spawn
(
Fst
'
"fs"
)
in
let:
"v2"
:=
Snd
'
"fs"
#()
in
let:
"v1"
:=
^
join
'
"handle"
in
Pair
'
"v1"
'
"v2"
.
Notation
Par
e1
e2
:=
(
^
par
(
Pair
(
λ
:
<>
,
e1
)
(
λ
:
<>
,
e2
)))
%
E
.
Notation
ParV
e1
e2
:=
(
par
(
Pair
(
λ
:
<>
,
e1
)
(
λ
:
<>
,
e2
)))
%
E
.
(
*
We
want
both
par
and
par
^
to
print
like
this
.
*
)
...
...
heap_lang/spawn.v
View file @
ccf74b05
...
...
@@ -4,11 +4,15 @@ From heap_lang Require Import wp_tactics notation.
Import
uPred
.
Definition
spawn
:
val
:=
λ
:
"f"
,
let
:
"c"
:=
ref
(
InjL
#
0
)
in
Fork
(
'
"c"
<-
InjR
(
'
"f"
#()))
;;
'
"c"
.
λ
:
"f"
,
let:
"c"
:=
ref
(
InjL
#
0
)
in
Fork
(
'
"c"
<-
InjR
(
'
"f"
#()))
;;
'
"c"
.
Definition
join
:
val
:=
rec:
"join"
"c"
:=
match
:
!
'
"c"
with
InjR
"x"
=>
'
"x"
|
InjL
<>
=>
'
"join"
'
"c"
end
.
rec:
"join"
"c"
:=
match:
!
'
"c"
with
InjR
"x"
=>
'
"x"
|
InjL
<>
=>
'
"join"
'
"c"
end
.
(
**
The
monoids
we
need
.
*
)
(
*
Not
bundling
heapG
,
as
it
may
be
shared
with
other
users
.
*
)
...
...
Write
Preview
Supports
Markdown
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