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

PVS Bug 866


Synopsis:        No methods applicable for generic function (introduced in 3.2)
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Nov 16 04:35:01 2004
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  although there was a problem (cf report #757), the following
  typecheck in previous versions. In 3.2. the typechecker crashes.
  
  
  Z : Theory
  Begin
    z : int
  End Z
  
  Y : Theory
  Begin
    My_Z : Theory = Z
  
    zy : Axiom z = 3
  End Y
  
  YImp : Theory
  Begin
    IMPORTING Y{{My_Z := Z}}
  End YImp
  
  
  
  Bye,
  
  Hendrik

How-To-Repeat: 

Fix: 
Fixed get-interpreted-mapping to only add declarations that are different,
and subst-mod-params* (name-expr) to handle bindings associated with
declarations, as occurs in mappings.

(defun get-interpreted-mapping (theory interpretation theory-name)
  (let* ((*subst-mod-params-map-bindings* nil)
	 (mapping (make-subst-mod-params-map-bindings
		   theory-name (mappings theory-name) nil))
	 (int-decls (when interpretation (all-decls interpretation))))
    (when interpretation
      (dolist (decl (interpretable-declarations theory))
	(unless (assq decl mapping)
	  (let ((fdecl (find decl int-decls
			     :test #'(lambda (x y)
				       (and (declaration? y)
					    (same-id x y))))))
	    (unless (eq decl fdecl)
	      (push (cons decl fdecl) mapping))))))
    #+pvsdebug (assert (every #'cdr mapping))
    mapping))

(defmethod subst-mod-params* ((expr name-expr) modinst bindings)
  (declare (ignore modinst))
  (let* ((decl (declaration expr))
	 (act (cdr (assq decl bindings))))
    (if act
	(if (declaration? act)
	    (mk-name-expr (id act) nil nil
			  (mk-resolution act
			    (mk-modname (id (module act)))
			    (type act)))
	    (expr act))
	(let ((nexpr (call-next-method)))
	  (if (eq nexpr expr)
	      expr
	      (let ((ntype (type (resolution nexpr))))
		(lcopy nexpr 'type ntype)))))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools