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

*To*: PVS-help <pvs-help@csl.sri.com>*Subject*: types in strategies*From*: Hanne Gottliebsen <hago@dcs.st-and.ac.uk>*Date*: Fri, 16 Feb 2001 15:35:29 +0000 (GMT)*Sender*: pvs-help-owner@csl.sri.com

I've got a problem with working out the actual parameters for some theories in a strategy. It work fine for types that are defined and given names outside the lemma I'm working on, but I would like to be able to use it without having to name the types. The problem seem to be that something like real as a print-type whereas something like {z:real|z/=1} doesn't. For the latter the print-type returns NIL, which I suspect is the cause of my problems. Here is (part of) my strategy: (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 (format nil "~a" (print-type (type-value (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")))) "" "") When running this on test_maple : LEMMA FORALL (x:{z:real| z /=1}) : continuous[{z:real| z /=1}](lambda (y:{z:real| z /=1}) : 1/(y-1),x) I get the error Actual does not resolve Whereas if I run the commands interactively (with the correct actuals) it works fine. Is the problem what I think it is, do I need to name the types or can I change my strategy to fit this situation too? I don't particularly want to make the strategy too hairy in the process, though. Thanks, Hanne --------------------------------------------------------- Hanne Gottliebsen Office P337 Dept. of Computer Science Ph: +44 1334 46 3265 University of St Andrews hago@dcs.st-and.ac.uk - I want a single-skin cotton tent like Mr Weasley's ---------------------------------------------------------

- Prev by Date:
**Re: Defining new infix operators** - Next by Date:
**Problems** - Prev by thread:
**Re: Problems** - Next by thread:
**Re: types in strategies** - Index(es):