module test

import qualified StdEnv
import StdEnv => qualified isEven, isOdd, class toInt(..), instance toInt Int, class toString(..)

:: Zero = Zero
:: Succ a = Succ
:: One :== Succ Zero
One :: One
One = undef
:: Two :== Succ (Succ Zero)
Two :: Two
Two = undef
:: Three :== Succ (Succ (Succ Zero))
Three :: Three
Three = undef
:: True = Tr
:: False = Fs

class Even a ~c
where
	isEven :: a -> c
	isEven _ = undef
class Odd a ~c
where
	isOdd :: a -> c
	isOdd _ = undef
instance Even Zero True
instance Odd Zero False
instance Even (Succ a) b | Odd a b
instance Odd (Succ a) b | Even a b

dec :: (Succ a) -> a
dec _ = undef

class Add a b ~c
where
	(:+:) infixl 6  :: a b -> c
	(:+:) _ _ = undef
instance Add Zero b b
instance Add (Succ a) b (Succ c) | Add a b c

class Mult a b ~c
where
	(:*:) infixl 7 :: a b -> c
	(:*:) _ _ = undef
instance Mult Zero b Zero
instance Mult (Succ a) b d | Mult a b c & Add b c d

class Pow a b ~c
where
	(:^:) infixr 8 :: a b -> c
	(:^:) _ _ = undef
instance Pow a Zero One
instance Pow a (Succ b) d | Pow a b c & Mult a c d

instance +++ {!a}
where
	(+++) l r =
		{  'StdEnv'._createArray (size l+size r)
		&  [i]=l.[i], [size l+j]=r.[j]
		\\ i<-[0..size l-1] & j <- [0..size r-1]
		}

:: Vec n a = Vec {!a}

empty :: Vec Zero a
empty = Vec {}

single :: a -> Vec (Succ Zero) a
single a = Vec {a}

length :: (Vec n a) -> n
length _ = undef

nrepeat :: n a -> Vec n a | toInt n
nrepeat _ a = repeat a

repeat :: a -> Vec n a | toInt n
repeat a = let r = Vec (createArray (toInt (length r)) a) in r

append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
append (Vec a) (Vec b) = Vec (a +++ b)

<<<<<<< HEAD
//Start = nrepeat (Three :*: Three) 'a'

v1 :: Vec (Succ (Succ Zero)) Int
v1 = append (single 1) (single 32)

v2 :: Vec Three Int
v2 = repeat 5

=======
>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
class Le a b ~c
where
	le :: a b -> c
	le _ _ = undef
instance Le Zero b True
instance Le (Succ a) Zero False
instance Le (Succ a) (Succ b) c | Le a b c

//Because toInt from StdEnv is strict in the first argument
class toInt a :: a -> Int
instance toInt Int where toInt i = i
instance toInt Zero where toInt _ = 0
instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))

(!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
(!!) (Vec a) i = a.[toInt i]

(=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
(=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}

:: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
:: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
:: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
<<<<<<< HEAD
:: Y = Y; :: Z = Z; :: Spc = Spc
:: Nl = Nl
:: SC l r = SC

:: Cons x xs = Cons
class HConcat a b ~c
where
	hconcat :: a b -> c
	hconcat _ _ = undef
instance HConcat () a a
instance HConcat (Cons x xs) ys (Cons x zs) | HConcat xs ys zs

:: FooS :== Cons F (Cons O (Cons O ()))
FooS :: FooS
FooS = undef
:: BarS :== Cons B (Cons A (Cons A ()))
BarS :: BarS
BarS = undef

:: NilS :== ()
NilS :: NilS
NilS = undef
=======
:: Y = Y; :: Z = Z;
:: Nul = Nul
:: SC l r = SC

Start = nrepeat (Three :*: Three) 'a'

e1 :: Vec (Succ (Succ Zero)) Int
e1 = append (single 1) (single 32)

e2 :: Vec Three Int
e2 = repeat 5
>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f