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

TYPE functions


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,
%Patch files loaded: patch2 version 2.417

%%% Author: Paul Y Gloess, e-mail: gloess@labri.u-bordeaux.fr
%%%         LaBRI, ENSERB & Universite Bordeaux I
%%%         351, Cours de la Liberation
%%%         33405  Talence Cedex
%%%         France
%%%   Date: 1 April 1998
%%% Three question to pvs-help@csl.sri.com and pvs-bugs@csl.sri.com
%%%  about TYPE definitions:
%%% 1) The first "starstar" type definition works fine and can effectively
%%%     be used as in "using_starstar" lemma: is this documented PVS syntax?
%%%     I could not find out in my documentation [actually I don't remember
%%%     how or where I got this idea!]. Could you please give me
%%%     pointers to up to date (most recent) PVS documentation?
%%% 2) The first "**" definition (equivalent to "starstar") works fine but
%%%     I cannot use it: the commented out lemmas "using_starstar2" or
%%%     "using_starstar3" do not parse correctly. Is this a bug related to
%%%     "infix" syntax?
%%% 3) What I really wanted to write was:
%%%       starstar(A, B: TYPE): TYPE
%%%         = [A -> list[B]] ;
%%%     or likewise with "**" in lieu of "starstar". It does not parse
%%%     correctly. Is there a reason for not accepting this kind of definition
%%%     which I would find convenient?
typefun[T: TYPE]: THEORY


    %% This is a TYPE definition with parameters:
    %% [I don't remember how or where I found that I could write this!].
    starstar(A, B: setof[T]): TYPE
      = [(A) -> list[(B)]] ;

    %% This is just an example using the above notation:
    using_starstar: LEMMA
      (FORALL (X, Y: setof[T], f: starstar(X, Y)):
         f = f) ;

    %% Note that if one uses ** infix binary operator instead of starstar,
    %%  the parser accepts the type definition, but not the lemma.
    **(A, B: setof[T]): TYPE
      = [(A) -> list[(B)]] ;

    %%  using_starstar2: LEMMA     % does not parse correctly.
    %%    (FORALL (X, Y: setof[T], f: (X ** Y)):
    %%       f = f) ;

    %%  using_starstar3: LEMMA     % does not parse correctly either.
    %%    (FORALL (X, Y: setof[T], f: X ** Y):
    %%       f = f) ;

    %% What I really wanted to do write (but it does not parse correctly!) was:
    %%   **(A, B: TYPE): TYPE
    %%     = [A -> list[B]] ;
    %%    or even
    %%   starstar(A, B: TYPE): TYPE
    %%     = [A -> list[B]] ;
  END typefun

(|typefun| (|using_starstar| "" (SKOSIMP) NIL))