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

Re: [PVS-Help] typecheck in lisp code


It is possible to do what you want, here you can see the basic interaction
in the *pvs* buffer.  Notice that when I did the typecheck first, it gave
a parse error, as the end of a theory (test1 in this case) requires the
theory id.  After fixing this, everything works as expected.

Let me know if you have further questions.

pvs(15): (typecheck-file "mfiles")
Parsing mfiles
There is garbage at the end of your file or string:
Line 6:     test2: THEORY

In file mfiles (line 6, col 5)
Error: Parse error

Restart actions (select using :continue):
 0: Return to Top Level (an "abort" restart).
 1: Abort entirely from this (lisp) process.
[1] pvs(22): :pop
pvs(23): (typecheck-file "mfiles")
Parsing mfiles
mfiles parsed in 0.00 seconds
Typechecking mfiles
test1 typechecked in 0.00s: No TCCs generated
test2 typechecked in 0.00s: No TCCs generated
(#<Theory test1> #<Theory test2>)
pvs(24): (get-typechecked-theory "test1")
#<Theory test1>
pvs(25): (get-typechecked-theory "test2")
#<Theory test2>

masoome parsa <masoome.parsa@xxxxxxxxx> wrote:

> 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
> test2: THEORY
> 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)