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

[PVS-Help] typecheck in lisp code



Hi,

Is it possible to use typecheck for 2 theories in the same pvs file in a lisp code ?
Here I have 2 theories in the pvs file :
test1: THEORY
BEGIN

END

test2: THEORY
BEGIN

END

and in my lisp code I have

        (typecheck-file pvsfile ...)

and

 (let* ((theory (get-typechecked-theory pvs_name))
       (*current-theory* theory)
       (*generate-tccs* (if nil 'all 'none))
       (*current-context* (or (saved-context theory)
                              (context nil)))
       (*suppress-msg* t)
       (*in-evaluator* t)
       (*destructive?* t)
       (*eval-verbose* nil)
       (*compile-verbose* nil)
       (*convert-back-to-pvs* nil)))

I wanted to know if I can use the above code first for theory test1 and then for theory test2 which are both in the same pvs file !?
I tried it but I got this error : can't find file for theory test2. (It gives the error for the second typecheck)