[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Michael Hohmuth <hohmuth@inf.tu-dresden.de>*Subject*: Re: [Reposting again] Re: [Repost] Instantiating multiple theories simultaneously*From*: Sam Owre <owre@csl.sri.com>*Date*: Tue, 20 May 2003 11:44:48 -0700*cc*: Sam Owre <owre@csl.sri.com>, pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Tue, 20 May 2003 16:34:19 +0200." <7sptmdr8k4.fsf_-_@agnes.inf.tu-dresden.de>*Sender*: pvs-help-owner@csl.sri.com

Hi Michael, I found a fix for this particular problem, but there was one other bug that kept it from working properly. I'm including the patches below, they haven't been thoroughly tested; I hope you don't mind testing it for us. Just add it to your ~/.pvs.lisp file (create it if necessary) and restart pvs. Let me know how it works out, Thanks, Sam -------------- (in-package :pvs) (defmethod pp* ((decl mod-decl)) (with-slots (modname) decl (write 'THEORY) (write-char #\=) (write-char #\space) (pprint-newline :fill) (pp* modname))) (defun set-type-mapping-rhs (rhs lhs modinst mappings) (typecase (declaration lhs) (type-decl (if (type-value rhs) (set-type* (type-value rhs) nil) (type-error (expr rhs) "Type expected here"))) (mod-decl (let ((threses (remove-if (complement #'(lambda (r) (and (typep (declaration r) '(or module mod-decl formal-theory-decl)) (eq (id (modname (declaration lhs))) (id (theory-ref (declaration r))))))) (resolutions (expr rhs))))) (cond ((cdr threses) (type-error (expr rhs) "Theory name ~a is ambiguous" (expr rhs))) ((null threses) (type-error (expr rhs) "No resolution for theory name ~a" (expr rhs))) (t (setf (resolutions (expr rhs)) threses) (when (mappings (expr rhs)) (set-type-mappings (name-to-modname (expr rhs)))))))) (t (let* ((mapmodinst (lcopy modinst 'mappings mappings)) (subst-type (subst-mod-params (type (declaration lhs)) mapmodinst))) (set-type* (expr rhs) subst-type))))) (defmethod theory-ref ((d module)) d) (defmethod theory-ref ((d mod-decl)) (modname d)) (defmethod theory-ref ((d formal-theory-decl)) (theory-name d)) (defmethod theory-ref ((d modname)) d) (defmethod theory-ref ((d name-expr)) (theory-ref (declaration (resolution d)))) (defvar *subst-mod-free-params* nil) (defun subst-mod-params (obj modinst &optional theory) (assert *current-context*) (assert (modname? modinst)) (let* ((th (or theory (get-theory modinst))) (formals (formals-sans-usings th)) (*subst-mod-free-params* nil)) (if (or (mappings modinst) (and (actuals modinst) (or (some #'(lambda (ofp) (memq ofp formals)) (free-params obj)) (some #'(lambda (a) (and (name-expr? (expr a)) (module? (declaration (expr a))))) (actuals modinst))))) (let* ((*generate-tccs* 'none) (caches (get-subst-mod-params-caches modinst)) (*subst-mod-params-cache* (car caches)) (*subst-mod-params-eq-cache* (cdr caches)) (*smp-mappings* (mappings modinst)) (bindings (make-subst-mod-params-bindings modinst formals (actuals modinst) (mappings modinst) nil)) (nobj (subst-mod-params* obj modinst bindings))) #+pvsdebug (assert (or (eq obj nobj) (not (tc-eq obj nobj)))) #+pvsdebug (assert (equal bindings (pairlis formals (actuals modinst)))) #+pvsdebug (assert (or (typep nobj 'modname) (fully-instantiated? nobj))) nobj) obj))) (defun make-subst-mod-params-bindings (modinst formals actuals mappings bindings) (cond ((null formals) (setq *subst-mod-free-params* (mapcar #'car bindings)) (make-subst-mod-params-map-bindings modinst mappings bindings)) (t (let ((pred-binding (make-subst-mod-params-pred-binding modinst (car formals) (car actuals) bindings))) (make-subst-mod-params-bindings modinst (cdr formals) (cdr actuals) mappings (let ((nbindings (make-subst-mod-params-binding (car formals) (car actuals) bindings))) (if pred-binding (cons pred-binding nbindings) nbindings))))))) (defmethod make-subst-mod-params-map-bindings* ((decl mod-decl) rhs bindings) (let* ((thname (theory-ref (expr rhs))) (interpreted-theory (generated-theory decl)) (source-theory (get-theory (theory-name decl))) (pre-bindings (make-subst-mod-params-bindings thname (formals-sans-usings source-theory) (actuals thname) (extended-mappings thname interpreted-theory source-theory) nil))) (acons decl rhs (append (mapcar #'(lambda (x) (let ((interp (assq (car x) (mapping interpreted-theory)))) (if interp (cons (cdr interp) (cdr x)) x))) pre-bindings) bindings)))) (defmethod subst-mod-params* :around (obj modinst bindings) (declare (type hash-table *subst-mod-params-cache*)) (or (gethash obj *subst-mod-params-eq-cache*) (let ((hobj (gethash obj *subst-mod-params-cache*))) (or hobj (let ((nobj (if (and (null (mappings modinst)) (not (some #'(lambda (b) (formal-theory-decl? (car b))) bindings)) (no-matching-free-params obj *subst-mod-free-params*)) obj (call-next-method)))) (when (and (typep obj 'type-expr) (typep nobj 'type-expr)) (when (print-type obj) (let ((pte (subst-mod-params* (print-type obj) modinst bindings))) (setq nobj (lcopy nobj 'print-type pte)))) (when (from-conversion obj) (let ((fconv (subst-mod-params* (from-conversion obj) modinst bindings))) (setq nobj (lcopy nobj 'from-conversion fconv))))) (if (and (null (freevars nobj)) (relatively-fully-instantiated? nobj)) (setf (gethash obj *subst-mod-params-cache*) nobj) (setf (gethash obj *subst-mod-params-eq-cache*) nobj)) #+pvsdebug (assert (every #'(lambda (fv) (or (binding? fv) (member fv (freevars obj) :test #'same-declaration) (member fv (freevars modinst) :test #'same-declaration))) (freevars nobj))) nobj))))) (defun no-matching-free-params (obj frees) (not (some #'(lambda (b) (memq b frees)) (free-params obj)))) (defun relatively-fully-instantiated? (obj &optional (freeparms *subst-mod-free-params*)) (let ((frees (set-difference (free-params obj) freeparms))) (or (null frees) (let ((formals (formals-sans-usings (current-theory)))) (every #'(lambda (fp) (memq fp formals)) frees))))) (defun update-current-context (theory theoryname) (assert (saved-context theory)) (update-known-subtypes theory theoryname) (update-judgements-of-current-context theory theoryname) (update-conversions-of-current-context theory theoryname) (update-auto-rewrites-of-current-context theory theoryname) (update-named-theories-of-current-context theory theoryname)) (defun update-named-theories-of-current-context (theory theoryname) (when (saved-context theory) (dolist (nt (named-theories (saved-context theory))) (pushnew nt (named-theories *current-context*))))) (defmethod generate-xref ((a mapping-rhs)) (if (type-value a) (generate-xref (type-value a)) (if (and (name-expr? (expr a)) (typep (declaration (expr a)) '(or module mod-decl formal-theory-decl))) (generate-xref (car (resolutions (expr a)))) (generate-xref (expr a)))))

**References**:**[Reposting again] Re: [Repost] Instantiating multiple theoriessimultaneously***From:*Michael Hohmuth <hohmuth@inf.tu-dresden.de>

- Prev by Date:
**[Reposting again] Re: [Repost] Instantiating multiple theoriessimultaneously** - Next by Date:
**recursive type** - Prev by thread:
**[Reposting again] Re: [Repost] Instantiating multiple theoriessimultaneously** - Next by thread:
**Re: strange problem with EG operator (fwd)** - Index(es):