Nat.purs

module Data.Typelevel.Nat where

import Prelude

import Data.Symbol (SProxy(..))
import Prim.Symbol as Symbol

class IsNat nat where
  reflectNat :: SProxy nat -> Int

instance nat0 :: IsNat "0" where
  reflectNat _ = 0
else
instance nat1 :: IsNat "1" where
  reflectNat _ = 1
else
instance nat2 :: IsNat "2" where
  reflectNat _ = 2
else
instance nat3 :: IsNat "3" where
  reflectNat _ = 3
else
instance nat4 :: IsNat "4" where
  reflectNat _ = 4
else
instance nat5 :: IsNat "5" where
  reflectNat _ = 5
else
instance nat6 :: IsNat "6" where
  reflectNat _ = 6
else
instance nat7 :: IsNat "7" where
  reflectNat _ = 7
else
instance nat8 :: IsNat "8" where
  reflectNat _ = 8
else
instance nat9 :: IsNat "9" where
  reflectNat _ = 9
else
instance nat' ::
  ( Symbol.Cons head tail nat
  , NatConcat head tail
  ) => IsNat nat where
  reflectNat _ = reflectNat' (SProxy :: SProxy head) (SProxy :: SProxy tail) 0

class NatConcat head tail where
  reflectNat' :: SProxy head -> SProxy tail -> Int -> Int

instance natConcatNil ::
  ( IsNat head
  ) => NatConcat head "" where
  reflectNat' head _ = (_ + reflectNat head)
else
instance natConcatCons ::
  ( Symbol.Cons head' tail' tail
  , NatConcat head' tail'
  , IsNat head
  ) => NatConcat head tail where
  reflectNat' head _ = reflectNat' (SProxy :: SProxy head') (SProxy :: SProxy tail') <<< (_ * 10) <<< (_ + reflectNat head)

----------------------------------------------------------------
-- repl:
-- > reflectNat (SProxy :: SProxy "123456")
-- 123456

-- > reflectNat (SProxy :: SProxy "1")
-- 1

-- > reflectNat (SProxy :: SProxy "0")
-- 0

-- > reflectNat (SProxy :: SProxy "91")
-- 91

-- > reflectNat (SProxy :: SProxy "123a")
-- Err