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

Instantiating datatypes with subtype of nat



Hello all, I've stumbled across a problem using PVS to
instantiate an ADT with a subtype based on nat. This is 
PVS version 2.1 Test (PL 2.3999) on a regular SPARC.
My example file is this:

--------- SNIP
%
% A silly datatype with one single parameter.
%
fooT [t : TYPE] : DATATYPE
BEGIN
	f(m:t) : f?
	g : g?
END fooT

%
% I instantiate the theory with an enum type. This works.
%
foo  : THEORY
BEGIN
	enum : TYPE = {a00,b00,c00}
	IMPORTING fooT[enum]

	ffoo(n : fooT[enum]) : nat =
		CASES n OF
			f(mmm) : ord(mmm),
			g : 0
		ENDCASES
END foo


%
% Here's the problem. If I instantiate with a subtype
% of nat -- upto(5) or {n:nat | n=7 OR n=9} or something
% else, then the typechecker gives me:
%
% g does not uniquely resolve - one of:
%  fooT_adt[number].g : (g?[number]),
%  fooT_adt[enum].g : (g?[enum])
%
% I understand that the lifting-subtyping system creates
% the fooT_adt[number] type (p. 21 of the Datatype Tutorial),
% but then how do I disambiguate them in a CASES statement?
%
bar  : THEORY
BEGIN
	enum : TYPE = upto(5)
	IMPORTING fooT[enum]

	ffoo(n : fooT[enum]) : nat =
	CASES n OF
		f(mmm) : mmm,
		g : 0
	ENDCASES
END bar
--------- SNIP


In the same general area: if I make fooT a type like this:

fooT [t : TYPE, n : nat ] : DATATYPE

Then typechecking gives me this:

Error: No methods applicable for generic function 
#<STANDARD-GENERIC-FUNCTION MODULE-INSTANCE> with args (NIL) of classes (NULL)

What gives?





-- 
+-----------------------------------+-------------------+
+ My brother went to London and all + adridg@sci.kun.nl +
+ I got was this lousy .sig.        +     (Ade)         +