Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
125
Issues
125
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
20fee52d
Commit
20fee52d
authored
Jul 30, 2015
by
Léon Gondelman
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Parser: add syntax "(e1.f1, e2.f2) <- (v1, v2)" for parallel assignments
parent
faf9a2be
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
21 additions
and
8 deletions
+21
-8
src/parser/parser.mly
src/parser/parser.mly
+16
-5
src/parser/ptree.ml
src/parser/ptree.ml
+1
-1
src/parser/typing.ml
src/parser/typing.ml
+4
-2
No files found.
src/parser/parser.mly
View file @
20fee52d
...
...
@@ -660,11 +660,22 @@ expr_:
|
IF
seq_expr
THEN
expr
%
prec
prec_no_else
{
Eif
(
$
2
,
$
4
,
mk_expr
(
Etuple
[]
)
$
startpos
$
endpos
)
}
|
expr
LARROW
expr
{
match
$
1
.
expr_desc
with
|
Eidapp
(
q
,
[
e1
])
->
Eassign
(
e1
,
q
,
$
3
)
|
Eidapp
(
Qident
id
,
[
e1
;
e2
])
when
id
.
id_str
=
mixfix
"[]"
->
Eidapp
(
Qident
{
id
with
id_str
=
mixfix
"[]<-"
}
,
[
e1
;
e2
;
$
3
])
|
_
->
raise
Error
}
{
let
loc
=
floc
$
startpos
$
endpos
in
let
rec
down
ll
rl
=
match
ll
,
rl
with
|
{
expr_desc
=
Eidapp
(
q
,
[
e1
])}
::
ll
,
e2
::
rl
->
(
e1
,
q
,
e2
)
::
down
ll
rl
|
{
expr_desc
=
Eidapp
(
Qident
id
,
[
_
;
_
]);
expr_loc
=
loc
}
::_,
_
::_
when
id
.
id_str
=
mixfix
"[]"
->
Loc
.
errorm
~
loc
"Parallel array assignments are not allowed"
|
{
expr_loc
=
loc
}
::_,
_
::_
->
Loc
.
errorm
~
loc
"Invalid left expression in an assignment"
|
[]
,
[]
->
[]
|
_
->
Loc
.
errorm
~
loc
"Invalid parallel assignment"
in
match
$
1
.
expr_desc
,
$
3
.
expr_desc
with
|
Eidapp
(
Qident
id
,
[
e1
;
e2
])
,
_
when
id
.
id_str
=
mixfix
"[]"
->
Eidapp
(
Qident
{
id
with
id_str
=
mixfix
"[]<-"
}
,
[
e1
;
e2
;
$
3
])
|
Etuple
ll
,
Etuple
rl
->
Eassign
(
down
ll
rl
)
|
Etuple
_
,
_
->
Loc
.
errorm
~
loc
"Invalid parallel assignment"
|
_
,
_
->
Eassign
(
down
[
$
1
]
[
$
3
])
}
|
LET
ghost
kind
pattern
EQUAL
seq_expr
IN
seq_expr
{
match
$
4
.
pat_desc
with
|
Pvar
id
->
Elet
(
id
,
$
2
,
$
3
,
$
6
,
$
8
)
...
...
src/parser/ptree.ml
View file @
20fee52d
...
...
@@ -128,7 +128,7 @@ and expr_desc =
|
Etuple
of
expr
list
|
Erecord
of
(
qualid
*
expr
)
list
|
Eupdate
of
expr
*
(
qualid
*
expr
)
list
|
Eassign
of
expr
*
qualid
*
expr
|
Eassign
of
(
expr
*
qualid
*
expr
)
list
(* control *)
|
Esequence
of
expr
*
expr
|
Eif
of
expr
*
expr
*
expr
...
...
src/parser/typing.ml
View file @
20fee52d
...
...
@@ -676,8 +676,10 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let
id
=
create_user_id
id
in
let
denv
=
denv_add_var
denv
id
(
dity_of_ity
ity_int
)
in
DEfor
(
id
,
efrom
,
dir
,
eto
,
inv
,
dexpr
muc
denv
e1
)
|
Ptree
.
Eassign
(
e1
,
q
,
e2
)
->
DEassign
[
dexpr
muc
denv
e1
,
find_record_field
muc
q
,
dexpr
muc
denv
e2
]
|
Ptree
.
Eassign
asl
->
let
mk_assign
(
e1
,
q
,
e2
)
=
dexpr
muc
denv
e1
,
find_record_field
muc
q
,
dexpr
muc
denv
e2
in
DEassign
(
List
.
map
mk_assign
asl
)
|
Ptree
.
Eraise
(
q
,
e1
)
->
let
xs
=
find_xsymbol
muc
q
in
let
e1
=
match
e1
with
...
...
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