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

Declaring a list of expressions in a .pvs file



Hello,

I have a strategy which at some point generates a number of
goals, each having a consequent of the form 

 EXISTS (e: SOME_DOMAIN):
        (e = expr_1 OR
          e = expr_2 OR 
           e = expr_3 OR ... )
         AND some_function(e)

When there is only one OR in the expression, then PVS manages to 
discharge the goal automatically.
However, when there are 2 or more ORs, I instantiate the statement
manually (inst-cp for every expr_i).

The list of exprs that can occur is quite small, and I can pass it as a 
parameter to the strategy as (``expr1'' ``expr2'' ``expr3'' ... ) and 
then the instantiation can be automated too.
However, I'd like to go a step further and have the user declare a named
list of expressions (each written as a string) in the .pvs file. 
The expressions are typically records, e.g. "(# a := 3, b := Z #)",
so I want to declare the list
mylist = ( "(# a := 3, b := Z #)" "(# a := 8, b := Y #)" "(# a := 5, b := Y #)")

The strategy would then use mylist. (In fact, the list can be generated
from other definitions in the .pvs file, and ideally this may be done by
some compiler).

Is there anyway to do this?

Thanks,
Tamarah