diff options
author | Tom Smeding <tom@tomsmeding.com> | 2024-05-28 14:51:48 +0200 |
---|---|---|
committer | Tom Smeding <tom@tomsmeding.com> | 2024-05-28 14:51:48 +0200 |
commit | 7f9383b2dd0fd9816a608b7a14ac517a9ff56aa6 (patch) | |
tree | c74ee97175f8cb8e9de4bb512af5cce62af6e5a6 | |
parent | 8e7f9981f9b8ca17bb3c46c942116eaa4f7cb0d3 (diff) |
Add permFromList
-rw-r--r-- | src/Data/Array/Mixed.hs | 7 |
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 |