Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

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.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools