Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
006726b2
Commit
006726b2
authored
Feb 17, 2014
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
minor improvement of an error message
parent
54554c44
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
16 additions
and
11 deletions
+16
-11
src/core/pretty.ml
src/core/pretty.ml
+6
-4
src/core/theory.ml
src/core/theory.ml
+4
-3
src/whyml/mlw_pretty.ml
src/whyml/mlw_pretty.ml
+6
-4
No files found.
src/core/pretty.ml
View file @
006726b2
...
...
@@ -506,8 +506,9 @@ let () = Exn_printer.register
|
Ty
.
BadTypeArity
({
ts_args
=
[]
}
as
ts
,
_
)
->
fprintf
fmt
"Type symbol %a expects no arguments"
print_ts
ts
|
Ty
.
BadTypeArity
(
ts
,
app_arg
)
->
fprintf
fmt
"Type symbol %a expects %i arguments but is applied to %i"
print_ts
ts
(
List
.
length
ts
.
ts_args
)
app_arg
let
i
=
List
.
length
ts
.
ts_args
in
fprintf
fmt
"Type symbol %a expects %i argument%s but is applied to %i"
print_ts
ts
i
(
if
i
=
1
then
""
else
"s"
)
app_arg
|
Ty
.
DuplicateTypeVar
tv
->
fprintf
fmt
"Type variable %a is used twice"
print_tv
tv
|
Ty
.
UnboundTypeVar
tv
->
...
...
@@ -518,9 +519,10 @@ let () = Exn_printer.register
fprintf
fmt
"%s %a expects no arguments"
(
if
ls
.
ls_value
=
None
then
"Predicate"
else
"Function"
)
print_ls
ls
|
Term
.
BadArity
(
ls
,
app_arg
)
->
fprintf
fmt
"%s %a expects %i arguments but is applied to %i"
let
i
=
List
.
length
ls
.
ls_args
in
fprintf
fmt
"%s %a expects %i argument%s but is applied to %i"
(
if
ls
.
ls_value
=
None
then
"Predicate"
else
"Function"
)
print_ls
ls
(
List
.
length
ls
.
ls_args
)
app_arg
print_ls
ls
i
(
if
i
=
1
then
""
else
"s"
)
app_arg
|
Term
.
EmptyCase
->
fprintf
fmt
"Empty match expression"
|
Term
.
DuplicateVar
vs
->
...
...
src/core/theory.ml
View file @
006726b2
...
...
@@ -907,10 +907,11 @@ let () = Exn_printer.register
Format
.
fprintf
fmt
"Metaproperty %s is already registered with \
a conflicting signature"
m
.
meta_name
|
BadMetaArity
(
m
,
n
)
->
Format
.
fprintf
fmt
"Metaproperty %s requires %d arguments but \
is applied to %d"
m
.
meta_name
(
List
.
length
m
.
meta_type
)
n
let
i
=
List
.
length
m
.
meta_type
in
Format
.
fprintf
fmt
"Metaproperty %s expects %d argument%s but \
is applied to %d"
m
.
meta_name
i
(
if
i
=
1
then
""
else
"s"
)
n
|
MetaTypeMismatch
(
m
,
t1
,
t2
)
->
Format
.
fprintf
fmt
"Metaproperty %s expects %a argument but \
Format
.
fprintf
fmt
"Metaproperty %s expects
a
%a argument but \
is applied to %a"
m
.
meta_name
print_meta_arg_type
t1
print_meta_arg_type
t2
|
_
->
raise
exn
...
...
src/whyml/mlw_pretty.ml
View file @
006726b2
...
...
@@ -432,12 +432,14 @@ let () = Exn_printer.register
|
Mlw_ty
.
BadItyArity
({
its_ts
=
{
ts_args
=
[]
}}
as
ts
,
_
)
->
fprintf
fmt
"Type symbol %a expects no arguments"
print_its
ts
|
Mlw_ty
.
BadItyArity
(
ts
,
app_arg
)
->
fprintf
fmt
"Type symbol %a expects %i arguments but is applied to %i"
print_its
ts
(
List
.
length
ts
.
its_ts
.
ts_args
)
app_arg
let
i
=
List
.
length
ts
.
its_ts
.
ts_args
in
fprintf
fmt
"Type symbol %a expects %i argument%s but is applied to %i"
print_its
ts
i
(
if
i
=
1
then
""
else
"s"
)
app_arg
|
Mlw_ty
.
BadRegArity
(
ts
,
app_arg
)
->
let
i
=
List
.
length
ts
.
its_regs
in
fprintf
fmt
"Type symbol %a expects \
%i region arguments but is applied to %i"
print_its
ts
(
List
.
length
ts
.
its_regs
)
app_arg
%i region argument
%
s but is applied to %i"
print_its
ts
i
(
if
i
=
1
then
""
else
"s"
)
app_arg
|
Mlw_ty
.
DuplicateRegion
r
->
fprintf
fmt
"Region %a is used twice"
print_reg
r
|
Mlw_ty
.
UnboundRegion
r
->
...
...
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