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

parameters in new strategies



I am trying to work out how to write new strategies. I have with me the
prover-guide and the "less elementary introduction", are there anything
that gives more examples/explanation of new strategies?

I have the following strategy:

(defstep simple-cts ( )
	(GRIND :DEFS NIL :THEORIES
   ("lambda_abstractions[real]" "continuous_functions[real]") :EXCLUDE
   ("continuous[real]" "continuity_def[real]"))
	"cts for fcts with domain real"
	"By theorems in continuous_functions")

which applied works fine.

I would like to give as a parameter to this strategy the parameter to be
used in the theories. Eg:

(defstep simple-cts2 (&optional fctdomain)
	(GRIND :DEFS NIL :THEORIES
   ("lambda_abstractions[fctdomain]" "continuous_functions[fctdomain]")
:EXCLUDE
   ("continuous[fctdomain]" "continuity_def[fctdomain]"))
	"cts for fcts with domain fctdomain"
	"By theorems in continuous_functions")

But this does not work at all:

test2 :  

  |-------
{1}   FORALL (a, y: real): continuous(LAMBDA x: a + x, y)

Rule? (simple-cts2 :fctdomain "real")
Actual does not resolve
Restoring the state.
test2 :  

  |-------
{1}   FORALL (a, y: real): continuous(LAMBDA x: a + x, y)

And I don't really want it as an optional parameter, but a required one
anyway.

Or is it that I should not expect PVS to handle theory-parameters as
arguments to strategies?


Thanks,
Hanne Gottliebsen
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
                   - Who moved the stone?
---------------------------------------------------------