# PVS Bug 464

Synopsis: Problem with reduce_nat
Severity: serious
Priority: medium
Responsible: owre
State: analyzed
Class: sw-bug
Arrival-Date: Thu Jun 15 12:40:01 2000
Originator: Natarajan Shankar
Organization: csl.sri.com
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
Sam:
Can you look at ~shankar/pvs/examples/bugs/mason/6-15-2000/Landin.pvs
and see why it is reporting a type error of the form
fifth argument to reduce_nat has the wrong type
Found: [[{i: integers.int | i >= 0},
[# dom: finite_sets_def[nat].finite_set,
sub: [(dom) -> Syntax_adt.E] #]] ->
{i: integers.int | i >= 0}]
Expected: [[{i: integers.int | i >= 0},
[# dom: finite_sets_def[nat].finite_set,
sub: [(dom) -> Syntax_adt.E] #]] ->
{i: integers.int | i >= 0}]
-Shankar
There are actually two bugs here. The first is that the error is
misleading, since the types look the same. The second is that for some
reason, nat is being printed as {i: integers.int | i >= 0}.
How-To-Repeat:
Fix:
The first bug is related to the fact that since E is a subtype of Syntax,
the type of the argument should be
[nat, [# dom: finite_set[nat], sub: [(dom) -> nat] #] -> nat]
rather than
[nat, [# dom: finite_set[nat], sub: [(dom) -> E] #] -> nat]
Internally, it actually has the right type, but it is being printed
incorrectly. This is because the substitution is being done in the
canonical form of the type, but not in the print-type.
The second relates to how subtypes are (re)typechecked - the print-type
needs to be copied correctly.