module Data.Nat where

import Data.Int as Int
import Prelude

class IsNat (n :: Nat) where
  reflectNat :: proxy n -> Int

instance isNatMagic :: IsNat <magic> where
  reflectNat = <magic>

foreign import data Add :: Nat -> Nat -> Nat
foreign import data Sub :: Nat -> Nat -> Nat
foreign import data Mul :: Nat -> Nat -> Nat
foreign import data Div :: Nat -> Nat -> Nat
foreign import data Pow :: Nat -> Nat -> Nat

instance isNatAdd :: (IsNat a, IsNat b) => IsNat (Add a b) where
  reflectNat _ = reflectNat @a + reflectNat @b

instance isNatSub :: (IsNat a, IsNat b) => IsNat (Sub a b) where
  reflectNat _ = clamp 0 top $ reflectNat @a - reflectNat @b

instance isNatMul :: (IsNat a, IsNat b) => IsNat (Mul a b) where
  reflectNat _ = reflectNat @a * reflectNat @b

instance isNatDiv :: (IsNat a, IsNat b) => IsNat (Div a b) where
  reflectNat _ = reflectNat @a / reflectNat @b

instance isNatPow :: (IsNat a, IsNat b) => IsNat (Pow a b) where
  reflectNat _ = Int.pow (reflectNat @a) (reflectNat @b)

infixl 6 type Add as +
infixl 6 type Sub as -
infixl 7 type Mul as *
infixl 7 type Div as /

module Data.Vect
  ( Vect
  , empty
  , cons
  , uncons
  , append
  ) where

newtype Vect (n :: Nat) a = Vect (List a)

empty :: forall a. Vect 0 a
empty = Vect Nil

cons :: forall a n. a -> Vect n a -> Vect (n + 1) a
cons a (Vect b) = Vect (a : b)

uncons :: forall a n. Vect (n + 1) a -> {head :: a, tail :: Vect n a}
uncons (Vect a) =
  let {head, tail} = unsafePartial fromJust $ List.uncons a
  in {head, tail: Vect tail}

append :: forall a n m. Vect n a -> Vect m a -> Vect (n + m) a
append (Vect a) (Vect b) = Vect (a <> b)