--Arithmetic.d
--this package forms the base type for things that act like numbers
--must have assertions on behavior demanded for each operator

face Arithmetic
is

	type baseType is private		--baseType is the custom type supplied by implementing bodies
	function `+'(lhs:baseType, rhs:baseType) return baseType	--addition
		{ all x,y:baseType in true are x+y=y+x }
	function `-'(lhs:baseType, rhs:baseType) return baseType	--subtraction
		{ all x,y:baseType in true are ((x+y)-x=y) and (x-x=0) }
	function `*'(lhs:baseType, rhs:baseType) return baseType	--multiply
		{ all x,y,z:baseType in true are (x*y=y*x) and (z*(x+y)=(z*x)+(z*y)) }	
	function `/'(lhs:baseType, rhs:baseType) return baseType	--divide
		{ all x,y:baseType in true are ((x*y)/x=y) or (x=0)}	
	function `**'(lhs:baseType, rhs:baseType) return baseType		--exponentiate
		--ooh exponentiation and log are tough to be perspicuous.  Any ideas Dr. Ricther?
	variable zero:constant baseType		--define zero
		{ all x:baseType in true are (x*zero=zero) and (x+zero=x) }
	variable one:constant baseType		--define unity
		{ all x:baseType in true are x*one=x }

	function toString(bt:baseType) return string
	function toInteger(bt:baseType) return integer
	function toFloating(bt:baseType) return floating
	function toRational(bt:baseType) return rational
	function fromString(bt:string) return baseType
	function fromInteger(bt:integer) return baseType
	function fromFloating(bt:floating) return baseType
	function fromRational(bt:rational) return baseType

end face 	--of Arithmetic

--------------------------------------------------------------

body builtInInteger:Arithmetic
is
	type baseType is integer	--there exists a type integer
	function `+'(lhs:baseType, rhs:baseType) return baseType	--addition
		{ all x,y:integer in true are x+y=y+x }
		is begin skip end
	function `-'(lhs:baseType, rhs:baseType) return baseType	--subtraction
		{ all x,y:integer in true are ((x+y)-x=y) and (x-x=0) }
		is begin skip end
	function `*'(lhs:baseType, rhs:baseType) return baseType	--multiply
		{ all x,y,z:integer in true are (x*y=y*x) and (z*(x+y)=(z*x)+(z*y)) }	
		is begin skip end
	function `/'(lhs:baseType, rhs:baseType) return baseType	--divide
		{ all x,y:integer in true are ((x*y)/x=y) or (x=0)}	
		is begin skip end
	function `mod'(lhs:baseType, rhs:baseType) return baseType	--divide
		{ all x,y,z:integer in true are (x>=0) and (y>0) and (x mod y = x-(x/y)*y) }	
		is begin skip end
	function `**'(lhs:baseType, rhs:baseType) return baseType		--exponentiate
		is begin skip end
	variable zero:constant baseType:=0;		--define zero
		{ all x:integer in true are (x*zero=zero) and (x+zero=x) }
	variable one:constant baseType:=1;		--define unity
		{ all x:integer in true are x*one=x }

	function toString(bt:baseType) return string
		is begin skip end
	function toInteger(bt:baseType) return integer
		is begin skip end
	function toFloating(bt:baseType) return floating
		is begin skip end
	function toRational(bt:baseType) return rational
		is begin skip end
	function fromString(bt:string) return baseType
		is begin skip end
	function fromInteger(bt:integer) return baseType
		is begin skip end
	function fromFloating(bt:floating) return baseType
		is begin skip end
	function fromRational(bt:rational) return baseType
		is begin skip end
	
	function log2(r:baseType) return baseType
		is begin skip end
		
end body		--end of builtInInteger

body builtInFloating:Arithmetic
is
	type baseType is floating	--there exists a type floating
	function `+'(lhs:baseType, rhs:baseType) return baseType	--addition
		{ all x,y:floating in true are x+y=y+x }
		is begin skip end
	function `-'(lhs:baseType, rhs:baseType) return baseType	--subtraction
		{ all x,y:floating in true are ((x+y)-x=y) and (x-x=0) }
		is begin skip end
	function `*'(lhs:baseType, rhs:baseType) return baseType	--multiply
		{ all x,y,z:floating in true are (x*y=y*x) and (z*(x+y)=(z*x)+(z*y)) }	
		is begin skip end
	function `/'(lhs:baseType, rhs:baseType) return baseType	--divide
		{ all x,y:baseType in true are ((x*y)/x=y) or (x=0)}	
		is begin skip end
	function `mod'(lhs:baseType, rhs:baseType) return baseType	--divide
		{ all x,y,z:baseType in true are (x>=0) and (y>0) and (x mod y = x-(x/y)*y) }	
		is begin skip end
	function `**'(lhs:baseType, rhs:baseType) return baseType		--exponentiate
		is begin skip end
	variable zero:constant baseType:=0;		--define zero
		{ all x:floating in true are (x*zero=zero) and (x+zero=x) }
	variable one:constant baseType:=1;		--define unity
		{ all x:floating in true are x*one=x }

	function toString(bt:baseType) return string
		is begin skip end
	function toInteger(bt:baseType) return integer
		is begin skip end
	function toFloating(bt:baseType) return floating
		is begin skip end
	function toRational(bt:baseType) return rational
		is begin skip end
	function fromString(bt:string) return baseType
		is begin skip end
	function fromInteger(bt:integer) return baseType
		is begin skip end
	function fromFloating(bt:floating) return baseType
		is begin skip end
	function fromRational(bt:rational) return baseType
		is begin skip end
end body		--end of builtInFloating