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

PVS Bug 562


Synopsis:        No methods applicable for generic function
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed May  9 18:25:00 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  --r5gRVUXMfa
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  if I run the proof of rel_const_cofib in the appended dump I get 
  
      Rerunning step: (REDUCE)
      Error: No methods applicable for generic function
  	   #<STANDARD-GENERIC-FUNCTION EXPRS> with args (a!1) of classes
  	   (NAME-EXPR)
        [condition type: PROGRAM-ERROR]
  
      Restart actions (select using :continue):
       0: Try calling it again
       1: Return to Top Level (an "abort" restart)
      [1c] PVS(24): (restore)
      rel_const_cofib.1 :  
  
  I use PVS Version 2.3 (patch level 1.2.2.133) on Linux ithif51
  2.2.18.
  
  Bye,
  
  Hendrik
  
  
  --r5gRVUXMfa
  Content-Type: text/plain
  Content-Disposition: inline;
  	filename="dump"
  Content-Transfer-Encoding: 7bit
  
  %Patch files loaded: patch2 version 1.2.2.133
  
  $$$PVSHOME/.pvs.lisp
  
  ;; load patches
  
  ;(load "~/Privat/Pvs/pvs-patches/20.4/patch2")
  ;(load "~/Privat/Pvs/pvs-patches/20.4/bin/sun4-SunOS5/runtime/ws1s.so")
  ;(load "~/Privat/Pvs/pvs-patches/20.4/bin/sun4-SunOS5/runtime/mu.so")
  
  ; (load "~/Privat/Pvs/pvs-patches/9.5./patch2")
  ; (load "~/Privat/Pvs/pvs-patches/9.5./bin/sun4-SunOS5/runtime/ws1s.so")
  ; (load "~/Privat/Pvs/pvs-patches/9.5./bin/sun4-SunOS5/runtime/mu.so")
  
  ;(load "~/Privat/Pvs/pvs-patches/6.9.00/patch2")
  ;(load "~/Privat/Pvs/pvs-patches/6.9.00/bin/sun4-SunOS5/runtime/ws1s.so")
  ;(load "~/Privat/Pvs/pvs-patches/6.9.00/bin/sun4-SunOS5/runtime/mu.so")
  
  ; ;PL 118 - no solaris version
  ; (load "~/Privat/Pvs/pvs-patches/pl118/patch2")
  ; ;(load "~/Privat/Pvs/pvs-patches/pl118/bin/sun4-SunOS5/runtime/ws1s.so")
  ; ;(load "~/Privat/Pvs/pvs-patches/pl118/bin/sun4-SunOS5/runtime/mu.so")
  ; (load "~/Privat/Pvs/pvs-patches/pl118/bin/ix86-redhat5/runtime/ws1s.so")
  ; (load "~/Privat/Pvs/pvs-patches/pl118/bin/ix86-redhat5/runtime/mu.so")
  
  ; ;PL 120 Athlon
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/patch2")
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/bin/ix86-redhat5/runtime/ws1s.so")
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/bin/ix86-redhat5/runtime/mu.so")
  
  
  ; ;PL 120 SUN
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/patch2")
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/bin/sun4-SunOS5/runtime/ws1s.so")
  ; (load "~/Privat/Pvs/pvs-patches/19.12.00/bin/sun4-SunOS5/runtime/mu.so")
  
  
  ; Sorry, I tested it on a rather trivial example - your example allowed me
  ; to determine where the problem is.  The following code should fix this -
  ; just add it to your ~/.pvs.lisp file.
  
  (defmethod pp* ((ex infix-application))
    (with-slots (operator argument) ex
      (if (and (typep operator 'name-expr)
  	     (memq (id operator) *infix-operators*)
  	     (typep argument 'tuple-expr)
  	     (= (length (exprs argument)) 2)
  	     (not (or (mod-id operator)
  		      (library operator)
  		      (actuals operator))))
  	(let ((lhs (car (exprs argument)))
  	      (rhs (cadr (exprs argument)))
  	      (oper (sbst-symbol (id operator))))
  	  (pprint-logical-block (nil nil)
  	    (pprint-indent :block 1)
  	    (if (and (zerop (parens lhs))
  		     (< (precedence lhs 'left)
  			(gethash oper (second *expr-prec-info*))))
  		(progn (write-char #\()
  		       (pp* lhs)
  		       (write-char #\)))
  		(pp* lhs))
  	    (write-char #\space)
  	    (pprint-newline :fill)
  	    (if (eq (id operator) 'O)
  		(pp* '|o|)
  		(pp* (id operator)))
  	    (write-char #\space)
  	    (pprint-newline :fill)
  	    (if (and (zerop (parens rhs))
  		     (< (precedence rhs 'right)
  			(gethash oper (third *expr-prec-info*))))
  		(progn (write-char #\()
  		       (pp* rhs)
  		       (write-char #\)))
  		(pp* rhs))))
  	(call-next-method))))
  
  $$$crash.pvs
  
  Product[A,B,C : Type] : Theory
  Begin
    f : Var [C -> A]
    g : Var [C -> B]
  
    pair(f,g) : [C -> [A,B]] =
  	lambda(c : C) : (f(c), g(c))
  
    pair_char : Lemma
  	let p1 = lambda(ab : [A,B]) : proj_1(ab),
  	    p2 = lambda(ab : [A,B]) : proj_2(ab)
  	in
  		p1 o pair(f,g) = f and
  		p2 o pair(f,g) = g
  
  end Product
  
  
  
  ProductFun[A,B,C,D : Type] : Theory
  Begin
    Importing Product
  
    f : Var [A -> C]
    g : Var [B -> D]
  
    times(f,g) : [[A,B] -> [C,D]] =
  	let p1 = lambda(ab : [A,B]) : proj_1(ab),
  	    p2 = lambda(ab : [A,B]) : proj_2(ab)
          in pair(f o p1, g o p2)
  
    times_char : Lemma
      times(f,g) = lambda(c : [A,B]) : (f(proj_1(c)), g(proj_2(c)))
  
  end ProductFun
  
  
  
  
  simple[A : Type] : Theory
  Begin
  
    a : Var A
  
  
    Importing Product
    delta : [A -> [A,A]] = pair(id,id)
  
    delta_char : Lemma
  	Forall(a : A) : delta(a) = (a,a)
  
  end simple
  
  
  TimesProp[A,B : Type] : Theory
  Begin
    IMPORTING ProductFun, simple
  
    times_id : Lemma
      times(id[A],id[B]) = id[[A,B]]
  end TimesProp
  
  Fibre[A : Type] : Theory
  Begin
    a : Var A
  
    truth : PRED[A] = lambda(a) : true;
  
    P,Q : Var PRED[A]
    fib_and(P , Q ) : PRED[A] =
  	    lambda(a) : P(a) and Q(a)
  end Fibre
  
  
  Pred[A, B : Type] : Theory
  Begin
    IMPORTING Fibre
  
    f :  Var [A -> B]
  
    star(f) : [PRED[B] -> PRED[A]] =
      lambda(Q:PRED[B]) : lambda(a:A) : Q(f(a))
  
    coprod(f) : [PRED[A] -> PRED[B]] =
      lambda(P:PRED[A]) : lambda(b:B) : Exists(a:(P)) : b = f(a)
  
  end Pred
  
  
  
  
  simpleCont[A : Type] : Theory
  Begin
    Importing Pred, simple
  
    equality : PRED[[A,A]] = coprod(delta)(truth)
  
    equality_char : lemma equality = { ab : [A,A] | proj_1(ab) = proj_2(ab) }
  
  end simpleCont
  
  
  
  PredProd[A,B : Type] : Theory
  Begin
    Importing Pred
  
    P : Var PRED[A]
    Q : Var PRED[B]
  
    /\(P,Q) : PRED[[A,B]] =
  	let p1 = lambda(ab : [A,B]) : Proj_1(ab),
              p2 = lambda(ab : [A,B]) : Proj_2(ab)
          in fib_and( star(p1)(P), star(p2)(Q) )
  
  
  end PredProd
  
  
  RelCart[A,B,C,D : Type] : Theory
  Begin
    Importing PredProd, ProductFun
  
    R : Var PRED[[A,B]]
    S : Var PRED[[C,D]]
  
    iso : [ [[A,C],[B,D]] -> [[A,B],[C,D]] ] = lambda(x : [[A,C],[B,D]] ) :
  	((proj_1(proj_1(x)), proj_1(proj_2(x))),
  	  (proj_2(proj_1(x)), proj_2(proj_2(x))))
  
    relprod(R,S) : PRED[[[A,C],[B,D]]] = star(iso)( R /\ S )
  
    rel_prod_char : Lemma relprod(R,S) =
  	{ (w : [A,C], v: [B, D]) | R(proj_1(w), proj_1(v))
  				and S(proj_2(w), proj_2(v)) }
  
  end RelCart
  
  
  CofibRel[A,B,C,D, X,Y,U,V : Type] : Theory
  Begin
    Importing simpleCont, RelCart, TimesProp
  
    R : Var PRED[[X,Y]]
    S : Var PRED[[A,B]]
    u : Var [X -> U]   
    v : Var [Y -> V]   
    f : Var [A -> C]   
    g : Var [B -> D]   
  
    rel_const_cofib : Lemma
          coprod(times( id[X],id[X]))( equality[X] ) = equality[X]
  
  end CofibRel
  
  
  
  
  
  
  
  $$$crash.prf
  (|EmptyFun|)
  (|Zero|)
  (|Initial|)
  (|Unit|)
  (|Bang|)
  (|Collection|)
  (|Lift|)
  (|Coproduct|)
  (|CoproductPair|)
  (|CoproductFun|)
  (|Pi_12|)
  (|Product|)
  (|ProductFun|)
  (|simple|)
  (|IdComp|)
  (|TimesProp|)
  (|ExpCat1|)
  (|ExpCat2|)
  (|Exp|)
  (|Fibre|)
  (|BinaryCollection|)
  (|Pred|)
  (|simpleCont|)
  (|RelOp|)
  (|RelOpOp|)
  (|PredCont|)
  (|PullbackCone|)
  (|Pullback|)
  (|SetPullback|)
  (BC)
  (|BCRel|)
  (|BCfor_graph|)
  (|Frobenius|)
  (|FrobeniusRel|)
  (|PredProd|)
  (|PredCoprod|)
  (|PredExp|)
  (|SymmTransRefl|)
  (|RelCart|)
  (|RelExp|)
  (|PredOverlineProp|)
  (|PredProps|)
  (|PredPropsBinary|)
  (|FibProps|)
  (|BisimProjProp|)
  (|CapInvProp|)
  (|RelCompProp|)
  (|RelPropsOp|)
  (|RelProps|)
  (|RelPropsBinary|)
  (|FibRel|)
  (|CofibRel|
   (|rel_const_cofib| "" (APPLY-EXTENSIONALITY :HIDE? T)
    ((""
      (AUTO-REWRITE "plus_char" "delta_char" "times_char" "exp_char"
                    "equality_char" "pred_prod_char" "pred_coprod_char"
                    "pred_exp_char" "rel_prod_char" "rel_sum_char"
                    "rel_exp_char" "pred_t_char2" "coprod" "prod" "id"
                    "o" "times_id" "star_id")
      (("" (ASSERT)
        (("" (IFF)
          (("" (PROP)
            (("1" (REDUCE) (("1" (POSTPONE) NIL)))
             ("2" (POSTPONE) NIL))))))))))))
  
  
  --r5gRVUXMfa--

How-To-Repeat: 

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