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

Lists in strategies - without brackets?

Tamarah Arons writes:

 > I have a strategy defined with the following parameters:
 > (defstep split-rho-all (&optional (values nil)(split-up 1)(inst-into -)
 > (force? f) (remove-impl? t)(no-sub? f)(split-all -)(hide? t))
 > The first parameter, values, is a list of values, e.g. 
 > ("i!1" "j!1" "z") etc. The other parameters are seldom used.
 > However, users often omit the brackets over the values e.g.
 >  (split-rho-all "i!1" "j!1") instead of
 >  (split-rho-all ("i!1" "j!1")) 
 > which results in a segmentation fault:

Obviously, a seg fault shouldn't happen here.  There's a PVS or Lisp
bug somewhere.  If you're just looking for a work-around, probably the
easiest thing to do is add some error checking to your strategy to
detect this case and deduce the intended argument list.

 > Is there any way to make PVS see that "j!1" is part of the values list?
 > The other parameters are always preceded by the formal name (i.e.
 > :split-up) when used, and I am willing that they always must be.
 > Even willing to exclude them from the strategy if necessary.
 > I.e. is there any way to allow (split-rho-all "i!1" "j!1")
 > to be interpreted with values as ("i!1" "j!1")?
 > Or, even better, to allow the user to type 
 > (split-rho-all "i!1" "j!1" :hide? f) and still bind values as ("i!1"
 > "j!1")?
 > Some inbuilt strategies allow lists to be given with or without brackets 
 > (e.g. hide). How can I do this?

I doubt that you can do what you want directly because it's
inconsistent with the semantics of Common Lisp and the prover's rule
interface.  It sounds like what you want is to have a &rest argument
that can appear first in an argument list, followed by optional
keyword arguments.  This is a reasonable request, but not accommodated
by the current conventions.

If you're willing to do a little Lisp programming, however, you can
extend the conventions and parse your own arg lists.  You could
declare a strategy with a single &rest arg:

    (defstep split-rho-all (&rest args) ... )

then scan the arg list for the end of the "values" portion by looking
for keyword args (symbols beginning with a colon).  Unfortunately,
this still won't allow you to enter:

   (split-rho-all "i!1" "j!1" :hide? f)

because Lisp (or PVS) protests, calling ":hide?" an invalid keyword.

If you're willing to introduce a variant convention, however, you can
make it work.  Consider this alternative input form:

   (split-rho-all "i!1" "j!1" => hide? f)

Here "=>" is used as a delimiter (any valid symbol will do) to mark
the end of the "values" list.  The remainder will be keyword-value
pairs with colons stripped off the keywords.

Here's a crude implementation to experiment with:

(defun group-into-alist (pairs)
  (if (consp pairs)
      (cons (list (car pairs) (cadr pairs)) (group-into-alist (cddr pairs)))

(defstep split-rho-all (&rest args)
  (let ((key-args-init
	 '((split-up 1) (inst-into -) (force? f) (remove-impl? t)
	   (no-sub? f) (split-all -) (hide? t)))
	(pos (position-if #'(lambda (x) (eq x '=>)) args))
	(opt-pos (or pos (length args)))
	(values (subseq args 0 opt-pos))
	(key-args (subseq args (1+ opt-pos)))
	(a-list (append (group-into-alist key-args) key-args-init))
	(msg1 (format nil "Values: ~A" values))
	(msg2 (format nil "Split-up: ~A~%Hide?: ~A"
		      (cadr (assoc 'split-up a-list))
		      (cadr (assoc 'hide? a-list)))))
    (then (skip-msg msg1) (skip-msg msg2)))
  "Split rho ..."
  "~%Splitting rho ...")

I realize this solution is not entirely satisfactory.  Its main
drawback is the nonstandard notation.  It might cause users more
problems than the original.  But at least this approach, or another
like it, provides an easy extension mechanism.

    Ben Di Vito                     b.l.divito@larc.nasa.gov
    1 South Wright Street, MS 130   http://shemesh.larc.nasa.gov/~bld
    NASA Langley Research Center    voice: +1-757-864-4883
    Hampton, VA 23681   USA         fax:   +1-757-864-4234