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

types in strategies

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))
		(transc_cont "trig_types" "aux") :EXCLUDE
(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.

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