Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
ce84499d
Commit
ce84499d
authored
May 04, 2010
by
Jean-Christophe Filliâtre
Browse files
programs: typing match
parent
aae6d3b5
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/parser/typing.ml
View file @
ce84499d
...
...
@@ -392,12 +392,13 @@ and dterm_node loc env = function
Tlet
(
e1
,
x
,
e2
)
,
e2
.
dt_ty
|
PPmatch
(
el
,
bl
)
->
let
tl
=
List
.
map
(
dterm
env
)
el
in
let
tyl
=
List
.
map
(
fun
t
->
t
.
dt_ty
)
tl
in
let
tb
=
(* the type of all branches *)
let
tv
=
create_tvsymbol
(
id_user
"a"
loc
)
in
Tyvar
(
create_ty_decl_var
~
loc
~
user
:
false
tv
)
in
let
branch
(
pl
,
e
)
=
let
env
,
pl
=
dpat_list
env
tl
pl
in
let
env
,
pl
=
dpat_list
env
t
y
l
pl
in
let
loc
=
e
.
pp_loc
in
let
e
=
dterm
env
e
in
if
not
(
unify
e
.
dt_ty
tb
)
then
term_expected_type
~
loc
e
.
dt_ty
tb
;
...
...
@@ -488,8 +489,9 @@ and dfmla env e = match e.pp_desc with
Flet
(
e1
,
x
,
e2
)
|
PPmatch
(
el
,
bl
)
->
let
tl
=
List
.
map
(
dterm
env
)
el
in
let
tyl
=
List
.
map
(
fun
t
->
t
.
dt_ty
)
tl
in
let
branch
(
pl
,
e
)
=
let
env
,
pl
=
dpat_list
env
tl
pl
in
let
env
,
pl
=
dpat_list
env
t
y
l
pl
in
pl
,
dfmla
env
e
in
Fmatch
(
tl
,
List
.
map
branch
bl
)
...
...
@@ -501,20 +503,20 @@ and dfmla env e = match e.pp_desc with
|
PPeps
_
|
PPconst
_
|
PPcast
_
->
error
~
loc
:
e
.
pp_loc
PredicateExpected
and
dpat_list
env
tl
pl
=
and
dpat_list
env
t
y
l
pl
=
check_pat_linearity
pl
;
let
pattern
(
env
,
pl
)
pat
t
=
let
pattern
(
env
,
pl
)
pat
t
y
=
let
loc
=
pat
.
pat_loc
in
let
env
,
pat
=
dpat
env
pat
in
if
not
(
unify
pat
.
dp_ty
t
.
dt_
ty
)
then
term_expected_type
~
loc
pat
.
dp_ty
t
.
dt_
ty
;
if
not
(
unify
pat
.
dp_ty
ty
)
then
term_expected_type
~
loc
pat
.
dp_ty
ty
;
env
,
pat
::
pl
in
let
loc
=
(
List
.
hd
pl
)
.
pat_loc
in
let
env
,
pl
=
try
List
.
fold_left2
pattern
(
env
,
[]
)
pl
tl
let
env
,
pl
=
try
List
.
fold_left2
pattern
(
env
,
[]
)
pl
t
y
l
with
Invalid_argument
_
->
errorm
~
loc
"This pattern has length %d but is expected to have length %d"
(
List
.
length
pl
)
(
List
.
length
tl
)
(
List
.
length
pl
)
(
List
.
length
t
y
l
)
in
env
,
List
.
rev
pl
...
...
@@ -1010,6 +1012,6 @@ let retrieve lp env sl =
(*
Local Variables:
compile-command: "make -C ../.. test"
compile-command: "
unset LANG;
make -C ../.. test"
End:
*)
src/parser/typing.mli
View file @
ce84499d
...
...
@@ -67,4 +67,13 @@ val type_fmla : denv -> vsymbol Mstr.t -> Ptree.lexpr -> fmla
val
dty
:
denv
->
Ptree
.
pty
->
Denv
.
dty
type
dpattern
val
dpat
:
denv
->
Ptree
.
pattern
->
denv
*
dpattern
val
dpat_list
:
denv
->
Denv
.
dty
list
->
Ptree
.
pattern
list
->
denv
*
dpattern
list
val
pattern
:
vsymbol
Mstr
.
t
->
dpattern
->
vsymbol
Mstr
.
t
*
pattern
src/programs/pgm_ttree.ml
View file @
ce84499d
...
...
@@ -70,6 +70,7 @@ and dexpr_desc =
|
DEif
of
dexpr
*
dexpr
*
dexpr
|
DEwhile
of
dexpr
*
Pgm_ptree
.
loop_annotation
*
dexpr
|
DElazy
of
lazy_op
*
dexpr
*
dexpr
|
DEmatch
of
dexpr
list
*
(
Typing
.
dpattern
list
*
dexpr
)
list
|
DEskip
|
DEabsurd
...
...
@@ -122,6 +123,7 @@ and expr_desc =
|
Eif
of
expr
*
expr
*
expr
|
Ewhile
of
expr
*
loop_annotation
*
expr
|
Elazy
of
lazy_op
*
expr
*
expr
|
Ematch
of
expr
list
*
(
Term
.
pattern
list
*
expr
)
list
|
Eskip
|
Eabsurd
...
...
src/programs/pgm_typing.ml
View file @
ce84499d
...
...
@@ -197,8 +197,19 @@ and expr_desc env loc = function
let
e2
=
dexpr
env
e2
in
expected_type
e2
(
dty_bool
env
.
uc
);
DElazy
(
op
,
e1
,
e2
)
,
(
dty_bool
env
.
uc
)
|
Pgm_ptree
.
Ematch
(
_el
,
_bl
)
->
assert
false
(*TODO*)
|
Pgm_ptree
.
Ematch
(
el
,
bl
)
->
let
el
=
List
.
map
(
dexpr
env
)
el
in
let
tyl
=
List
.
map
(
fun
e
->
e
.
dexpr_type
)
el
in
let
ty
=
create_type_var
loc
in
(* the type of all branches *)
let
branch
(
pl
,
e
)
=
let
denv
,
pl
=
Typing
.
dpat_list
env
.
denv
tyl
pl
in
let
env
=
{
env
with
denv
=
denv
}
in
let
e
=
dexpr
env
e
in
expected_type
e
ty
;
pl
,
e
in
let
bl
=
List
.
map
branch
bl
in
DEmatch
(
el
,
bl
)
,
ty
|
Pgm_ptree
.
Eskip
->
DEskip
,
(
dty_unit
env
.
uc
)
|
Pgm_ptree
.
Eabsurd
->
...
...
@@ -332,6 +343,14 @@ and expr_desc uc env denv = function
Ewhile
(
expr
uc
env
e1
,
la
,
expr
uc
env
e2
)
|
DElazy
(
op
,
e1
,
e2
)
->
Elazy
(
op
,
expr
uc
env
e1
,
expr
uc
env
e2
)
|
DEmatch
(
el
,
bl
)
->
let
el
=
List
.
map
(
expr
uc
env
)
el
in
let
branch
(
pl
,
e
)
=
let
env
,
pl
=
map_fold_left
Typing
.
pattern
env
pl
in
(
pl
,
expr
uc
env
e
)
in
let
bl
=
List
.
map
branch
bl
in
Ematch
(
el
,
bl
)
|
DEskip
->
Eskip
|
DEabsurd
->
...
...
@@ -422,3 +441,12 @@ Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
(*
TODO:
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified
- typing effects
*)
tests/test-pgm-jcf.mlw
View file @
ce84499d
...
...
@@ -12,18 +12,16 @@ let test (n:int) =
in
is_even n
let rec is_even (x:int) =
let rec is_even (x:int) variant {x} =
{x>=1}
if x = 0 then True else not (is_odd (x-1))
{true}
and is_odd (x:int) =
and is_odd (x:int)
variant {x}
=
if x = 0 then False else not (is_even (x-1))
let b = is_even 2
(*
let rec mem (x:int) (l:int list) =
{ true }
match l with
...
...
@@ -31,7 +29,7 @@ let rec mem (x:int) (l:int list) =
| Cons (y, r) -> x = y || mem x r
end
{ true }
*)
let p =
let x = ref 0 in
x := 1;
...
...
@@ -47,7 +45,9 @@ let f (x : int ref) =
parameter g : x:int -> y:int ref -> { true } int { result = x + old(!y) }
let foo r = g 2 r
parameter r : int ref
let foo = g 2 r
(*
Local Variables:
...
...
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