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

Re: Prolog & PVS




Pieter -

What you're probably looking for is a PVS datatype.  Try this one:

prolog: THEORY
BEGIN

  atom : TYPE+

  term : DATATYPE
  BEGIN
    simpleterm   (a : atom) : simpleterm?
    compoundterm (a : atom, ts : (cons?[term])) : compoundterm?
  END term
    
END prolog

'simpleterm' and 'compoundterm' are constructors that you can use to
generate things of type term from atoms and other terms.  'a' and 'ts' are
accessors, that are used to peek inside things of type term.
'simpleterm?'  and 'compoundterm?' are recognizers, used if you need to
determine which sort of term you're dealing with [They don't need to end
in '?' - that's just a convention we use to denote predicates].  For
example:


  hydrogen, helium : atom

  hterm : term = compoundterm(hydrogen,
                              cons[term](simpleterm(helium), null))

  trivial : THEOREM
    a(car(ts(hterm))) = helium

  trivial2 : THEOREM
    compoundterm?(hterm)


More detail on PVS datatypes can be found in the PVS language reference,
available from http://pvs.csl.sri.com/manuals.html

Dave

---
Dr Dave Stringer-Calvert,  Senior Project Manager,  Computer Science Lab
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com