[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

  atom : TYPE+

  term : DATATYPE
    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

  hydrogen, helium : atom

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

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

  trivial2 : THEOREM

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


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