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