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

PVS Bug 717


Synopsis:        axiom translation and theory instantiation
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Nov  8 12:10:01 2002
Originator:      Jaco van de Pol
Organization:    cwi.nl
Release:         PVS 3.0 Beta
Environment: 
 System:          
 Architecture: 

Description: 
  Dear Sam,
  I found two problems with theory instantiations that I cannot
  explain. I guess these are bugs.
  
  I have the simple theories:
  
  test1: THEORY
  BEGIN
  Bool: TYPE+ = bool
  T: TYPE+
  e: T
  f: [T->T]
  E110: AXIOM FORALL (b:Bool,x:T) : f(x) = x
  END test1
  
  test2: THEORY
  BEGIN
  IMPORTING test1{{T:=nat, f(x:nat):= x, e := 5}} AS T
  a: LEMMA 1=2
  END test2
  
  PROBLEM 1:
  ==========
  Now the importing generates one TCC, while I expected two:
  T_TCC1: OBLIGATION EXISTS (x: nat): TRUE;
  
  Indeed replacing Bool by bool in E110,
  so we get: E110: AXIOM FORALL (b:bool,x:T) : f(x) = x 
  we obtain two TCCS as expected:
  T_TCC1: OBLIGATION EXISTS (x: nat): TRUE;
  T_TCC2: OBLIGATION FORALL (b: bool, x: nat): x = x;
  
  I don't understand the difference.
  
  PROBLEM 2:
  ==========
  While proving LEMMA a, I type:
  (LEMMA "E110")
  Then I get:
  {-1}  FORALL (b: bool, x: T): f(x) = x
    |-------
  [1]   1 = 2
  
  So AXIOM E110 has not been translated, as I would expect.
  Do I miss something? (The second problem remains the same 
  if I remove all references to Bool or bool).
  
  Regards,
  Jaco van de Pol
  
  
  

How-To-Repeat: 

Fix: 
Problem 1: a test for whether a mapped axiom was fully-interpreted was not
           quite right in generate-mapped-axiom-tccs.

Problem 2: the name resolution functions were checking whether there were
           actuals, and generating a trivial resolution if there weren't.
           The fix in get-decl-resolutions is to also check whether there
           are any theory instances in the importings that have mappings.

(defun generate-mapped-axiom-tccs (modinst)
  (let ((mod (get-theory modinst)))
    (unless (or (eq mod (current-theory))
		(member modinst (assuming-instances (current-theory))
			:test #'tc-eq))
      ;; Don't want to save this module instance unless it does not
      ;; depend on any conditions, including implicit ones in the
      ;; prover
      (unless (or (or *in-checker* *in-evaluator*)
		  *tcc-conditions*)
	(push modinst (assuming-instances (current-theory))))
      (dolist (ax (remove-if-not #'axiom? (theory mod)))
	(let* ((*old-tcc-name* nil)
	       (ndecl (make-mapped-axiom-tcc-decl ax modinst)))
	  (if ndecl
	      (let ((refs (collect-references (definition ndecl))))
		(if (some #'(lambda (d)
			      (and (same-id (module d) modinst)
				   (interpretable? d)))
			  refs)
		    (pvs-warning "Axiom ~a not translated" (id ax))
		    (insert-tcc-decl 'mapped-axiom modinst ax ndecl)))
	      (incf (tccs-simplified))))))))

(defun get-decl-resolutions (decl acts mappings kind args)
  (let ((dth (module decl)))
    (when (and (kind-match (kind-of decl) kind)
	       (or (eq dth (current-theory))
		   (and (visible? decl)
			(can-use-for-assuming-tcc? decl)))
	       (not (disallowed-free-variable? decl))
	       (or (null args)
		   (case kind
		     (type (and (formals decl)
				(or (length= (formals decl) args)
				    (singleton? (formals decl))
				    (singleton? args))))
		     (expr (let ((ftype (find-supertype (type decl))))
			     (and (typep ftype 'funtype)
				  (or (length= (domain-types ftype) args)
				      (singleton? (domain-types ftype))
				      (singleton? args)))))
		     (t nil))))
      (if (null acts)
	  (if (and (or (eq dth (current-theory))
		       (and (null (formals-sans-usings dth))
			    (every (complement #'mappings)
				   (gethash dth (current-using-hash)))))
		   (null args))
	      (list (mk-resolution decl (mk-modname (id (module decl)))
				   (case kind
				     (expr (type decl))
				     (type (type-value decl)))))
	      (let* ((modinsts (decl-args-compatible? decl args mappings))
		     (unint-modinsts
		      (remove-if
			  #'(lambda (mi)
			      (and (mappings mi)
				   (find decl (mappings mi)
					 :key #'(lambda (m)
						  (and (mapping-def? m)
						       (declaration (lhs m)))))))
			modinsts))
		     (thinsts (if nil ;mappings have already been considered
				  (remove-if-not
				      #'(lambda (mi)
					  (matching-mappings mappings mi))
				    unint-modinsts)
				  unint-modinsts)))
		(mapcar #'(lambda (thinst)
			    (if mappings
				(make-resolution-with-mappings
				 decl thinst mappings)
				(make-resolution decl thinst)))
		  thinsts)))
	  (when (length= acts (formals-sans-usings dth))
	    (let* ((thinsts (gethash dth (current-using-hash)))
		   (genthinst (find-if-not #'actuals thinsts)))
	      (if genthinst
		  (let* ((nacts (compatible-parameters?
				 acts (formals-sans-usings dth)))
			 (dthi (when nacts
				 (mk-modname-no-tccs (id dth) nacts)))
			 (*generate-tccs* 'none))
		    (when dthi
		      (set-type-actuals dthi)
		      #+pvsdebug (assert (fully-typed? dthi))
		      (when (compatible-arguments? decl dthi args
						   (current-theory))
			(list (make-resolution decl dthi)))))
		  (let* ((modinsts (decl-args-compatible? decl args mappings))
			 (thinsts (matching-decl-theory-instances
				   acts dth modinsts)))
		    (when thinsts
		      (mapcar #'(lambda (thinst)
				  (make-resolution decl thinst))
			thinsts))))))))))
	      			

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