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 Control.Applicative (Applicative(..))
  23 import Data.Bool
  24 import Data.Eq (Eq(..))
  25 import Data.Foldable (Foldable)
  26 import Data.Function ((.), flip)
  27 import Data.Functor (Functor(..), (<$>))
  28 import Data.Int (Int)
  29 import Data.Maybe (Maybe(..))
  30 import Data.Monoid (Monoid(..))
  31 import Data.Ord (Ord(..), Ordering(..))
  32 import Data.Proxy (Proxy(..))
  33 import Data.Traversable (Traversable(..))
  34 import Data.Tuple (fst, snd)
  35 import Data.Type.Equality ((:~:)(..))
  36 import GHC.TypeNats
  37 import Numeric.Natural (Natural)
  38 import Prelude ((-), undefined, fromIntegral)
  39 import Text.Show (Show(..))
  40 import Unsafe.Coerce (unsafeCoerce)
  41 import qualified Control.Monad.Trans.State.Strict as S
  42 import qualified Data.ByteString as BS
  43 import qualified Data.List as List
  44
  45 import Utils.Constraint
  46 import Utils.Natural
  47
  48 -- * Type 'List'
  49 -- | A list whose length is known at the type-level.
  50 newtype MeasuredList (n::Nat) a = ML [a]
  51  deriving (Eq,Ord,Functor,Foldable,Traversable)
  52 instance Show a => Show (MeasuredList n a) where
  53         showsPrec p (ML xs) = showsPrec p xs
  54
  55 cons :: a -> MeasuredList n a -> MeasuredList (n+1) a
  56 cons x (ML xs) = ML (x:xs)
  57 uncons :: (1<=n) => MeasuredList n a -> (a, MeasuredList (n-1) a)
  58 uncons (ML (x:xs)) = (x, ML xs)
  59
  60 pattern (:#) :: (1<=n) => a -> MeasuredList (n-1) a -> MeasuredList n a
  61 pattern (:#) x xs <- (uncons -> (x,xs))
  62  where  (:#) x xs | ML l <- cons x xs = ML l
  63 infixr 5 :#
  64
  65 fromList :: forall n a. KnownNat n => [a] -> Maybe (MeasuredList n a)
  66 fromList xs | List.length xs == fromIntegral (natVal (Proxy::Proxy n)) = Just (ML xs)
  67             | otherwise = Nothing
  68
  69 head :: (1<=n) => MeasuredList n a -> a
  70 head (ML xs) = List.head xs
  71 tail :: (1<=n) => MeasuredList n a -> MeasuredList (n-1) a
  72 tail (ML xs) = ML (List.tail xs)
  73 concat :: MeasuredList n a -> MeasuredList m a -> MeasuredList (n+m) a
  74 concat (ML xs) (ML ys) = ML (xs List.++ ys)
  75 reverse :: MeasuredList n a -> MeasuredList n a
  76 reverse (ML xs) = ML (List.reverse xs)
  77 length :: forall n a. KnownNat n => MeasuredList n a -> Natural
  78 length _xs = natVal (Proxy::Proxy n)
  79
  80 splitAt :: forall i n a proxy.
  81  KnownNat i => (i<=n) =>
  82  proxy i -> MeasuredList n a -> (MeasuredList i a, MeasuredList (n-i) a)
  83 splitAt _i (ML xs) = (ML ls, ML rs)
  84         where
  85         (ls,rs) = List.splitAt i xs
  86         i = fromIntegral (natVal (Proxy::Proxy i))
  87
  88 zip :: MeasuredList n a -> MeasuredList n b -> MeasuredList n (a,b)
  89 zip (ML as) (ML bs) = ML (List.zip as bs)
  90 zipWith :: (a -> b -> c) -> MeasuredList n a -> MeasuredList n b -> MeasuredList n c
  91 zipWith f (ML as) (ML bs) = ML (List.zipWith f as bs)