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

PVS Bug 423


Synopsis:        File no longer typechecking after loading patch
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan 17 23:00:02 2000
Originator:      Tamarah Arons
Organization:    wisdom.weizmann.ac.il
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  I have loaded the patch with the result that my old theory, which I ran
  under the version 2-3 no longer type-checks and I cannot understand why.
  
  I get the error:
  
  = does not uniquely resolve - one of:
  
    equalities[[# head: naturalnumbers.nat,
     list: [mipsDefs[R, U, Z, M].AL_ID -> mipsDefs[R, U, Z, M].FL_ENTRY_TYPE],
     tail: mipsDefs[R, U, Z, M].AL_ID,
     wrap: booleans.bool #]].= : [[[# head: nat,
       list: [AL_ID[R, U, Z, M] -> FL_ENTRY_TYPE[R, U, Z, M]],
       tail: AL_ID[R, U, Z, M],
       wrap: bool #],
    [# head: nat,
       list: [AL_ID[R, U, Z, M] -> FL_ENTRY_TYPE[R, U, Z, M]],
       tail: AL_ID[R, U, Z, M],
       wrap: bool #]] ->
     boolean],
  
    equalities[mipsDefs[R, U, Z, M].FL_TYPE].= : [[FL_TYPE[R, U, Z, M], FL_TYPE
 [R, U, Z, M]] -> boolean]
  
  On the equality 
  
  FL_p =
                   IF t(prog(pc)) > 0
                     THEN (# head := succ(head(FL)),
                             tail := tail(FL),
                             wrap := wrap(FL) AND NOT succ(head(FL)) = 1,
                             list
                               := (LAMBDA rb:
                                     IF rb = head(FL)
                                       THEN list(FL)(rb) with [oc := FALSE]
                                     ELSE list(FL)(rb)
                                     ENDIF) #)
                   ELSE FL
                   ENDIF
  
  where 
   FL and FL_p are FL_TYPES defined in mipsDefs as :
  
   FL_ENTRY_TYPE: TYPE = [# oc: OCCUPIED, pr: PH_REG_ID #]
  
    FL_TYPE: TYPE =
    [# list: [AL_ID -> FL_ENTRY_TYPE], head: AL_ID, tail: AL_ID, wrap: bool #]
  
  I have no function called "equalities" anywhere, nor have I defined an = oper
 ator
  etc. 
  
  I would appreciate any suggestions on how to overcome this problem. 
  
  Thanks,
  Tamarah

How-To-Repeat: 

Fix: 
Added filter-equality-resolutions to take the compatible-types of any
resolutions that come from (dis)equalities.  This is needed since
find-supertype is used for creating the module instance, and it does not
lift record or tuple types, as it would be too expensive (and unnecessary).
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools