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

Re: types in strategies



Hanne,

You should never use the print-type in strategies; it is used
strictly for printing.  It is, as you noted, not always set.  This
is because the prettyprinter (which is the only code that is
expected to use the print-type) prints the print-type if it is
there, and otherwise just does it's normal processing.  Thus rat
is actually
  {x: {x: number | real_pred(x)} | rational_pred(x)} but its
print-type is the type-name rat.  The type rational is the same,
but with print-type rational.  This is one of the reasons not to
use the print-type; there may be many names for the same type.

I believe your strategy would work simply by removing the call to
print-type, as the format macro uses the print-object methods
which have been defined to prettyprint on type expressions.  In
fact, print-object has also been defined on actuals, so I would
probably use something like

(defstep cts () 
  (THEN (GRIND :DEFS NIL)(shuffle-forms)
 (let ((fmla (formula (car (p-sforms (current-goal *ps*))))))
    (if (and (application? fmla)
               (eq (id (operator fmla)) '|continuous|))
          (let ((act (car (actuals (module-instance (resolution (operator fmla)))))))
  (let ((transc_cont (format nil "transc_cont[~a]" act))
        (continuous (format nil "continuous[~a]" act))
	(GRIND$ :DEFS NIL :THEORIES
		(transc_cont "trig_types" "aux") :EXCLUDE
				     (continuous))))
(skip-msg "cts only useful on top level op of continuous"))))
"" 
"")

If this doesn't work let me know.

Sam

P.S. I notice other potential problems with this strategy.  First,
it assumes the operator of an application is a name-expr.  Thus it
would break on something like F(x)(2), which is an application
with operator F(x), which has no id.  The fix for this is simple;
just check that the operator is a name-expr.

The second potential problem is that it assumes there is only one
operator named continuous.  PVS allows overloading, and the user
may define his own function with that name, but that takes a
different set of parameters.  You can deal with this by checking
that it is from the right theory:
 (and (application? fmla)
      (name-expr? (operator fmla))
      (eq (id (operator fmla)) '|continuous|)
      (eq (id (module-instance (resolution (operator fmla))))
          '|continuous_functions|))