Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
e63b87af
Commit
e63b87af
authored
Jul 16, 2010
by
Jean-Christophe Filliâtre
Browse files
programs: type-checking the any construct
parent
726da3e1
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/programs/ropes.mlw
0 → 100644
View file @
e63b87af
{
type char
use array.ArrayLength as S
type string = S.t char
logic empty_string : string
type rope =
| Str string (*ofs:*) int (len: int)
| App rope rope (len: int)
}
let empty () = Str empty_string 0 0
let length r = len r
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/ropes"
End:
*)
src/programs/pgm_typing.ml
View file @
e63b87af
...
...
@@ -1023,8 +1023,8 @@ and expr_desc gl env loc ty = function
|
IElabel
(
lab
,
e1
)
->
let
e1
=
expr
gl
env
e1
in
Elabel
(
lab
,
e1
)
,
e1
.
expr_type_v
,
e1
.
expr_effect
|
IEany
_
->
assert
false
(*TODO*)
|
IEany
c
->
Eany
c
,
c
.
c_result_type
,
c
.
c_effect
and
triple
gl
env
(
p
,
e
,
q
)
=
let
e
=
expr
gl
env
e
in
...
...
tests/test-pgm-jcf.mlw
View file @
e63b87af
let foo () =
{}
any {} int {result=2} + 1
{result=3}
let rec div x y variant {x} =
{ 0 <= x and 0 < y }
if y < x then
...
...
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