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
16
Merge Requests
16
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
0615e692
Commit
0615e692
authored
Mar 05, 2014
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
alternative implementation of commit
e66e2a3f
parent
683e3dae
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
44 additions
and
52 deletions
+44
-52
examples/quicksort.mlw
examples/quicksort.mlw
+1
-1
src/parser/parser.mly
src/parser/parser.mly
+43
-51
No files found.
examples/quicksort.mlw
View file @
0615e692
...
...
@@ -51,7 +51,7 @@ module Quicksort
assert { qs_partition (at a 'N) a l !m r v };
'O: quick_rec a (!m + 1) r;
assert { qs_partition (at a 'O) a l !m r v };
assert { qs_partition (at a 'N) a l !m r v }
assert { qs_partition (at a 'N) a l !m r v }
;
end
let quicksort (a: array int) =
...
...
src/parser/parser.mly
View file @
0615e692
...
...
@@ -191,7 +191,9 @@ end
%
nonassoc
prec_mark
%
nonassoc
prec_fun
%
nonassoc
IN
%
right
SEMICOLON
%
nonassoc
below_SEMI
%
nonassoc
SEMICOLON
%
nonassoc
LET
VAL
%
nonassoc
prec_no_else
%
nonassoc
DOT
ELSE
GHOST
%
nonassoc
prec_named
...
...
@@ -1121,32 +1123,18 @@ list1_rec_defn:
|
rec_defn
WITH
list1_rec_defn
{
$
1
::
$
3
}
;
inner_list1_rec_defn
:
|
inner_rec_defn
{
[
$
1
]
}
|
inner_rec_defn
WITH
inner_list1_rec_defn
{
$
1
::
$
3
}
rec_defn
:
|
top_ghost
lident_rich
labels
list1_binder
opt_cast
spec
EQUAL
spec
expr
{
add_lab
$
2
$
3
,
$
1
,
(
$
4
,
$
5
,
$
9
,
spec_union
$
6
$
8
)
}
;
inner_rec_defn
:
|
top_ghost
lident_rich
labels
list1_binder
opt_cast
spec
EQUAL
spec
final_expr
|
top_ghost
lident_rich
labels
list1_binder
opt_cast
spec
EQUAL
spec
seq_expr
{
add_lab
$
2
$
3
,
$
1
,
(
$
4
,
$
5
,
$
9
,
spec_union
$
6
$
8
)
}
;
fun_defn
:
|
list1_binder
opt_cast
spec
EQUAL
spec
expr
{
(
$
1
,
$
2
,
$
6
,
spec_union
$
3
$
5
)
}
;
inner_fun_defn
:
|
list1_binder
opt_cast
spec
EQUAL
spec
final_expr
|
list1_binder
opt_cast
spec
EQUAL
spec
seq_expr
{
(
$
1
,
$
2
,
$
6
,
spec_union
$
3
$
5
)
}
;
fun_expr
:
|
FUN
list1_binder
spec
ARROW
spec
expr
%
prec
prec_fun
|
FUN
list1_binder
spec
ARROW
spec
seq_
expr
%
prec
prec_fun
{
(
$
2
,
None
,
$
6
,
spec_union
$
3
$
5
)
}
;
...
...
@@ -1181,66 +1169,68 @@ expr:
{
let
b
=
rhs_start_pos
1
in
List
.
fold_left
(
fun
f
(
e
,
a
)
->
mk_expr_l
(
Loc
.
extract
(
b
,
e
))
(
Eapply
(
f
,
a
)))
$
1
$
2
}
|
IF
final
_expr
THEN
expr
ELSE
expr
|
IF
seq
_expr
THEN
expr
ELSE
expr
{
mk_expr
(
Eif
(
$
2
,
$
4
,
$
6
))
}
|
IF
final
_expr
THEN
expr
%
prec
prec_no_else
|
IF
seq
_expr
THEN
expr
%
prec
prec_no_else
{
mk_expr
(
Eif
(
$
2
,
$
4
,
mk_expr
(
Etuple
[]
)))
}
/*
|
expr
SEMICOLON
expr
{
mk_expr
(
Esequence
(
$
1
,
$
3
))
}
*/
|
assertion_kind
LEFTBRC
lexpr
RIGHTBRC
{
mk_expr
(
Eassert
(
$
1
,
$
3
))
}
|
expr
AMPAMP
expr
{
mk_expr
(
Elazy
(
LazyAnd
,
$
1
,
$
3
))
}
|
expr
BARBAR
expr
{
mk_expr
(
Elazy
(
LazyOr
,
$
1
,
$
3
))
}
|
LET
pattern
EQUAL
final_expr
IN
expr
|
LET
pattern
EQUAL
seq_expr
IN
seq_
expr
{
match
$
2
.
pat_desc
with
|
PPpvar
id
->
mk_expr
(
Elet
(
id
,
Gnone
,
$
4
,
$
6
))
|
PPpwild
->
mk_expr
(
Elet
(
id_anonymous
()
,
Gnone
,
$
4
,
$
6
))
|
PPptuple
[]
->
mk_expr
(
Elet
(
id_anonymous
()
,
Gnone
,
{
$
4
with
expr_desc
=
Ecast
(
$
4
,
PPTtuple
[]
)
}
,
$
6
))
|
_
->
mk_expr
(
Ematch
(
$
4
,
[
$
2
,
$
6
]))
}
|
LET
GHOST
pat_arg
EQUAL
final_expr
IN
expr
|
LET
GHOST
pat_arg
EQUAL
seq_expr
IN
seq_
expr
{
match
$
3
.
pat_desc
with
|
PPpvar
id
->
mk_expr
(
Elet
(
id
,
Gghost
,
$
5
,
$
7
))
|
PPpwild
->
mk_expr
(
Elet
(
id_anonymous
()
,
Gghost
,
$
5
,
$
7
))
|
PPptuple
[]
->
mk_expr
(
Elet
(
id_anonymous
()
,
Gghost
,
{
$
5
with
expr_desc
=
Ecast
(
$
5
,
PPTtuple
[]
)
}
,
$
7
))
|
_
->
mk_expr
(
Ematch
({
$
5
with
expr_desc
=
Eghost
$
5
}
,
[
$
3
,
$
7
]))
}
|
LET
lident
labels
inner_fun_defn
IN
expr
|
LET
lident
labels
fun_defn
IN
seq_
expr
{
mk_expr
(
Efun
(
add_lab
$
2
$
3
,
Gnone
,
$
4
,
$
6
))
}
|
LET
lident_op_id
labels
inner_fun_defn
IN
expr
|
LET
lident_op_id
labels
fun_defn
IN
seq_
expr
{
mk_expr
(
Efun
(
add_lab
$
2
$
3
,
Gnone
,
$
4
,
$
6
))
}
|
LET
GHOST
lident
labels
inner_fun_defn
IN
expr
|
LET
GHOST
lident
labels
fun_defn
IN
seq_
expr
{
mk_expr
(
Efun
(
add_lab
$
3
$
4
,
Gghost
,
$
5
,
$
7
))
}
|
LET
GHOST
lident_op_id
labels
inner_fun_defn
IN
expr
|
LET
GHOST
lident_op_id
labels
fun_defn
IN
seq_
expr
{
mk_expr
(
Efun
(
add_lab
$
3
$
4
,
Gghost
,
$
5
,
$
7
))
}
|
LET
lident_op_id
labels
EQUAL
final_expr
IN
expr
|
LET
lident_op_id
labels
EQUAL
seq_expr
IN
seq_
expr
{
mk_expr
(
Elet
(
add_lab
$
2
$
3
,
Gnone
,
$
5
,
$
7
))
}
|
LET
GHOST
lident_op_id
labels
EQUAL
final_expr
IN
expr
|
LET
GHOST
lident_op_id
labels
EQUAL
seq_expr
IN
seq_
expr
{
mk_expr
(
Elet
(
add_lab
$
3
$
4
,
Gghost
,
$
6
,
$
8
))
}
|
LET
LEMMA
lident_rich
labels
EQUAL
final_expr
IN
expr
|
LET
LEMMA
lident_rich
labels
EQUAL
seq_expr
IN
seq_
expr
{
mk_expr
(
Elet
(
add_lab
$
3
$
4
,
Glemma
,
$
6
,
$
8
))
}
|
LET
LEMMA
lident_rich
labels
inner_fun_defn
IN
expr
|
LET
LEMMA
lident_rich
labels
fun_defn
IN
seq_
expr
{
mk_expr
(
Efun
(
add_lab
$
3
$
4
,
Glemma
,
$
5
,
$
7
))
}
|
LET
REC
inner_list1_rec_defn
IN
expr
|
LET
REC
list1_rec_defn
IN
seq_
expr
{
mk_expr
(
Erec
(
$
3
,
$
5
))
}
|
fun_expr
{
mk_expr
(
Elam
$
1
)
}
|
VAL
top_ghost
lident_rich
labels
tail_type_c
IN
expr
|
VAL
top_ghost
lident_rich
labels
tail_type_c
IN
seq_
expr
{
mk_expr
(
Elet
(
add_lab
$
3
$
4
,
$
2
,
mk_expr_l
(
floc_i
5
)
(
Eany
$
5
)
,
$
7
))
}
|
MATCH
final
_expr
WITH
bar_
program_match_cases
END
|
MATCH
seq
_expr
WITH
bar_
program_match_cases
END
{
mk_expr
(
Ematch
(
$
2
,
$
5
))
}
|
MATCH
list2_expr_sep_comma
WITH
bar_
program_match_cases
END
{
mk_expr
(
Ematch
(
mk_expr
(
Etuple
$
2
)
,
$
5
))
}
|
quote_uident
COLON
expr
%
prec
prec_mark
|
quote_uident
COLON
seq_
expr
%
prec
prec_mark
{
mk_expr
(
Emark
(
$
1
,
$
3
))
}
|
LOOP
loop_annotation
final
_expr
END
|
LOOP
loop_annotation
seq
_expr
END
{
mk_expr
(
Eloop
(
$
2
,
$
3
))
}
|
WHILE
final_expr
DO
loop_annotation
final
_expr
DONE
|
WHILE
seq_expr
DO
loop_annotation
seq
_expr
DONE
{
mk_expr
(
Ewhile
(
$
2
,
$
4
,
$
5
))
}
|
FOR
lident
EQUAL
final_expr
for_direction
final
_expr
DO
for_loop_invariant
final
_expr
DONE
|
FOR
lident
EQUAL
seq_expr
for_direction
seq
_expr
DO
for_loop_invariant
seq
_expr
DONE
{
mk_expr
(
Efor
(
$
2
,
$
4
,
$
5
,
$
6
,
$
8
,
$
9
))
}
|
ABSURD
{
mk_expr
Eabsurd
}
...
...
@@ -1248,22 +1238,24 @@ expr:
{
mk_expr
(
Ecast
(
$
1
,
$
3
))
}
|
RAISE
uqualid
{
mk_expr
(
Eraise
(
$
2
,
None
))
}
|
RAISE
LEFTPAR
uqualid
final
_expr
RIGHTPAR
|
RAISE
LEFTPAR
uqualid
seq
_expr
RIGHTPAR
{
mk_expr
(
Eraise
(
$
3
,
Some
$
4
))
}
|
TRY
final
_expr
WITH
bar_
list1_handler_sep_bar
END
|
TRY
seq
_expr
WITH
bar_
list1_handler_sep_bar
END
{
mk_expr
(
Etry
(
$
2
,
$
5
))
}
|
ANY
simple_type_c
{
mk_expr
(
Eany
$
2
)
}
|
GHOST
expr
{
mk_expr
(
Eghost
$
2
)
}
|
ABSTRACT
spec
final
_expr
END
|
ABSTRACT
spec
seq
_expr
END
{
mk_expr
(
Eabstract
(
$
3
,
$
2
))
}
|
label
expr
%
prec
prec_named
{
mk_expr
(
Enamed
(
$
1
,
$
2
))
}
;
final_expr
:
|
expr
opt_semicolon
{
$
1
}
seq_expr
:
|
expr
%
prec
below_SEMI
{
$
1
}
|
expr
SEMICOLON
{
$
1
}
|
expr
SEMICOLON
seq_expr
{
mk_expr
(
Esequence
(
$
1
,
$
3
))
}
;
expr_arg
:
...
...
@@ -1284,9 +1276,9 @@ expr_dot:
expr_sub
:
|
expr_dot
DOT
lqualid_rich
{
mk_expr
(
Eidapp
(
$
3
,
[
$
1
]))
}
|
LEFTPAR
final
_expr
RIGHTPAR
|
LEFTPAR
seq
_expr
RIGHTPAR
{
$
2
}
|
BEGIN
final
_expr
END
|
BEGIN
seq
_expr
END
{
$
2
}
|
LEFTPAR
RIGHTPAR
{
mk_expr
(
Etuple
[]
)
}
...
...
@@ -1319,12 +1311,12 @@ list1_expr_arg:
;
list2_expr_sep_comma
:
|
final_
expr
COMMA
list1_expr_sep_comma
{
$
1
::
$
3
}
|
expr
COMMA
list1_expr_sep_comma
{
$
1
::
$
3
}
;
list1_expr_sep_comma
:
|
final_
expr
{
[
$
1
]
}
|
final_
expr
COMMA
list1_expr_sep_comma
{
$
1
::
$
3
}
|
expr
{
[
$
1
]
}
|
expr
COMMA
list1_expr_sep_comma
{
$
1
::
$
3
}
;
list1_handler_sep_bar
:
...
...
@@ -1333,9 +1325,9 @@ list1_handler_sep_bar:
;
handler
:
|
uqualid
ARROW
final
_expr
|
uqualid
ARROW
seq
_expr
{
(
$
1
,
None
,
$
3
)
}
|
uqualid
pat_arg
ARROW
final
_expr
|
uqualid
pat_arg
ARROW
seq
_expr
{
(
$
1
,
Some
$
2
,
$
4
)
}
;
...
...
@@ -1345,7 +1337,7 @@ program_match_cases:
;
program_match_case
:
|
pattern
ARROW
final
_expr
{
(
$
1
,$
3
)
}
|
pattern
ARROW
seq
_expr
{
(
$
1
,$
3
)
}
;
assertion_kind
:
...
...
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