[Git][ghc/ghc][wip/T24245] Add reflections of GHC.TypeLits/Nats type families
Oleg Grenrus (@phadej)
gitlab at gitlab.haskell.org
Mon May 13 21:44:01 UTC 2024
Oleg Grenrus pushed to branch wip/T24245 at Glasgow Haskell Compiler / GHC
Commits:
2632abcf by Oleg Grenrus at 2024-05-14T00:43:51+03:00
Add reflections of GHC.TypeLits/Nats type families
- - - - -
7 changed files:
- libraries/ghc-experimental/ghc-experimental.cabal
- + libraries/ghc-experimental/src/GHC/TypeLits/Experimental.hs
- + libraries/ghc-experimental/src/GHC/TypeNats/Experimental.hs
- testsuite/tests/interface-stability/ghc-experimental-exports.stdout
- + testsuite/tests/numeric/should_run/T24245.hs
- + testsuite/tests/numeric/should_run/T24245.stdout
- testsuite/tests/numeric/should_run/all.T
Changes:
=====================================
libraries/ghc-experimental/ghc-experimental.cabal
=====================================
@@ -23,9 +23,11 @@ common warnings
library
import: warnings
exposed-modules:
- GHC.Profiling.Eras
- Data.Tuple.Experimental
Data.Sum.Experimental
+ Data.Tuple.Experimental
+ GHC.Profiling.Eras
+ GHC.TypeLits.Experimental
+ GHC.TypeNats.Experimental
Prelude.Experimental
if arch(wasm32)
exposed-modules: GHC.Wasm.Prim
=====================================
libraries/ghc-experimental/src/GHC/TypeLits/Experimental.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE TypeOperators #-}
+module GHC.TypeLits.Experimental (
+ appendSSymbol,
+ consSSymbol,
+ sCharToSNat,
+ sNatToSChar,
+) where
+
+import GHC.Internal.TypeLits
+import Data.Char (ord, chr)
+
+appendSSymbol :: SSymbol a -> SSymbol b -> SSymbol (AppendSymbol a b)
+appendSSymbol (UnsafeSSymbol a) (UnsafeSSymbol b) = UnsafeSSymbol (a ++ b)
+
+consSSymbol :: SChar a -> SSymbol b -> SSymbol (ConsSymbol a b)
+consSSymbol (UnsafeSChar a) (UnsafeSSymbol b) = UnsafeSSymbol (a : b)
+
+sCharToSNat :: SChar a -> SNat (CharToNat a)
+sCharToSNat (UnsafeSChar a) = UnsafeSNat (fromIntegral (ord a))
+
+sNatToSChar :: (n <= 1114111) => SNat n -> SChar (NatToChar n)
+sNatToSChar (UnsafeSNat n) = UnsafeSChar (chr (fromIntegral n))
=====================================
libraries/ghc-experimental/src/GHC/TypeNats/Experimental.hs
=====================================
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE TypeOperators #-}
+module GHC.TypeNats.Experimental (
+ plusSNat,
+ timesSNat,
+ powerSNat,
+ minusSNat,
+ divSNat,
+ modSNat,
+ log2SNat,
+) where
+
+import GHC.Internal.TypeNats
+import GHC.Num.Natural (naturalLog2)
+
+plusSNat :: SNat n -> SNat m -> SNat (n + m)
+plusSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (n + m)
+
+timesSNat :: SNat n -> SNat m -> SNat (n * m)
+timesSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (n * m)
+
+powerSNat :: SNat n -> SNat m -> SNat (n ^ m)
+powerSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (n ^ m)
+
+minusSNat :: (m <= n) => SNat n -> SNat m -> SNat (n - m)
+minusSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (n - m)
+
+divSNat :: (1 <= m) => SNat n -> SNat m -> SNat (Div n m)
+divSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (div n m)
+
+modSNat :: (1 <= m) => SNat n -> SNat m -> SNat (Mod n m)
+modSNat (UnsafeSNat n) (UnsafeSNat m) = UnsafeSNat (mod n m)
+
+log2SNat :: (1 <= n) => SNat n -> SNat (Log2 n)
+log2SNat (UnsafeSNat n) = UnsafeSNat (fromIntegral (naturalLog2 n))
=====================================
testsuite/tests/interface-stability/ghc-experimental-exports.stdout
=====================================
@@ -4322,6 +4322,23 @@ module GHC.Profiling.Eras where
incrementUserEra :: GHC.Types.Word -> GHC.Types.IO GHC.Types.Word
setUserEra :: GHC.Types.Word -> GHC.Types.IO ()
+module GHC.TypeLits.Experimental where
+ -- Safety: Safe-Inferred
+ appendSSymbol :: forall (a :: GHC.Types.Symbol) (b :: GHC.Types.Symbol). GHC.Internal.TypeLits.SSymbol a -> GHC.Internal.TypeLits.SSymbol b -> GHC.Internal.TypeLits.SSymbol (GHC.Internal.TypeLits.AppendSymbol a b)
+ consSSymbol :: forall (a :: GHC.Types.Char) (b :: GHC.Types.Symbol). GHC.Internal.TypeLits.SChar a -> GHC.Internal.TypeLits.SSymbol b -> GHC.Internal.TypeLits.SSymbol (GHC.Internal.TypeLits.ConsSymbol a b)
+ sCharToSNat :: forall (a :: GHC.Types.Char). GHC.Internal.TypeLits.SChar a -> GHC.Internal.TypeNats.SNat (GHC.Internal.TypeLits.CharToNat a)
+ sNatToSChar :: forall (n :: GHC.Num.Natural.Natural). (n GHC.Internal.Data.Type.Ord.<= 1114111) => GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeLits.SChar (GHC.Internal.TypeLits.NatToChar n)
+
+module GHC.TypeNats.Experimental where
+ -- Safety: None
+ divSNat :: forall (m :: GHC.Num.Natural.Natural) (n :: GHC.Internal.TypeNats.Nat). (1 GHC.Internal.Data.Type.Ord.<= m) => GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (GHC.Internal.TypeNats.Div n m)
+ log2SNat :: forall (n :: GHC.Num.Natural.Natural). (1 GHC.Internal.Data.Type.Ord.<= n) => GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat (GHC.Internal.TypeNats.Log2 n)
+ minusSNat :: forall (m :: GHC.Internal.TypeNats.Nat) (n :: GHC.Internal.TypeNats.Nat). (m GHC.Internal.Data.Type.Ord.<= n) => GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (n GHC.Internal.TypeNats.- m)
+ modSNat :: forall (m :: GHC.Num.Natural.Natural) (n :: GHC.Internal.TypeNats.Nat). (1 GHC.Internal.Data.Type.Ord.<= m) => GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (GHC.Internal.TypeNats.Mod n m)
+ plusSNat :: forall (n :: GHC.Internal.TypeNats.Nat) (m :: GHC.Internal.TypeNats.Nat). GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (n GHC.Internal.TypeNats.+ m)
+ powerSNat :: forall (n :: GHC.Internal.TypeNats.Nat) (m :: GHC.Internal.TypeNats.Nat). GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (n GHC.Internal.TypeNats.^ m)
+ timesSNat :: forall (n :: GHC.Internal.TypeNats.Nat) (m :: GHC.Internal.TypeNats.Nat). GHC.Internal.TypeNats.SNat n -> GHC.Internal.TypeNats.SNat m -> GHC.Internal.TypeNats.SNat (n GHC.Internal.TypeNats.* m)
+
module Prelude.Experimental where
-- Safety: Trustworthy
type CSolo :: Constraint -> Constraint
=====================================
testsuite/tests/numeric/should_run/T24245.hs
=====================================
@@ -0,0 +1,83 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import GHC.TypeLits
+import GHC.TypeNats.Experimental
+import GHC.TypeLits.Experimental
+
+main :: IO ()
+main = do
+ testBinary plusSNat (SNat @2) (SNat @3) SNat
+ testBinary timesSNat (SNat @2) (SNat @3) SNat
+ testBinary powerSNat (SNat @2) (SNat @3) SNat
+ testBinary minusSNat (SNat @7) (SNat @3) SNat
+ testBinary divSNat (SNat @7) (SNat @3) SNat
+ testBinary modSNat (SNat @7) (SNat @3) SNat
+ testUnary log2SNat (SNat @7) SNat
+
+ testBinaryS appendSSymbol (SSymbol @"foo") (SSymbol @"bar") SSymbol
+ testBinaryCSS consSSymbol (SChar @'x') (SSymbol @"yz") SSymbol
+ testUnaryCN sCharToSNat (SChar @'x') SNat
+ testUnaryNC sNatToSChar (SNat @62) SChar
+
+testBinary
+ :: (SNat a -> SNat b -> SNat c)
+ -> SNat a
+ -> SNat b
+ -> SNat c
+ -> IO ()
+testBinary f n m p = do
+ print (f n m, p)
+ assertEqualOnShow (f n m) p
+
+testUnary
+ :: (SNat a -> SNat b)
+ -> SNat a
+ -> SNat b
+ -> IO ()
+testUnary f n m = do
+ print (f n, m)
+ assertEqualOnShow (f n) m
+
+testBinaryS
+ :: (SSymbol a -> SSymbol b -> SSymbol c)
+ -> SSymbol a
+ -> SSymbol b
+ -> SSymbol c
+ -> IO ()
+testBinaryS f n m p = do
+ print (f n m, p)
+ assertEqualOnShow (f n m) p
+
+testBinaryCSS
+ :: (SChar a -> SSymbol b -> SSymbol c)
+ -> SChar a
+ -> SSymbol b
+ -> SSymbol c
+ -> IO ()
+testBinaryCSS f n m p = do
+ print (f n m, p)
+ assertEqualOnShow (f n m) p
+
+testUnaryCN
+ :: (SChar a -> SNat b)
+ -> SChar a
+ -> SNat b
+ -> IO ()
+testUnaryCN f n m = do
+ print (f n, m)
+ assertEqualOnShow (f n) m
+
+testUnaryNC
+ :: (SNat a -> SChar b)
+ -> SNat a
+ -> SChar b
+ -> IO ()
+testUnaryNC f n m = do
+ print (f n, m)
+ assertEqualOnShow (f n) m
+
+assertEqualOnShow :: Show a => a -> a -> IO ()
+assertEqualOnShow x y
+ | show x == show y = return ()
+ | otherwise = fail "inequality"
=====================================
testsuite/tests/numeric/should_run/T24245.stdout
=====================================
@@ -0,0 +1,11 @@
+(SNat @5,SNat @5)
+(SNat @6,SNat @6)
+(SNat @8,SNat @8)
+(SNat @4,SNat @4)
+(SNat @2,SNat @2)
+(SNat @1,SNat @1)
+(SNat @2,SNat @2)
+(SSymbol @"foobar",SSymbol @"foobar")
+(SSymbol @"xyz",SSymbol @"xyz")
+(SNat @120,SNat @120)
+(SChar @'>',SChar @'>')
=====================================
testsuite/tests/numeric/should_run/all.T
=====================================
@@ -84,3 +84,4 @@ test('T22671', js_fragile(24259), compile_and_run, [''])
test('foundation', [when(js_arch(), run_timeout_multiplier(2)), js_fragile(24259)], compile_and_run, ['-O -package transformers'])
test('T24066', normal, compile_and_run, [''])
test('div01', normal, compile_and_run, [''])
+test('T24245', normal, compile_and_run, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2632abcf2117bb03e1a8873d8b9c985230e474b9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2632abcf2117bb03e1a8873d8b9c985230e474b9
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240513/76b5210e/attachment-0001.html>
More information about the ghc-commits
mailing list