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

*To*: PVS Help <pvs-help@csl.sri.com>*Subject*: TYPE functions*From*: Paul Y GLOESS <gloess@labri.u-bordeaux.fr>*Date*: Wed, 01 Apr 1998 16:47:35 +0200*CC*: PVS Bugs <pvs-bugs@csl.sri.com>*Organization*: LaBRI & ENSERB*Sender*: gloess@labri.u-bordeaux.fr

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

%Patch files loaded: patch2 version 2.417 $$$typefun.pvs %%% %%% 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 BEGIN %% %% 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.prf (|typefun| (|using_starstar| "" (SKOSIMP) NIL))

- Prev by Date:
**Re: pvs error** - Next by Date:
**pvs error** - Prev by thread:
**Re: typecheck error** - Next by thread:
**Re: TYPE functions** - Index(es):