Commit cd504d85 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Fixup basic type-lits test.

There is still one more test that needs fixing:

   indexed-types/should_fail  T7786 [stderr mismatch] (normal)

I need to understand what is going on there, as it appears to be
using the `Sing` constructors a bunch.
parent f76d68d3
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module TcTypeNatSimple where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Test evaluation
e1 :: Sing (2 + 3) -> Sing 5
e1 :: Proxy (2 + 3) -> Proxy 5
e1 = id
e2 :: Sing (2 * 3) -> Sing 6
e2 :: Proxy (2 * 3) -> Proxy 6
e2 = id
e3 :: Sing (2 ^ 3) -> Sing 8
e3 :: Proxy (2 ^ 3) -> Proxy 8
e3 = id
e4 :: Sing (0 + x) -> Sing x
e4 :: Proxy (0 + x) -> Proxy x
e4 = id
e5 :: Sing (x + 0) -> Sing x
e5 :: Proxy (x + 0) -> Proxy x
e5 = id
e6 :: Sing (x * 0) -> Sing 0
e6 :: Proxy (x * 0) -> Proxy 0
e6 = id
e7 :: Sing (0 * x) -> Sing 0
e7 :: Proxy (0 * x) -> Proxy 0
e7 = id
e8 :: Sing (x * 1) -> Sing x
e8 :: Proxy (x * 1) -> Proxy x
e8 = id
e9 :: Sing (1 * x) -> Sing x
e9 :: Proxy (1 * x) -> Proxy x
e9 = id
e10 :: Sing (x ^ 1) -> Sing x
e10 :: Proxy (x ^ 1) -> Proxy x
e10 = id
e11 :: Sing (1 ^ x) -> Sing 1
e11 :: Proxy (1 ^ x) -> Proxy 1
e11 = id
e12 :: Sing (x ^ 0) -> Sing 1
e12 :: Proxy (x ^ 0) -> Proxy 1
e12 = id
e13 :: Sing (1 <=? 2) -> Sing True
e13 :: Proxy (1 <=? 2) -> Proxy True
e13 = id
e14 :: Sing (2 <=? 1) -> Sing False
e14 :: Proxy (2 <=? 1) -> Proxy False
e14 = id
e15 :: Sing (x <=? x) -> Sing True
e15 :: Proxy (x <=? x) -> Proxy True
e15 = id
e16 :: Sing (0 <=? x) -> Sing True
e16 :: Proxy (0 <=? x) -> Proxy True
e16 = id
e17 :: Sing (3 - 2) -> Sing 1
e17 :: Proxy (3 - 2) -> Proxy 1
e17 = id
e18 :: Sing (a - 0) -> Sing a
e18 :: Proxy (a - 0) -> Proxy a
e18 = id
--------------------------------------------------------------------------------
-- Test interactions with inerts
ti1 :: Sing (x + y) -> Sing x -> ()
ti1 :: Proxy (x + y) -> Proxy x -> ()
ti1 _ _ = ()
ti2 :: Sing (y + x) -> Sing x -> ()
ti2 :: Proxy (y + x) -> Proxy x -> ()
ti2 _ _ = ()
ti3 :: Sing (2 * y) -> ()
ti3 :: Proxy (2 * y) -> ()
ti3 _ = ()
ti4 :: Sing (y * 2) -> ()
ti4 :: Proxy (y * 2) -> ()
ti4 _ = ()
ti5 :: Sing (2 ^ y) -> ()
ti5 :: Proxy (2 ^ y) -> ()
ti5 _ = ()
ti6 :: Sing (y ^ 2) -> ()
ti6 :: Proxy (y ^ 2) -> ()
ti6 _ = ()
type family SomeFun (n :: Nat)
ti7 :: (x <= y, y <= x) => Sing (SomeFun x) -> Sing y -> ()
ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()
ti7 _ _ = ()
ti8 :: Sing (x - y) -> Sing x -> ()
ti8 :: Proxy (x - y) -> Proxy x -> ()
ti8 _ _ = ()
ti9 :: Sing (y - x) -> Sing x -> ()
ti9 :: Proxy (y - x) -> Proxy x -> ()
ti9 _ _ = ()
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module Main(main) where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Test top-reactions
tsub :: SingI x => Sing (x + y) -> Sing y -> Sing x
tsub _ _ = sing
tsub :: Proxy (x + y) -> Proxy y -> Proxy x
tsub _ _ = Proxy
tdiv :: SingI x => Sing (x * y) -> Sing y -> Sing x
tdiv _ _ = sing
tdiv :: Proxy (x * y) -> Proxy y -> Proxy x
tdiv _ _ = Proxy
troot :: SingI x => Sing (x ^ y) -> Sing y -> Sing x
troot _ _ = sing
troot :: Proxy (x ^ y) -> Proxy y -> Proxy x
troot _ _ = Proxy
tlog :: SingI y => Sing (x ^ y) -> Sing x -> Sing y
tlog _ _ = sing
tlog :: Proxy (x ^ y) -> Proxy x -> Proxy y
tlog _ _ = Proxy
tleq :: (SingI x, (x <=? y) ~ True) => Sing y -> Sing x
tleq _ = sing
tleq :: ((x <=? y) ~ True) => Proxy y -> Proxy x
tleq _ = Proxy
main :: IO ()
main = print [ show (tsub (sing :: Sing 5) (sing :: Sing 3)) == "2"
, show (tdiv (sing :: Sing 8) (sing :: Sing 2)) == "4"
, show (troot (sing :: Sing 9) (sing :: Sing 2)) == "3"
, show (tlog (sing :: Sing 8) (sing :: Sing 2)) == "3"
, show (tleq (sing :: Sing 0)) == "0"
main = print [ sh (tsub (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
, sh (tdiv (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "4"
, sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
, sh (tlog (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
, sh (tleq (Proxy :: Proxy 0)) == "0"
]
where
sh x = show (natVal x)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment