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
32f90012
Commit
32f90012
authored
Jan 20, 2011
by
Jean-Christophe
Browse files
programs: debugging in progress
parent
3ce8ffb1
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/programs/TODO
View file @
32f90012
X refs -> mutable types
X loadpath: how to retrieve program files? (cannot use "env")
o what about pervasives old, at, label, unit = (), lt_nat
o what about pervasives old, at, label, unit = ()
in particular, how to prevent old and at from being used in programs?
can we get rid of theories/programs.why?
o fmla_effect
o bench/programs/good/recfun: FIXME
o
global reference
o
fixed precedence of label (label L: e) wrt sequence (e ; e)
o
vacid_0_spare_array: typing bug with create
o
misfix _[_] and _[_] := _ for arrays (both in logic and programs)
o fixed precedence of label (label L: e) wrt sequence (e ; e)
o misfix _[_] and _[_] := _
src/programs/pgm_pretty.mli
View file @
32f90012
open
Format
val
print_
expr
:
Format
.
formatter
->
Pgm_t
tree
.
expr
->
unit
val
print_
pv
:
formatter
->
Pgm_t
ypes
.
T
.
pvsymbol
->
unit
val
print_recfun
:
Format
.
formatter
->
Pgm_ttree
.
recfun
->
unit
val
print_expr
:
formatter
->
Pgm_ttree
.
expr
->
unit
val
print_recfun
:
formatter
->
Pgm_ttree
.
recfun
->
unit
src/programs/pgm_types.ml
View file @
32f90012
...
...
@@ -361,10 +361,19 @@ end = struct
let
rec
eq_type_v
v1
v2
=
match
v1
,
v2
with
|
Tpure
ty1
,
Tpure
ty2
->
ty_equal
ty1
ty2
|
Tarrow
_
,
Tarrow
_
->
false
(* TODO? *)
|
Tarrow
(
bl1
,
c1
)
,
Tarrow
(
bl2
,
c2
)
->
assert
(
List
.
length
bl1
=
List
.
length
bl2
);
(* FIXME? *)
let
s
=
List
.
fold_left2
(
fun
s
v1
v2
->
Mpv
.
add
v1
(
R
.
Rlocal
v2
)
s
)
Mpv
.
empty
bl1
bl2
in
eq_type_c
(
subst_type_c
s
Mtv
.
empty
Mvs
.
empty
c1
)
c2
|
_
->
assert
false
false
and
eq_type_c
c1
c2
=
eq_type_v
c1
.
c_result_type
c2
.
c_result_type
&&
E
.
equal
c1
.
c_effect
c2
.
c_effect
(* pretty-printers *)
...
...
src/programs/pgm_typing.ml
View file @
32f90012
...
...
@@ -962,7 +962,9 @@ let rec print_iexpr fmt e = match e.iexpr_desc with
|
IElet
(
v
,
e1
,
e2
)
->
fprintf
fmt
"@[let %a = %a in@ %a@]"
print_vs
v
.
i_pgm
print_iexpr
e1
print_iexpr
e2
|
IEif
(
e1
,
e2
,
e3
)
->
fprintf
fmt
"@[if %a then %a else %a@]"
print_iexpr
e1
print_iexpr
e2
print_iexpr
e3
|
_
->
fprintf
fmt
"<other>"
...
...
@@ -1360,10 +1362,15 @@ and letrec gl env dl = (* : env * recfun list *)
map_fold_left
type1
Mvs
.
empty
dl
in
let
rec
fixpoint
m
=
(*
printf "fixpoint...@\n"; *)
(* printf "fixpoint...@\n"; *)
let
m'
,
dl'
=
one_step
m
in
let
same_effect
(
i
,_,_,_,_
)
=
E
.
equal
(
Mvs
.
find
i
.
i_pgm
m
)
.
c_effect
(
Mvs
.
find
i
.
i_pgm
m'
)
.
c_effect
let
same_effect
(
i
,
bl
,_,_,_
)
=
let
c
=
Mvs
.
find
i
.
i_pgm
m
and
c'
=
Mvs
.
find
i
.
i_pgm
m'
in
let
v
=
tarrow
bl
c
and
v'
=
tarrow
bl
c'
in
(* printf " v = %a@." print_type_v v; *)
(* printf " v'= %a@." print_type_v v'; *)
eq_type_v
v
v'
(* E.equal c.c_effect c'.c_effect *)
in
if
List
.
for_all
same_effect
dl
then
m
,
dl'
else
fixpoint
m'
in
...
...
tests/test-pgm-jcf.mlw
View file @
32f90012
...
...
@@ -4,8 +4,9 @@ module P
use import int.Int
use import module stdlib.Ref
let rec f5 (a b : ref int) =
if True then !b else f5 a b
let f1 () (a : ref int) = !a
let f2 (a : ref int) = f1 () a
end
...
...
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