]> Git — Sourcephile - majurity.git/blob - hjugement-protocol/Utils/MeasuredList.hs
protocol: change F to be a Natural, not an Integer.
[majurity.git] / 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)