From 7f9383b2dd0fd9816a608b7a14ac517a9ff56aa6 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 28 May 2024 14:51:48 +0200
Subject: Add permFromList

---
 src/Data/Array/Mixed.hs | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Data/Array')

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
-- 
cgit v1.2.3-70-g09d2