[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