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
9733052e
Commit
9733052e
authored
Jul 17, 2010
by
Andrei Paskevich
Browse files
produce non-covered patterns correctly
parent
b48d1573
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/core/pattern.ml
View file @
9733052e
...
...
@@ -103,9 +103,8 @@ module Compile (X : Action) = struct
else
begin
try
compile
constructors
tl
wilds
with
NonExhaustive
pl
->
let
al
=
List
.
map
pat_wild
cs
.
ls_args
in
let
pat
=
pat_app
cs
al
(
of_option
cs
.
ls_value
)
in
raise
(
NonExhaustive
(
pat
::
pl
))
let
al
=
List
.
map
(
fun
t
->
pat_wild
t
.
t_ty
)
al
in
raise
(
NonExhaustive
(
pat_app
cs
al
ty
::
pl
))
end
|
_
->
begin
let
pw
=
pat_wild
ty
in
...
...
@@ -115,8 +114,9 @@ module Compile (X : Action) = struct
let
unused
=
Sls
.
filter
test
css
in
if
Sls
.
is_empty
unused
then
None
else
let
cs
=
Sls
.
choose
unused
in
let
pl
=
List
.
map
pat_wild
cs
.
ls_args
in
Some
(
pat_app
cs
pl
(
of_option
cs
.
ls_value
))
let
tm
=
ty_match
Mtv
.
empty
(
of_option
cs
.
ls_value
)
ty
in
let
wild
ty
=
pat_wild
(
ty_inst
tm
ty
)
in
Some
(
pat_app
cs
(
List
.
map
wild
cs
.
ls_args
)
ty
)
in
let
base
=
match
nopat
with
|
None
->
[]
...
...
src/core/pretty.ml
View file @
9733052e
...
...
@@ -199,15 +199,15 @@ and print_tnode pri fmt t = match t.t_node with
print_ls
fs
(
print_list
space
(
print_lterm
5
))
tl
print_ty
t
.
t_ty
|
Tif
(
f
,
t1
,
t2
)
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if %a@ then %a@ else %a"
)
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if
@[
%a@
]
then %a@ else %a"
)
print_fmla
f
print_term
t1
print_term
t2
|
Tlet
(
t1
,
tb
)
->
let
v
,
t2
=
t_open_bound
tb
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a =
@ %a
in@ %a"
)
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a =
@[%a@]
in@ %a"
)
print_vs
v
(
print_lterm
4
)
t1
print_term
t2
;
forget_var
v
|
Tcase
(
t1
,
bl
)
->
fprintf
fmt
"match
%a
with@
\n
@[<hov>%a@]@
\n
end"
fprintf
fmt
"match
@[%a@]
with@
\n
@[<hov>%a@]@
\n
end"
print_term
t1
(
print_list
newline
print_tbranch
)
bl
|
Teps
fb
->
let
v
,
f
=
f_open_bound
fb
in
...
...
@@ -240,15 +240,15 @@ and print_fnode pri fmt f = match f.f_node with
|
Fnot
f
->
fprintf
fmt
(
protect_on
(
pri
>
4
)
"not %a"
)
(
print_lfmla
4
)
f
|
Fif
(
f1
,
f2
,
f3
)
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if %a@ then %a@ else %a"
)
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if
@[
%a@
]
then %a@ else %a"
)
print_fmla
f1
print_fmla
f2
print_fmla
f3
|
Flet
(
t
,
f
)
->
let
v
,
f
=
f_open_bound
f
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a =
@ %a
in@ %a"
)
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a =
@[%a@]
in@ %a"
)
print_vs
v
(
print_lterm
4
)
t
print_fmla
f
;
forget_var
v
|
Fcase
(
t
,
bl
)
->
fprintf
fmt
"match
%a
with@
\n
@[<hov>%a@]@
\n
end"
fprintf
fmt
"match
@[%a@]
with@
\n
@[<hov>%a@]@
\n
end"
print_term
t
(
print_list
newline
print_fbranch
)
bl
and
print_tbranch
fmt
br
=
...
...
@@ -487,9 +487,8 @@ let () = Exn_printer.register
fprintf
fmt
"Ident %s is already declared, with a different declaration"
id
.
id_string
|
Decl
.
NonExhaustiveExpr
(
pl
,
e
)
->
fprintf
fmt
"Non-exhaustive pattern list:@
\n
@[<hov 2>%a@]@
\n
in expression %a"
(
print_list
newline
print_pat
)
pl
print_expr
e
fprintf
fmt
"Pattern @[%a@] is not covered in expression:@
\n
@[%a@]"
(
print_list
comma
print_pat
)
pl
print_expr
e
|
_
->
raise
exn
end
src/util/exn_printer.ml
View file @
9733052e
...
...
@@ -31,19 +31,23 @@ let () =
exception
Exit_loop
let
exn_printer
fmt
exn
=
let
test
f
=
try
f
fmt
exn
;
raise
Exit_loop
with
Exit_loop
->
raise
Exit_loop
|
_
->
()
in
try
Stack
.
iter
test
exn_printers
let
exn_printer
fmt
exn
=
let
test
f
=
try
Format
.
fprintf
fmt
"@[%a@]"
f
exn
;
raise
Exit_loop
with
|
Exit_loop
->
raise
Exit_loop
|
_
->
()
in
try
Stack
.
iter
test
exn_printers
with
Exit_loop
->
()
(** For Config *)
let
()
=
register
(
fun
fmt
exn
->
match
exn
with
|
Config
.
Dynlink
.
Error
error
->
Format
.
fprintf
fmt
"Dynlink: %s"
(
Config
.
Dynlink
.
error_message
error
)
|
_
->
raise
exn
)
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