-- This is written in Haskell.
module MarkerType where
	{
	data Singleton a = Singleton;

	instance Show (Singleton a) where
		{
		show Singleton = "singleton";
		};

	-- Booleans expressed as Haskell types.
	data True;
	data False;
	
	class BooleanType a;
	instance BooleanType True;
	instance BooleanType False;

	class Is a;
	instance Is True;

	class Isnt a;
	instance Isnt False;

	class EitherIs a b;
	instance EitherIs True b;
	instance EitherIs False True;

	class BothAre a b;
	instance BothAre True True;
	
	class Not a b | a -> b;
	instance Not True False;
	instance Not False True;
	
	class Or a b c | a b -> c;
	instance Or True b True;
	instance Or False b b;
	
	class And a b c | a b -> c;
	instance And True b b;
	instance And False b False;

	class Pick which t f r | which t f -> r;
	instance Pick True  t f t;
	instance Pick False t f f;

	{--
	Integers expressed as Haskell types. Zero is 0.
	If type a is Zero or positive, then (Succ a) is positive;
	if type a is Zero or negative, then (Pred a) is negative.
	This is very crude and should be replaced with sign-magnitude 
	representation.
	--}

	data Zero;
	data Succ n;
	data Pred n;

	class NaturalType a;
	instance NaturalType Zero;
	instance NaturalType (Succ a);

	class IntegerType a;
	instance IntegerType Zero;
	instance IntegerType (Succ a);
	instance IntegerType (Pred a);

	type One	= Succ Zero;
	type Two	= Succ One;
	type Three	= Succ Two;
	type Four	= Succ Three;
	type Five	= Succ Four;
	type Six	= Succ Five;
	type Seven	= Succ Six;
	type Eight	= Succ Seven;
	type Nine	= Succ Eight;
	type Ten	= Succ Nine;
	type MinusOne = Pred Zero;
	type MinusTwo = Pred MinusOne;
	type MinusThree = Pred MinusTwo;

	class Successor a b | a -> b;
	instance Successor Zero One;
	instance Successor (Succ a) (Succ (Succ a));
	instance Successor (Pred a) a;

	class Predecessor a b | a -> b;
	instance Predecessor Zero MinusOne;
	instance Predecessor (Succ a) a;
	instance Predecessor (Pred a) (Pred (Pred a));

	class IsAtLeast a b c | a b -> c; -- c == (a >= b)
	instance IsAtLeast Zero Zero True;

	instance IsAtLeast Zero (Pred b) True;
	instance IsAtLeast Zero (Succ b) False;

	instance IsAtLeast (Succ a) Zero True;
	instance IsAtLeast (Pred a) Zero False;

	instance IsAtLeast (Succ a) (Pred b) True;
	instance IsAtLeast (Pred a) (Succ b) False;

	instance (IsAtLeast a b c) => IsAtLeast (Succ a) (Succ b) c;
	instance (IsAtLeast a b c) => IsAtLeast (Pred a) (Pred b) c;

	class IsEven a e | a -> e;
	instance IsEven Zero True;
	instance (IsEven a e,Not e ne) => IsEven (Succ a) ne;
	instance (IsEven a e,Not e ne) => IsEven (Pred a) ne;

	class AtLeast a b; -- a >= b
	instance (IsAtLeast a b True) => AtLeast a b;

	class AtLeastOne a;
	instance (NaturalType a) => AtLeastOne (Succ a);

	-- Integer addition. Both operands are either positive, negative
	-- or zero, so we consider 3*3=9 cases.
	class Add a b c | a b -> c;

	instance Add Zero Zero Zero;

	instance Add Zero (Succ b) (Succ b);
	instance Add Zero (Pred b) (Pred b);

	instance Add (Succ b) Zero (Succ b);
	instance Add (Pred b) Zero (Pred b);

	instance Add a b c => Add (Succ a) (Succ b) (Succ (Succ c));
	instance Add a b c => Add (Pred a) (Pred b) (Pred (Pred c));

	instance Add a b c => Add (Succ a) (Pred b) c;
	instance Add a b c => Add (Pred a) (Succ b) c;

	class Negate a b | a -> b;
	instance Negate Zero Zero;
	instance (Negate a b) => Negate (Succ a) (Pred b);
	instance (Negate a b) => Negate (Pred a) (Succ b);

	class Sub a b c | a b -> c;

	instance Sub Zero Zero Zero;

	instance Negate b c => Sub Zero (Succ b) (Pred c);
	instance Negate b c => Sub Zero (Pred b) (Succ c);

	instance Sub (Succ b) Zero (Succ b);
	instance Sub (Pred b) Zero (Pred b);

	instance Sub a b c => Sub (Succ a) (Succ b) c;
	instance Sub a b c => Sub (Pred a) (Pred b) c;

	instance Sub a b c => Sub (Succ a) (Pred b) (Succ (Succ c));
	instance Sub a b c => Sub (Pred a) (Succ b) (Pred (Pred c));

	class Abs a b | a -> b;
	instance Abs Zero Zero;
	instance Abs (Succ a) (Succ a);
	instance (Abs a b) => Abs (Pred a) (Succ b);

	class GCD a b gcd | a b -> gcd;
	instance GCD Zero b b;
	instance GCD (Succ a) Zero (Succ a);
	instance
		(
		Sub a b amb,
		Abs amb diff,
		IsAtLeast Zero amb abigger,
		Pick abigger b a smaller,
		GCD (Succ smaller) diff gcd
		)
		=> GCD (Succ a) (Succ b) gcd;

	-- only instances for a mod b == 0
	class Divide a b c | a b -> c;
	instance
		(
		Negate a na,
		Negate b nb,
		Divide na (Succ nb) c
		)
		=> Divide a (Pred b) c;
	instance Divide Zero (Succ b) Zero;
	instance
		(
		Sub a b amb,
		Divide amb (Succ b) c
		)
		=> Divide (Succ a) (Succ b) (Succ c);
	instance
		(
		Add a b apb,
		Divide apb (Succ b) c
		)
		=> Divide (Pred a) (Succ b) (Pred c);
	
	data RationalType num denom;
	
	class MakeRational n d r | n d -> r;
	instance
		(
		GCD n d gcd,
		Divide n gcd num,
		Divide d gcd denom
		)
		=> MakeRational n d (RationalType num denom);
	}