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
119
Issues
119
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
1d0d5289
Commit
1d0d5289
authored
Mar 23, 2010
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
classes d'operateurs 1 2 3 et 4
parent
4523328d
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
90 additions
and
54 deletions
+90
-54
src/parser/lexer.mll
src/parser/lexer.mll
+20
-10
src/parser/parser.mly
src/parser/parser.mly
+10
-19
src/programs/pgm_main.ml
src/programs/pgm_main.ml
+1
-1
src/programs/pgm_parser.mly
src/programs/pgm_parser.mly
+6
-4
src/programs/pgm_ptree.mli
src/programs/pgm_ptree.mli
+19
-16
src/programs/pgm_typing.ml
src/programs/pgm_typing.ml
+32
-2
src/test.why
src/test.why
+2
-2
No files found.
src/parser/lexer.mll
View file @
1d0d5289
...
...
@@ -127,6 +127,14 @@ let int_literal =
decimal_literal
|
hex_literal
|
oct_literal
|
bin_literal
let
hexadigit
=
[
'
0
'
-
'
9
'
'
a'
-
'
f'
'
A'
-
'
F'
]
let
op_char_1
=
[
'
=
'
'
<
'
'
>
'
]
let
op_char_2
=
[
'
+
'
'
-
'
]
let
op_char_3
=
[
'
*
'
'
/
'
'
%
'
]
let
op_char_4
=
[
'
!
'
'
$
'
'
&
'
'
?
'
'
@
'
'
^
'
'
~
'
'.'
'
:
'
'
|
'
'
#
'
]
let
op_char_34
=
op_char_3
|
op_char_4
let
op_char_234
=
op_char_2
|
op_char_34
let
op_char_1234
=
op_char_1
|
op_char_234
rule
token
=
parse
|
"#"
space
*
(
"
\"
"
([
^
'\010'
'\013'
'
"' ]* as file) "
\
""
)
?
space
*
(
digit
+
as
line
)
space
*
(
digit
+
as
char
)
space
*
"#"
...
...
@@ -168,22 +176,24 @@ rule token = parse
{
ARROW
}
|
"<->"
{
LRARROW
}
|
"="
{
EQUAL
}
|
"<>"
|
"<"
|
"<="
|
">"
|
">="
as
s
{
OP0
s
}
|
"+"
|
"-"
as
c
{
OP2
(
String
.
make
1
c
)
}
|
"*"
|
"/"
|
"%"
|
"!"
as
c
{
OP3
(
String
.
make
1
c
)
}
|
"."
{
DOT
}
|
"|"
{
BAR
}
|
"="
{
EQUAL
}
|
"["
{
LEFTSQ
}
|
"]"
{
RIGHTSQ
}
|
"|"
{
BAR
}
|
op_char_1234
*
op_char_1
op_char_1234
*
as
s
{
OP1
s
}
|
op_char_234
*
op_char_2
op_char_234
*
as
s
{
OP2
s
}
|
op_char_34
*
op_char_3
op_char_34
*
as
s
{
OP3
s
}
|
op_char_4
+
as
s
{
OP4
s
}
|
"
\"
"
{
string_start_loc
:=
loc
lexbuf
;
STRING
(
string
lexbuf
)
}
|
eof
...
...
src/parser/parser.mly
View file @
1d0d5289
...
...
@@ -40,7 +40,6 @@
let
infix
s
=
"infix "
^
s
let
prefix
s
=
"prefix "
^
s
let
postfix
s
=
"postfix "
^
s
%
}
...
...
@@ -48,7 +47,7 @@
%
token
<
string
>
LIDENT
UIDENT
%
token
<
string
>
INTEGER
%
token
<
string
>
OP
0
OP1
OP2
OP3
%
token
<
string
>
OP
1
OP2
OP3
OP4
%
token
<
Ptree
.
real_constant
>
FLOAT
%
token
<
string
>
STRING
...
...
@@ -88,12 +87,11 @@
%
right
OR
%
right
AND
%
nonassoc
NOT
%
left
EQUAL
OP0
%
left
OP1
%
left
EQUAL
OP1
%
left
OP2
%
left
OP3
%
left
OP4
%
nonassoc
prefix_op
%
nonassoc
postfix_op
/*
Entry
points
*/
...
...
@@ -148,23 +146,21 @@ lident_rich:
{
{
id
=
infix
$
3
;
id_loc
=
loc
()
}
}
|
LEFTPAR
lident_op
UNDERSCORE
RIGHTPAR
{
{
id
=
prefix
$
2
;
id_loc
=
loc
()
}
}
/*
|
LEFTPAR
UNDERSCORE
lident_op
RIGHTPAR
{
{
id
=
postfix
$
3
;
id_loc
=
loc
()
}
}
*/
;
lident_op
:
|
OP
0
{
$
1
}
|
OP
1
{
$
1
}
|
OP2
{
$
1
}
|
OP3
{
$
1
}
|
OP4
{
$
1
}
|
EQUAL
{
"="
}
;
any_op
:
|
OP
0
{
$
1
}
|
OP
1
{
$
1
}
|
OP2
{
$
1
}
|
OP3
{
$
1
}
|
OP4
{
$
1
}
;
uident
:
...
...
@@ -362,9 +358,6 @@ lexpr:
|
lexpr
EQUAL
lexpr
{
let
id
=
{
id
=
infix
"="
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
;
$
3
]))
}
|
lexpr
OP0
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
;
$
3
]))
}
|
lexpr
OP1
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
;
$
3
]))
}
...
...
@@ -374,14 +367,12 @@ lexpr:
|
lexpr
OP3
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
;
$
3
]))
}
|
lexpr
OP4
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
;
$
3
]))
}
|
any_op
lexpr
%
prec
prefix_op
{
let
id
=
{
id
=
prefix
$
1
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
2
]))
}
/*
|
lexpr
any_op
%
prec
postfix_op
{
let
id
=
{
id
=
postfix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
1
]))
}
*/
|
qualid
{
mk_pp
(
PPvar
$
1
)
}
|
qualid
LEFTPAR
list1_lexpr_sep_comma
RIGHTPAR
...
...
src/programs/pgm_main.ml
View file @
1d0d5289
...
...
@@ -69,7 +69,7 @@ let type_file file =
List
.
fold_left
(
fun
uc
d
->
match
d
with
|
Dlogic
dl
->
List
.
fold_left
(
Typing
.
add_decl
env
Mnm
.
empty
)
uc
dl
|
Dcode
(
id
,
e
)
->
ignore
(
Pgm_typing
.
code
id
e
);
uc
)
|
Dcode
(
id
,
e
)
->
ignore
(
Pgm_typing
.
code
uc
id
e
);
uc
)
uc
p
in
()
...
...
src/programs/pgm_parser.mly
View file @
1d0d5289
...
...
@@ -28,8 +28,8 @@
let
loc_i
i
=
(
rhs_start_pos
i
,
rhs_end_pos
i
)
let
loc_ij
i
j
=
(
rhs_start_pos
i
,
rhs_end_pos
j
)
let
mk_expr
d
=
{
expr_loc
=
loc
()
;
expr_desc
=
d
}
let
mk_expr_i
i
d
=
{
expr_loc
=
loc_i
i
;
expr_desc
=
d
}
let
mk_expr
d
=
{
expr_loc
=
loc
()
;
expr_
info
=
()
;
expr_
desc
=
d
}
let
mk_expr_i
i
d
=
{
expr_loc
=
loc_i
i
;
expr_
info
=
()
;
expr_
desc
=
d
}
(* FIXME: factorize with parser/parser.mly *)
let
infix
s
=
"infix "
^
s
...
...
@@ -45,10 +45,12 @@
Eapply
(
f
,
a
)
|
a
::
l
->
let
loc
=
join
f
.
expr_loc
a
.
expr_loc
in
mk_apply
{
expr_loc
=
loc
;
expr_desc
=
Eapply
(
f
,
a
)
}
l
mk_apply
{
expr_loc
=
loc
;
expr_
info
=
()
;
expr_
desc
=
Eapply
(
f
,
a
)
}
l
let
mk_apply_id
id
=
let
e
=
{
expr_desc
=
Eident
(
Qident
id
);
expr_loc
=
id
.
id_loc
}
in
let
e
=
{
expr_desc
=
Eident
(
Qident
id
);
expr_info
=
()
;
expr_loc
=
id
.
id_loc
}
in
mk_apply
e
let
mk_infix
e1
op
e2
=
...
...
src/programs/pgm_ptree.mli
View file @
1d0d5289
...
...
@@ -27,33 +27,36 @@ type constant = Term.constant
type
assertion_kind
=
Aassert
|
Aassume
|
Acheck
type
lexpr
=
Ptree
.
lexpr
type
loop_annotation
=
{
loop_invariant
:
Ptree
.
lexpr
option
;
loop_variant
:
Ptree
.
lexpr
option
;
loop_invariant
:
lexpr
option
;
loop_variant
:
lexpr
option
;
}
type
expr
=
{
expr_desc
:
expr_desc
;
type
'
info
expr
=
{
expr_desc
:
'
info
expr_desc
;
expr_loc
:
loc
;
expr_info
:
'
info
;
}
and
expr_desc
=
and
'
info
expr_desc
=
|
Econstant
of
constant
|
Eident
of
qualid
|
Eapply
of
expr
*
expr
|
Esequence
of
expr
*
expr
|
Eif
of
expr
*
expr
*
expr
|
Eapply
of
'
info
expr
*
'
info
expr
|
Esequence
of
'
info
expr
*
'
info
expr
|
Eif
of
'
info
expr
*
'
info
expr
*
'
info
expr
|
Eskip
|
Eassert
of
assertion_kind
*
Ptree
.
lexpr
|
Elazy_and
of
expr
*
expr
|
Elazy_or
of
expr
*
expr
|
Elet
of
ident
*
expr
*
expr
|
Eghost
of
expr
|
Elabel
of
ident
*
expr
|
Ewhile
of
expr
*
loop_annotation
*
expr
|
Eassert
of
assertion_kind
*
lexpr
|
Elazy_and
of
'
info
expr
*
'
info
expr
|
Elazy_or
of
'
info
expr
*
'
info
expr
|
Elet
of
ident
*
'
info
expr
*
'
info
expr
|
Eghost
of
'
info
expr
|
Elabel
of
ident
*
'
info
expr
|
Ewhile
of
'
info
expr
*
loop_annotation
*
'
info
expr
type
decl
=
|
Dcode
of
ident
*
expr
|
Dcode
of
ident
*
unit
expr
|
Dlogic
of
Ptree
.
decl
list
type
file
=
decl
list
...
...
src/programs/pgm_typing.ml
View file @
1d0d5289
...
...
@@ -17,8 +17,38 @@
(* *)
(**************************************************************************)
let
code
id
e
=
assert
false
(*TODO*)
open
Theory
open
Pgm_ptree
type
env
=
{
env_uc
:
theory_uc
;
}
let
create_env
uc
=
assert
false
(*TODO*)
let
rec
expr
env
e
=
let
d
,
ty
=
expr_desc
env
e
.
expr_loc
e
.
expr_desc
in
{
expr_desc
=
d
;
expr_info
=
ty
;
expr_loc
=
e
.
expr_loc
}
and
expr_desc
env
loc
=
function
_
->
assert
false
(*TODO*)
(* | Econstant of constant *)
(* | Eident of qualid *)
(* | Eapply of 'info expr * 'info expr *)
(* | Esequence of 'info expr * 'info expr *)
(* | Eif of 'info expr * 'info expr * 'info expr *)
(* | Eskip *)
(* | Eassert of assertion_kind * lexpr *)
(* | Elazy_and of 'info expr * 'info expr *)
(* | Elazy_or of 'info expr * 'info expr *)
(* | Elet of ident * 'info expr * 'info expr *)
(* | Eghost of 'info expr *)
(* | Elabel of ident * 'info expr *)
(* | Ewhile of 'info expr * loop_annotation * 'info expr *)
let
code
uc
id
e
=
let
env
=
create_env
uc
in
ignore
(
expr
env
e
)
(*
Local Variables:
...
...
src/test.why
View file @
1d0d5289
...
...
@@ -27,8 +27,8 @@ end
theory Test_conjunction
use import prelude.Int
goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x
=
-8) and x*x*2 = 8)
goal G2 : forall x:int. (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x
=
-8) and x*x*2 = 8)
goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x
=
-8) and x*x*2 = 8)
goal G2 : forall x:int. (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x
=
-8) and x*x*2 = 8)
end
theory Split_conj
...
...
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