aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2024-05-28 14:51:48 +0200
committerTom Smeding <tom@tomsmeding.com>2024-05-28 14:51:48 +0200
commit7f9383b2dd0fd9816a608b7a14ac517a9ff56aa6 (patch)
treec74ee97175f8cb8e9de4bb512af5cce62af6e5a6
parent8e7f9981f9b8ca17bb3c46c942116eaa4f7cb0d3 (diff)
Add permFromList
-rw-r--r--src/Data/Array/Mixed.hs7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index 24a8482..1a622fb 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -7,6 +7,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
@@ -720,6 +721,12 @@ snatLengthHList :: HList f list -> SNat (Rank list)
snatLengthHList HNil = SNat
snatLengthHList (_ `HCons` l) | SNat <- snatLengthHList l = SNat
+permFromList :: [Int] -> (forall list. HList SNat list -> r) -> r
+permFromList [] k = k HNil
+permFromList (x : xs) k = withSomeSNat (fromIntegral x) $ \case
+ Just sn -> permFromList xs $ \list -> k (sn `HCons` list)
+ Nothing -> error $ "Data.Array.Mixed.permFromList: negative number in list: " ++ show x
+
type family TakeLen ref l where
TakeLen '[] l = '[]
TakeLen (_ : ref) (x : xs) = x : TakeLen ref xs