{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, ExplicitForAll #-}
module TcTypeNatSimple where
import GHC.TypeLits as L
import Data.Proxy

--------------------------------------------------------------------------------
-- Test evaluation
e1 :: Proxy (2 + 3) -> Proxy 5
e1 = id

e2 :: Proxy (2 L.* 3) -> Proxy 6
e2 = id

e3 :: Proxy (2 ^ 3) -> Proxy 8
e3 = id

e4 :: Proxy (0 + x) -> Proxy x
e4 = id

e5 :: Proxy (x + 0) -> Proxy x
e5 = id

e6 :: Proxy (x L.* 0) -> Proxy 0
e6 = id

e7 :: Proxy (0 L.* x) -> Proxy 0
e7 = id

e8 :: Proxy (x L.* 1) -> Proxy x
e8 = id

e9 :: Proxy (1 L.* x) -> Proxy x
e9 = id

e10 :: Proxy (x ^ 1) -> Proxy x
e10 = id

e11 :: Proxy (1 ^ x) -> Proxy 1
e11 = id

e12 :: Proxy (x ^ 0) -> Proxy 1
e12 = id

e13 :: Proxy (1 <=? 2) -> Proxy True
e13 = id

e14 :: Proxy (2 <=? 1) -> Proxy False
e14 = id

e15 :: forall (x :: Nat). Proxy (x <=? x) -> Proxy True
e15 = id

e17 :: Proxy (3 - 2) -> Proxy 1
e17 = id

e18 :: Proxy (a - 0) -> Proxy a
e18 = id

e19 :: Proxy (Div 10 3) -> Proxy 3
e19 = id

e20 :: Proxy (Div x 1) -> Proxy x
e20 = id

e21 :: Proxy (Mod 10 3) -> Proxy 1
e21 = id

e22 :: Proxy (Mod x 1) -> Proxy 0
e22 = id

e23 :: Proxy (Log2 10) -> Proxy 3
e23 = id

--------------------------------------------------------------------------------
-- Test interactions with inerts

-- ti1 :: Proxy (x + y) -> Proxy x -> ()
-- ti1 _ _ = ()

ti2 :: Proxy (y + x) -> Proxy x -> ()
ti2 _ _ = ()

ti3 :: Proxy (2 L.* y) -> ()
ti3 _ = ()

ti4 :: Proxy (y L.* 2) -> ()
ti4 _ = ()

ti5 :: Proxy (2 ^ y) -> ()
ti5 _ = ()

ti6 :: Proxy (y ^ 2) -> ()
ti6 _ = ()

ti8 :: Proxy (x - y) -> Proxy x -> ()
ti8 _ _ = ()

ti9 :: Proxy (y - x) -> Proxy x -> ()
ti9 _ _ = ()