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

[PVS-Help] Reading PVS AST


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,

 (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.

Aditya Kanade.
Ph.D. student, CSE, IIT Bombay.