
   0 | module Data.Compress.Utils.Parser
   1 | 
   2 | import Data.List
   3 | import Data.List.Elem
   4 | import Data.List1
   5 | import Data.Vect
   6 | import Data.Void
   7 | import Data.Bits
   8 | import Data.SnocList
   9 | import Decidable.Equality
  10 | import Syntax.WithProof
  11 | import Data.Compress.Utils.Bytes
  12 | 
  13 | public export
  14 | interface Cons a s | s where
  15 |   singleton : a -> s
  16 |   uncons : s -> Maybe (a, s)
  17 | 
  18 | public export
  19 | Cons Char String where
  20 |   singleton = cast
  21 |   uncons = strUncons
  22 | 
  23 | public export
  24 | Cons a (List a) where
  25 |   singleton = pure
  26 |   uncons [] = Nothing
  27 |   uncons (x :: xs) = Just (x, xs)
  28 | 
  29 | public export
  30 | record Bitstream where
  31 |   constructor MkBitstream 
  32 |   content : List (Fin 8, Bits8)
  33 | 
  34 | export
  35 | fromBits8 : List Bits8 -> Bitstream
  36 | fromBits8 = MkBitstream . map (FZ,)
  37 | 
  38 | export
  39 | toBits8 : Bitstream -> List Bits8
  40 | toBits8 bs = mapMaybe (\(i,x) => (guard (i == 0)) $> x) bs.content
  41 | 
  42 | export
  43 | Semigroup Bitstream where
  44 |   a <+> b = MkBitstream (a.content <+> b.content)
  45 | 
  46 | export
  47 | Monoid Bitstream where
  48 |   neutral = MkBitstream []
  49 | 
  50 | export
  51 | is_byte_aligned : Bitstream -> Bool
  52 | is_byte_aligned bs = all (\(i,_) => 0 == i) bs.content
  53 | 
  54 | public export
  55 | Cons Bool Bitstream where
  56 |   singleton x = MkBitstream [(0, if x then 1 else 0)]
  57 |   uncons bitstream =
  58 |     case bitstream.content of
  59 |       [] => Nothing
  60 |       (i, x) :: xs =>
  61 |         case strengthen (FS i) of
  62 |           Just i' => Just (testBit x i, MkBitstream ((i', x) :: xs))
  63 |           Nothing => Just (testBit x i, MkBitstream xs)
  64 | 
  65 | public export
  66 | data Parser : (input : Type) -> (error : Type) -> (a : Type) -> Type where
  67 |   Fail : e -> Parser i e a
  68 |   Pure : (leftover : i) -> a -> Parser i e a
  69 |   More : (on_feed : (i -> Parser i e a)) -> Parser i e a
  70 |   Alt : Parser i e a -> Lazy (Parser i e a) -> Parser i e a
  71 | 
  72 | public export
  73 | Functor (Parser i e) where
  74 |   map f (Fail e) = Fail e
  75 |   map f (Pure leftover x) = Pure leftover (f x)
  76 |   map f (More on_feed) = More (map f . on_feed)
  77 |   map f (Alt p1 p2) = Alt (map f p1) (map f p2)
  78 | 
  79 | public export
  80 | transform : (i -> Either e i') -> (i' -> Either e i) -> Parser i e a -> Parser i' e a
  81 | transform f g (Fail e) = Fail e
  82 | transform f g (Alt p1 p2) = Alt (transform f g p1) (transform f g p2)
  83 | transform f g (Pure leftover x) =
  84 |   case f leftover of
  85 |     Right leftover' => Pure leftover' x
  86 |     Left err => Fail err
  87 | transform f g (More on_feed) = More $ \x =>
  88 |   let Right x' = g x
  89 |       | Left err => Fail err
  90 |   in transform f g $ on_feed x'
  91 | 
  92 | ||| maps over the errors of the parser
  93 | public export
  94 | map_error : (e -> e') -> Parser i e a -> Parser i e' a
  95 | map_error f (Fail e) = Fail (f e)
  96 | map_error f (Pure leftover x) = Pure leftover x
  97 | map_error f (More on_feed) = More (map_error f . on_feed)
  98 | map_error f (Alt p1 p2) = Alt (map_error f p1) (map_error f p2)
  99 | 
 100 | public export
 101 | (<|>) : Semigroup e => Parser i e a -> Lazy (Parser i e a) -> Parser i e a
 102 | Fail e <|> p = map_error (e <+>) p
 103 | Pure leftover x <|> p = Pure leftover x
 104 | p <|> q = Alt p q
 105 | 
 106 | ||| fail with an error
 107 | public export
 108 | fail : e -> Parser i e a
 109 | fail = Fail
 110 | 
 111 | ||| feed input into the parser incrementally
 112 | public export
 113 | feed : (Semigroup e, Semigroup i) => i -> Parser i e a -> Parser i e a
 114 | feed input (Fail e) = Fail e
 115 | feed input (Pure leftover x) = Pure (leftover <+> input) x
 116 | feed input (More on_feed) = on_feed input
 117 | feed input (Alt p1 p2) = feed input p1 <|> feed input p2
 118 | 
 119 | apply : (Semigroup e, Semigroup i) => (Parser i e a -> Parser i e b) -> Parser i e a -> Parser i e b
 120 | apply f (Fail msg) = Fail msg
 121 | apply f (Alt p1 p2) = Alt (f p1) (f p2)
 122 | apply f (More on_feed) = More (f . on_feed)
 123 | apply f parser = More (\input => f $ feed input parser)
 124 | 
 125 | public export
 126 | pure : Monoid i => a -> Parser i e a
 127 | pure x = Pure neutral x
 128 | 
 129 | public export
 130 | (<*>) : (Semigroup e, Monoid i) => Parser i e (a -> b) -> Lazy (Parser i e a) -> Parser i e b
 131 | Pure leftover f <*> p = map f $ feed leftover p
 132 | p1 <*> p2 = apply (<*> p2) p1
 133 | 
 134 | public export
 135 | (<*) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e a
 136 | x <* y = map const x <*> y
 137 | 
 138 | public export
 139 | (*>) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e b
 140 | x *> y = map (const id) x <*> y
 141 | 
 142 | public export
 143 | (>>=) : (Semigroup e, Monoid i) => Parser i e a -> (a -> Parser i e b) -> Parser i e b
 144 | (>>=) (Pure leftover x) f = feed leftover $ f x
 145 | (>>=) p f = apply (>>= f) p
 146 | 
 147 | public export
 148 | more : (i -> Parser i e a) -> Parser i e a
 149 | more = More
 150 | 
 151 | ||| peek into the next token without consuming it
 152 | public export
 153 | peek : Cons c i => Parser i e c
 154 | peek = more $ \input =>
 155 |   case uncons input of
 156 |     Just (x, _) => Pure input x
 157 |     Nothing => peek
 158 | 
 159 | ||| reads the next token
 160 | public export
 161 | token : Cons c i => Parser i e c
 162 | token = more $ \input =>
 163 |   case uncons input of
 164 |     Just (x, xs) => Pure xs x
 165 |     Nothing => token
 166 | 
 167 | ||| run `p` `k` times and collect the results
 168 | public export
 169 | count : (Semigroup e, Monoid i) => (k : Nat) -> (p : Parser i e a) -> Parser i e (Vect k a)
 170 | count Z parser = pure []
 171 | count (S k) parser = pure $ !parser :: !(count k parser)
 172 | 
 173 | ||| return the result of `p` if it succeeds, otherwise return `x`
 174 | public export
 175 | option : (Semigroup e, Monoid i) => (x : a) -> (p : Parser i e a) -> Parser i e a
 176 | option x p = p <|> pure x
 177 | 
 178 | mutual
 179 |   public export
 180 |   some : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List1 a)
 181 |   some p = pure $ !p ::: !(many p)
 182 | 
 183 |   public export
 184 |   many : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List a)
 185 |   many p = option [] (forget <$> some p)
 186 | 
 187 | namespace Error
 188 |   ||| example: `SimpleError String`
 189 |   public export
 190 |   data SimpleError : Type -> Type where
 191 |     Msg : a -> SimpleError a
 192 |     Alt : SimpleError a -> SimpleError a -> SimpleError a
 193 |     Under : a -> SimpleError a -> SimpleError a
 194 | 
 195 |   public export
 196 |   Semigroup (SimpleError a) where
 197 |     (<+>) = Alt
 198 | 
 199 |   public export
 200 |   Show a => Show (SimpleError a) where
 201 |     show (Msg x) = show x
 202 |     show (Alt a b) = "(" <+> show a <+> " <|> " <+> show b <+> ")"
 203 |     show (Under x a) = "(" <+> show x <+> ": " <+> show a <+> ")"
 204 | 
 205 |   public export
 206 |   msg : e -> SimpleError e
 207 |   msg = Msg
 208 | 
 209 |   public export
 210 |   under : e -> Parser i (SimpleError e) a -> Parser i (SimpleError e) a
 211 |   under = map_error . Under
 212 | 
 213 | export
 214 | bit_getbyte : Parser Bitstream e Bits8
 215 | bit_getbyte = more $ \(MkBitstream input) => f input
 216 |   where
 217 |   f : List (Fin 8, Bits8) -> Parser Bitstream e Bits8
 218 |   f ((FZ, x) :: xs) = Pure (MkBitstream xs) x
 219 |   f ((_ , x) :: xs) = f xs
 220 |   f [] = bit_getbyte
 221 | 
 222 | ||| parse the next `n` bytes as a natural number in big endian style
 223 | export
 224 | p_nat : Semigroup e => (n : Nat) -> Parser (List Bits8) e Nat
 225 | p_nat n = cast {to = Nat} . le_to_integer <$> count n token
 226 | 
 227 | export
 228 | p_be_nat : Semigroup e => (n : Nat) -> Parser (List Bits8) e Nat
 229 | p_be_nat n = cast {to = Nat} . le_to_integer . reverse <$> count n token
 230 | 
 231 | export
 232 | le_nat : Semigroup e => (n : Nat) -> Parser Bitstream e Nat
 233 | le_nat n = cast {to = Nat} . le_to_integer <$> count n bit_getbyte
 234 | 
 235 | ||| make sure that `p` MUST consume at least `n` tokens, fails otherwise
 236 | public export
 237 | p_exact : (Cons c i, Monoid i) => (n : Nat) -> (p : Parser i (SimpleError String) a) -> Parser i (SimpleError String) a
 238 | p_exact Z (Pure leftover x) = pure x
 239 | p_exact (S i) (Pure leftover x) = fail $ msg $ "over fed, " <+> show (S i) <+> " bytes more to go"
 240 | p_exact i (Fail msg) = fail msg
 241 | p_exact Z parser = fail $ msg $ "under fed, wants more"
 242 | p_exact (S i) parser = do
 243 |   b <- token
 244 |   p_exact i (feed (singleton b) parser)
 245 | 
 246 | record LazyParser i e a where
 247 |   constructor Lazify
 248 |   parser : Lazy (Parser i e a)
 249 | 
 250 | Functor (LazyParser i e) where
 251 |   map f p = Lazify $ delay $ map {f=Parser i e} f p.parser
 252 | 
 253 | (Semigroup e, Monoid i) => Applicative (LazyParser i e) where
 254 |   pure a = Lazify $ delay $ pure a
 255 |   a <*> b = Lazify $ delay (Parser.(<*>) a.parser b.parser)
 256 | 
 257 | export
 258 | ifA : Monoid i => Bool -> Lazy (Parser i e a) -> Parser i e (Maybe a)
 259 | ifA cond action = if cond then map Just (Force action) else pure Nothing
 260 | 
 261 | export
 262 | for : {i,e: _} -> (Semigroup e, Monoid i, Traversable f) => f a -> (a -> Lazy (Parser i e b)) -> Parser i e (f b)
 263 | for f p = Force (for f (Lazify . p)).parser
 264 | 
 265 | export
 266 | take_until : (Semigroup e, Monoid i) => (a -> Bool) -> Parser i e a -> Parser i e (List a)
 267 | take_until f parser = loop Lin where
 268 |   loop : SnocList a -> Parser i e (List a)
 269 |   loop acc = do
 270 |     t <- parser
 271 |     if not $ f t then loop (acc :< t) else pure $ toList acc
 272 | 
 273 | export
 274 | get_bit : Num n => Parser Bitstream (SimpleError String) n
 275 | get_bit = map (\b => if b then 1 else 0) token
 276 | 
 277 | fin_range : (n : Nat) -> List (Fin n)
 278 | fin_range _ = toList Fin.range
 279 | 
 280 | read_bits : (List Bool -> List Bool) -> Fin 32 -> Parser Bitstream (SimpleError String) Bits32
 281 | read_bits f n = do
 282 |   bits <- toList <$> count (finToNat n) token
 283 |   pure $ foldl (\a,(i,b) => if b then setBit a i else a) 0 $ zip (fin_range 32) (f bits)
 284 | 
 285 | export
 286 | get_bits : ?
 287 | get_bits = read_bits id
 288 | 
 289 | export
 290 | get_huff : ?
 291 | get_huff = read_bits reverse
 292 |