-- vector.as 6.4.00 -- A type of Integer Vectors; Vector(n), given a recursive type -- definition. Also defines constructors, print function, addition and -- vector append. Uses pretend heavily to reassure the type checker. -- The programs don't just type check but actually work too! #include "axllib" import from Integer; -- to use Integer -- In order to push these definitions through the type checker, we -- have to use pretend in two different ways: -- A: pretend is used to force elements from the two -- possible types (Integer and Record) to Vector(n) -- B: it is used to make up for the fact that there is no -- evaluation in the type checking mechanism of Aldor. -- These pretends can be inserted according to the error -- messages produced by the compiler when the undecorated -- program fails to compile. -- In the body of the programs these are illustrated by comments -- thus: -- A -- -- B -- The definition of Vectors of length n. Vector(n:Integer): Type == if n<=1 then Integer else Record(fst:Integer,rst:Vector(n-1)); -- Constructing a Vector(n) from an Integer and a Vector(n-1). -- In order to use the record constructors at the appropriate type -- they need explicitly to be imported at that type; since the type -- contains variables, the import can only take place when the -- variables are in scope. vCons(n:Integer,x:Integer,v:Vector(n-1)):Vector(n) == { import from Record(fst:Integer,rst:Vector(n-1)); [x,v]@Record(fst:Integer,rst:Vector(n-1)) pretend Vector(n); -- B }; -- Building vectors. -- Build the vector < f(0),f(1),...,f(n-1) > buildVec(n:Integer,f:Integer->Integer):Vector(n) == if n<=1 then f(0) pretend Vector(n) -- A else vCons(n,f(0),buildVec(n-1,next(f))); -- takes the integer f to \n.f(n+1) next(f:Integer->Integer):(Integer->Integer) == (n:Integer):Integer +-> f (n+1); -- Some example vectors. -- The constant zero vector < 0,0,...,0 > built using build. zeroVec(n:Integer):Vector(n) == buildVec(n,(n:Integer):Integer +-> 0); zVec(n:Integer):Vector(n) == if n<=1 then 0 pretend Vector(n) -- A else vCons(n,0,zVec(n-1)); -- The factorial function fac(n:Integer):Integer == if n<=0 then 1 else (n*fac(n-1)); -- A vector of factorials facVec(n:Integer):Vector(n) == buildVec(n,fac); -- Add up the entries of a Vector(n). addVec(n:Integer,v:Vector(n)):Integer == { import from Record(fst:Integer,rst:Vector(n-1)); if n<=1 then 0 else vec.fst + addVec(n-1,vec.rst); where { vec == (v pretend -- A Record(fst:Integer,rst:Vector(n-1))); }}; -- Append two Vectors. append(n:Integer,m:Integer,v:Vector(n),w:Vector(m)):Vector(n+m) == { if n<=0 then w pretend Vector(n+m) -- B else if n=1 then vCons(m+1, (v pretend Integer), -- A (w pretend Vector((m+1)-1))) -- B pretend Vector(n+m) else vCons(n+m, vec.fst, append(n-1,m,vec.rst,w) pretend Vector((n+m)-1)) -- B where { vec == (v pretend -- A Record(fst:Integer,rst:Vector(n-1))); }}; -- Print a Vector(n) with entries comma separated. printVec(tw:TextWriter,n:Integer,v:Vector(n)) : TextWriter == { import from Record(fst:Integer,rst:Vector(n-1)); if n<1 then tw else if n=1 then tw << (v pretend Integer) -- A else printVec((tw << vec.fst << ","),n-1,vec.rst) where { vec == (v pretend -- A Record(fst:Integer,rst:Vector(n-1))); }}; -- Testing the various functions: -- two variants of zero vector printVec(print,3,zeroVec(3)) << newline; printVec(print,3,zVec(3)) << newline; -- a factorial vector. printVec(print,6,facVec(6)) << newline; -- append: note it gives a Vector(6+3). printVec(print,6+3,append(6,3,facVec(6),zVec(3))) << newline; -- and adding two appended vectors. print << addVec(6+3,append(6,3,facVec(6),zVec(3))) << newline;