]> Git — Sourcephile - majurity.git/blob - hjugement-protocol/Utils/MeasuredList.hs
protocol: polish description
[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 , 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)