
   0 | module 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 Decidable.Equality
   8 | import Syntax.WithProof
   9 | 
  10 | public export
  11 | interface Cons a s | s where
  12 |   singleton : a -> s
  13 |   uncons : s -> Maybe (a, s)
  14 | 
  15 | public export
  16 | Cons Char String where
  17 |   singleton = cast
  18 |   uncons = strUncons
  19 | 
  20 | public export
  21 | Cons a (List a) where
  22 |   singleton = pure
  23 |   uncons [] = Nothing
  24 |   uncons (x :: xs) = Just (x, xs)
  25 | 
  26 | ||| a simple incremental parser
  27 | public export
  28 | data Parser : (input : Type) -> (error : Type) -> (a : Type) -> Type where
  29 |   Fail : e -> Parser i e a
  30 |   Pure : (leftover : i) -> a -> Parser i e a
  31 |   More : (on_feed : (i -> Parser i e a)) -> Parser i e a
  32 |   Alt : Parser i e a -> Lazy (Parser i e a) -> Parser i e a
  33 | 
  34 | public export
  35 | Functor (Parser i e) where
  36 |   map f (Fail e) = Fail e
  37 |   map f (Pure leftover x) = Pure leftover (f x)
  38 |   map f (More on_feed) = More (map f . on_feed)
  39 |   map f (Alt p1 p2) = Alt (map f p1) (map f p2)
  40 | 
  41 | ||| maps over the errors of the parser
  42 | public export
  43 | map_error : (e -> e') -> Parser i e a -> Parser i e' a
  44 | map_error f (Fail e) = Fail (f e)
  45 | map_error f (Pure leftover x) = Pure leftover x
  46 | map_error f (More on_feed) = More (map_error f . on_feed)
  47 | map_error f (Alt p1 p2) = Alt (map_error f p1) (map_error f p2)
  48 | 
  49 | public export
  50 | (<|>) : Semigroup e => Parser i e a -> Lazy (Parser i e a) -> Parser i e a
  51 | Fail e <|> p = map_error (e <+>) p
  52 | Pure leftover x <|> p = Pure leftover x
  53 | p <|> q = Alt p q
  54 | 
  55 | ||| fail with an error
  56 | public export
  57 | fail : e -> Parser i e a
  58 | fail = Fail
  59 | 
  60 | ||| feed input into the parser incrementally
  61 | public export
  62 | feed : (Semigroup e, Semigroup i) => i -> Parser i e a -> Parser i e a
  63 | feed input (Fail e) = Fail e
  64 | feed input (Pure leftover x) = Pure (leftover <+> input) x
  65 | feed input (More on_feed) = on_feed input
  66 | feed input (Alt p1 p2) = feed input p1 <|> feed input p2
  67 | 
  68 | apply : (Semigroup e, Semigroup i) => (Parser i e a -> Parser i e b) -> Parser i e a -> Parser i e b
  69 | apply f (Fail msg) = Fail msg
  70 | apply f (Alt p1 p2) = Alt (f p1) (f p2)
  71 | apply f (More on_feed) = More (f . on_feed)
  72 | apply f parser = More (\input => f $ feed input parser)
  73 | 
  74 | public export
  75 | pure : Monoid i => a -> Parser i e a
  76 | pure x = Pure neutral x
  77 | 
  78 | public export
  79 | (<*>) : (Semigroup e, Monoid i) => Parser i e (a -> b) -> Lazy (Parser i e a) -> Parser i e b
  80 | Pure leftover f <*> p = map f $ feed leftover p
  81 | p1 <*> p2 = apply (<*> p2) p1
  82 | 
  83 | public export
  84 | (<*) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e a
  85 | x <* y = map const x <*> y
  86 | 
  87 | public export
  88 | (*>) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e b
  89 | x *> y = map (const id) x <*> y
  90 | 
  91 | public export
  92 | (>>=) : (Semigroup e, Monoid i) => Parser i e a -> (a -> Parser i e b) -> Parser i e b
  93 | (>>=) (Pure leftover x) f = feed leftover $ f x
  94 | (>>=) p f = apply (>>= f) p
  95 | 
  96 | public export
  97 | more : (i -> Parser i e a) -> Parser i e a
  98 | more = More
  99 | 
 100 | ||| peek into the next token without consuming it
 101 | public export
 102 | peek : Cons c i => Parser i e c
 103 | peek = more $ \input =>
 104 |   case uncons input of
 105 |     Just (x, _) => Pure input x
 106 |     Nothing => peek
 107 | 
 108 | ||| reads the next token
 109 | public export
 110 | token : Cons c i => Parser i e c
 111 | token = more $ \input =>
 112 |   case uncons input of
 113 |     Just (x, xs) => Pure xs x
 114 |     Nothing => token
 115 | 
 116 | ||| run `p` `k` times and collect the results
 117 | public export
 118 | count : (Semigroup e, Monoid i, Cons c i) => (k : Nat) -> (p : Parser i e a) -> Parser i e (Vect k a)
 119 | count Z parser = pure []
 120 | count (S k) parser = pure $ !parser :: !(count k parser)
 121 | 
 122 | ||| return the result of `p` if it succeeds, otherwise return `x`
 123 | public export
 124 | option : (Semigroup e, Monoid i) => (x : a) -> (p : Parser i e a) -> Parser i e a
 125 | option x p = p <|> pure x
 126 | 
 127 | mutual
 128 |   public export
 129 |   some : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List1 a)
 130 |   some p = pure $ !p ::: !(many p)
 131 | 
 132 |   public export
 133 |   many : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List a)
 134 |   many p = option [] (forget <$> some p)
 135 | 
 136 | namespace Error
 137 |   ||| example: `SimpleError String`
 138 |   public export
 139 |   data SimpleError : Type -> Type where
 140 |     Msg : a -> SimpleError a
 141 |     Alt : SimpleError a -> SimpleError a -> SimpleError a
 142 |     Under : a -> SimpleError a -> SimpleError a
 143 | 
 144 |   public export
 145 |   Semigroup (SimpleError a) where
 146 |     (<+>) = Alt
 147 | 
 148 |   public export
 149 |   Show a => Show (SimpleError a) where
 150 |     show (Msg x) = show x
 151 |     show (Alt a b) = "(" <+> show a <+> " <|> " <+> show b <+> ")"
 152 |     show (Under x a) = "(" <+> show x <+> ": " <+> show a <+> ")"
 153 | 
 154 |   public export
 155 |   msg : e -> SimpleError e
 156 |   msg = Msg
 157 | 
 158 |   public export
 159 |   under : e -> Parser i (SimpleError e) a -> Parser i (SimpleError e) a
 160 |   under = map_error . Under
 161 |