[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: TYPE functions
The grammar doesn't currently allow infix operators for type constructors,
but I'll look into adding this feature, as I'm currently updating the
Type definitions with type parameters are a little more difficult.
We would like to add type variables, but it must be done carefully to
ensure that the type system is sound. Shankar and I are just starting to
design this, but it will probably be awhile before it will be available in
Finally, the documentation definitely needs to be updated; right now the
best I can do is point to the ftp://ftp.csl.sri.com/pub/pvs2.1/CHANGES and
to some of the papers mentioned in http://csl.sri.com/pvs.html. If you
have specific questions, I would be happy to try and answer them.
> I recently discovered (I don't remember where or how!) that I could add
> parameters to a TYPE definition. In other words I can write a "function"
> whose result is a type. For instance, the following type definition
> works fine:
> starstar(A, B: setof[T]): TYPE
> = [(A) -> list[(B)]] ;
> However, if I replace "starstar" with infix operator "**", although the
> definition works, the "**" does not seem available as a type
> constructor. This may be a bug with "infix" syntax handling.
> I also tried the following definition, which unfortunately does not
> starstar(A, B: TYPE): TYPE
> = [A -> list[B]] ;
> Is there a deep reason for disallowing this? To me, it just looks
> equivalent to the less flexible style:
> whatever[A, B: TYPE]: THEORY
> starstar: TYPE = [A -> list[B]] ;
> END whatever
> Detail of my questions are included in the attached PVS dump, which I
> also send as a bug report.
> My PVS documentation is not up to date: please give me pointers to the
> most recent documents available.
> Thanks a lot,