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

problems with writing strategies for PVS



Dear PVS experts,

I ran into some trouble while writing strategies for PVS. I really appreciate
if someone can give me a solution to this problem.

I would like to have a strategy which filters all the conditional statements
from the sequent formulas. On these statements I would like to apply
a function.

Below, I have written the most crucial part of the strategy. 

    (let ((sforms (gather-seq (s-forms (current-goal *ps*))
                              '*
                              nil
                              PRED1))
          (fnums (gather-fnums sforms
                               '*
                               nil
                               PRED2)))
      (.....))


PRED1 should be read as 

    #'(lambda (sf) (or (branch? (formula sf))
                       (and (negation? (formula sf))
                            (branch? (args1 (formula sf)))))

(or something like that)

After having extracted the conditional statements, I would like to apply
a function on the THEN and ELSE part. I can extract the conditional
expression and the THEN part with (args1 (formula sf)) and 
(args2 (formula sf)), respectively, but I didn't manage the extract the ELSE
part. I hope that one of you can help me!

My second question is: is it feasible (and if so, how?) to evaluate the
expressions which are written in the THEN and ELSE part? More specifically,
can I recognise the boolean values TRUE and FALSE (easily)? I have searched
for recognisers for them, but I couldn't find any. Any suggestion is very
welcome!


Yours sincerely,
Joachim van den Berg

--
________________________________________________________________________
  Joachim van den Berg______________________________tel. +31 24 36 52710
  Computer Science Institute____________________mailto:joachim@cs.kun.nl
  University of Nijmegen_____________http://www.cs.kun.nl/~joachim/LOOP/