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

"<<" TCC ?



Hello,

I want to define an abstract data type and some operations with it.
After typecheckeing I've got TCC which is unprovable. Could you hint  
me: what do I wrong ? 

thanks in advance, Sergey

My type is: 

gen_tree[T: TYPE]: DATATYPE
BEGIN

IMPORTING list
leaf(fringe: list[T]): isLeaf?
node(val: T, desc: list[gen_tree]): isNode?

END gen_tree

Then I define function size in the next way;

sum(ls: list[nat]): RECURSIVE nat =
CASES ls OF
	null: 0,
	cons(x, ls1): x + sum(ls1)
ENDCASES
MEASURE ls BY <<

%size function
size(tr): RECURSIVE nat = 
CASEs tr OF  
	leaf(tr): length(tr),
	node(val,desc): 1 + sum(map(size ,desc))
ENDCASES
MEASURE tr BY <<