hjugement-protocol/Utils/MeasuredList.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DeriveTraversable #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE ViewPatterns #-}
   6 module Utils.MeasuredList
   7  ( type MeasuredList
   8  , pattern (:#)
   9  , cons
  10  , uncons
  11  , head
  12  , tail
  13  , concat
  14  , reverse
  15  , length
  16  , splitAt
  17  , fromList
  18  , zip
  19  , zipWith
  20  ) where
  21
  22 import Data.Bool
  23 import Data.Eq (Eq(..))
  24 import Data.Foldable (Foldable)
  25 import Data.Functor (Functor(..))
  26 import Data.Maybe (Maybe(..))
  27 import Data.Ord (Ord(..))
  28 import Data.Proxy (Proxy(..))
  29 import Data.Traversable (Traversable(..))
  30 import GHC.TypeNats
  31 import Numeric.Natural (Natural)
  32 import Prelude (fromIntegral, error)
  33 import Text.Show (Show(..))
  34 import qualified Data.List as List
  35
  36 -- * Type 'List'
  37 -- | A list whose length is known at the type-level.
  38 newtype MeasuredList (n::Nat) a = ML [a]
  39  deriving (Eq,Ord,Functor,Foldable,Traversable)
  40 instance Show a => Show (MeasuredList n a) where
  41         showsPrec p (ML xs) = showsPrec p xs
  42
  43 cons :: a -> MeasuredList n a -> MeasuredList (n+1) a
  44 cons x (ML xs) = ML (x:xs)
  45 uncons :: (1<=n) => MeasuredList n a -> (a, MeasuredList (n-1) a)
  46 uncons (ML (x:xs)) = (x, ML xs)
  47 uncons (ML []) = error "MeasuredList.uncons: impossible happened"
  48
  49 pattern (:#) :: (1<=n) => a -> MeasuredList (n-1) a -> MeasuredList n a
  50 pattern x:#xs <- (uncons -> (x,xs))
  51  where  x:#xs | ML l <- cons x xs = ML l
  52 infixr 5 :#
  53
  54 fromList :: forall n a. KnownNat n => [a] -> Maybe (MeasuredList n a)
  55 fromList xs | List.length xs == fromIntegral (natVal (Proxy::Proxy n)) = Just (ML xs)
  56             | otherwise = Nothing
  57
  58 head :: (1<=n) => MeasuredList n a -> a
  59 head (ML xs) = List.head xs
  60 tail :: (1<=n) => MeasuredList n a -> MeasuredList (n-1) a
  61 tail (ML xs) = ML (List.tail xs)
  62 concat :: MeasuredList n a -> MeasuredList m a -> MeasuredList (n+m) a
  63 concat (ML xs) (ML ys) = ML (xs List.++ ys)
  64 reverse :: MeasuredList n a -> MeasuredList n a
  65 reverse (ML xs) = ML (List.reverse xs)
  66 length :: forall n a. KnownNat n => MeasuredList n a -> Natural
  67 length _xs = natVal (Proxy::Proxy n)
  68
  69 splitAt :: forall i n a proxy.
  70  KnownNat i => (i<=n) =>
  71  proxy i -> MeasuredList n a -> (MeasuredList i a, MeasuredList (n-i) a)
  72 splitAt _i (ML xs) = (ML ls, ML rs)
  73         where
  74         (ls,rs) = List.splitAt i xs
  75         i = fromIntegral (natVal (Proxy::Proxy i))
  76
  77 zip :: MeasuredList n a -> MeasuredList n b -> MeasuredList n (a,b)
  78 zip (ML as) (ML bs) = ML (List.zip as bs)
  79 zipWith :: (a -> b -> c) -> MeasuredList n a -> MeasuredList n b -> MeasuredList n c
  80 zipWith f (ML as) (ML bs) = ML (List.zipWith f as bs)