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

PVS Bug 825


Synopsis:        Datatype typecheck error + feature request
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Mar  8 09:45:00 2004
Originator:      Tamarah Arons
Organization:    weizmann.ac.il
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  This is both a bug report and a feature request.
  
  When I try to typecheck the theory 
  
  ss[STATE: TYPE+]: THEORY
   BEGIN
  
   TIME : TYPE = nat
  
   STATE_SEQ: DATATYPE
     BEGIN
      infinite(sequence: [TIME -> STATE]): infinite?t
      finite(size : nat, sequence : [below[size] -> STATE]): finite?
     END STATE_SEQ
  
   end ss
  
  I get the ``Error: No methods applicable for generic function'' error.
  
  The problem is the below[size] field. 
   finite(size : nat, sequence : below[10] ): finite? 
  does typecheck, but
   finite(size : nat, sequence : [below[10] -> STATE] ): finite? 
  and 
   finite(size : nat, sequence : below[size] ): finite? 
  both generate the no methods applicable error.
  
  I request that datatypes allowing dependent types please be added in 
  the future, if possible.
  
  (I am using PVS3.1 on Linux)
  
  Thanks,
  Tamarah
  

How-To-Repeat: 

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