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

Re: TYPE functions



Hi Paul,

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
grammar anyway.

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
PVS.

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.

Sam

> Hi!
> 
> 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
> work:
> 
>     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
>       BEGIN
>          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,
> -- 
>     pyg