Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

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 | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|