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

PVS Bug 478


Synopsis:        Type checker problem
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Aug 21 23:40:02 2000
Originator:      "ian a. mason"
Organization:    turing.une.edu.au
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  Sam or Shankar,
  
  I have a problem with the typechecker. It can't seem to resolve
  something, even though it should be obvious. Note that 
  "p_var!1" is clearly of type (P?). There is a link to the dmp file
  (this is the 18th tcc of Fill) from our pvs page:
  
  "http://mcs.une.edu.au/~pvs/"
  
  Any help will be gladly appreciated!! (also on the page is a paper
  we submitted to cats about the church rosser experience)
  
  cheers, i.
  
  
  Rule? (typepred "i(p_var!1)")
  i does not uniquely resolve - one of:
  
    Syntax_adt.i : [(X?) -> nat],
  
    Syntax_adt.i : [(P?) -> nat]
  Restoring the state.
  Fill_TCC18 :  
  
  {-1}  P?(p_var!1)
  [-2]  P?(p_var!1)
  [-3]  e!1 = H(p_var!1, s_var!1)
  [-4]  dom(s_var!1)(i(p_var!1))
    |-------
  [1]   A?(Subst(sub(s_var!1)(i(p_var!1)),
                 (# dom := dom(s_var!1),
                    sub
                      := LAMBDA (j: (dom(s_var!1))):
                           v!1(sub(s_var!1)(j), s!1) #)))
  [2]   X?(Subst(sub(s_var!1)(i(p_var!1)),
                 (# dom := dom(s_var!1),
                    sub
                      := LAMBDA (j: (dom(s_var!1))):
                           v!1(sub(s_var!1)(j), s!1) #)))
  [3]   L?(Subst(sub(s_var!1)(i(p_var!1)),
                 (# dom := dom(s_var!1),
                    sub
                      := LAMBDA (j: (dom(s_var!1))):
                           v!1(sub(s_var!1)(j), s!1) #)))
  [4]   O?(Subst(sub(s_var!1)(i(p_var!1)),
                 (# dom := dom(s_var!1),
                    sub
                      := LAMBDA (j: (dom(s_var!1))):
                           v!1(sub(s_var!1)(j), s!1) #)))
  [5]   H?(Subst(sub(s_var!1)(i(p_var!1)),
                 (# dom := dom(s_var!1),
                    sub
                      := LAMBDA (j: (dom(s_var!1))):
                           v!1(sub(s_var!1)(j), s!1) #)))
  
  Rule? 
  
  
  -- 
  	Dr Ian A. Mason.
          Acting Convener of Computer Science
  	Computer Science Postgraduate Coordinator
  	School of Mathematical & Computer Sciences
  	University of New England
  	Armidale    2351
  	N.S.W  
  	Australia
  
  	phone:  +61 (0)2 6773 2327 
  	fax:    +61 (0)2 6773 3312 
  	iam@turing.une.edu.au
          http://mcs.une.edu.au/~iam/

How-To-Repeat: 

Fix: 
Modified mk-adt-subtype to generate the eta-reduced form of subtypes with
only a single corresponding recognizer.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools