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

[PVS-Help] Reading PVS AST



Hi,

Is there a function to walk over PVS abstract syntax tree generated
after parsing and typechecking a specification? I want to generate
some files from PVS specifications (as I'd mentioned in an earlier query). 

Currently, I'm trying a bit adhoc method of exploring only relevent
parts of AST that I'm interested in but sometime I may need to look at
a whole AST. The pvs-send-and-wait function returns a string but as I
need to work on the objects generated in PVS, I'm installing (or
evaluating) my functions in PVS Lisp directly.

For example,

(pvs-send-and-wait 
 (format "(defun get-theory-from-file (file-name) 
\"Get the (first and only) theory object from the file.\"
(car (typecheck-file file-name)))"))
 
and I then use this function in another function which again I
delegate completely to PVS. The only functions that I handle in Elisp
are some higher level functions, file/buffer operations, etc.

I would like know whether this is how one should proceed or is there
any better way to do this. Please advise.

Regards,
Aditya Kanade.
Ph.D. student, CSE, IIT Bombay.
http://www.cse.iitb.ac.in/~aditya