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