
   0 | |||This is a slightly modified copy of the same module from `contrib` package.
   1 | module TyRE.Text.Parser
   2 | 
   3 | import public Data.Bool
   4 | import public Data.List
   5 | import public Data.List1
   6 | import public Data.Nat
   7 | import public Data.Vect
   8 | 
   9 | import public TyRE.Text.Parser.Core
  10 | import public TyRE.Text.Quantity
  11 | import public TyRE.Text.Token
  12 | 
  13 | ||| Parse a terminal based on a kind of token.
  14 | public export
  15 | match : (Eq k, TokenKind k) =>
  16 |         (kind : k) ->
  17 |         Grammar (Token k) True (TokType kind)
  18 | match kind = terminal "Unrecognised input" $
  19 |   \(Tok kind' text) => if kind' == kind
  20 |                           then Just $ tokValue kind text
  21 |                           else Nothing
  22 | 
  23 | ||| Optionally parse a thing, with a default value if the grammar doesn't
  24 | ||| match. May match the empty input.
  25 | public export
  26 | option : {c : Bool} ->
  27 |          (def : a) -> (p : Grammar tok c a) ->
  28 |          Grammar tok False a
  29 | option {c = False} def p = p <|> pure def
  30 | option {c = True} def p = p <|> pure def
  31 | 
  32 | ||| Optionally parse a thing.
  33 | ||| To provide a default value, use `option` instead.
  34 | public export
  35 | optional : {c : _} ->
  36 |            (p : Grammar tok c a) ->
  37 |            Grammar tok False (Maybe a)
  38 | optional p = option Nothing (map Just p)
  39 | 
  40 | ||| Try to parse one thing or the other, producing a value that indicates
  41 | ||| which option succeeded. If both would succeed, the left option
  42 | ||| takes priority.
  43 | public export
  44 | choose : {c1, c2 : _} ->
  45 |          (l : Grammar tok c1 a) ->
  46 |          (r : Grammar tok c2 b) ->
  47 |          Grammar tok (c1 && c2) (Either a b)
  48 | choose l r = map Left l <|> map Right r
  49 | 
  50 | ||| Produce a grammar by applying a function to each element of a container,
  51 | ||| then try each resulting grammar until the first one succeeds. Fails if the
  52 | ||| container is empty.
  53 | public export
  54 | choiceMap : {c : Bool} ->
  55 |             (a -> Grammar tok c b) ->
  56 |             Foldable t => t a ->
  57 |             Grammar tok c b
  58 | choiceMap f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
  59 |                                            f x <|> acc)
  60 |                        (fail "No more options") xs
  61 | 
  62 | %hide Prelude.(>>=)
  63 | 
  64 | ||| Try each grammar in a container until the first one succeeds.
  65 | ||| Fails if the container is empty.
  66 | public export
  67 | choice : {c : _} ->
  68 |          Foldable t => t (Grammar tok c a) ->
  69 |          Grammar tok c a
  70 | choice = Parser.choiceMap id
  71 | 
  72 | mutual
  73 |   ||| Parse one or more things
  74 |   public export
  75 |   some : Grammar tok True a ->
  76 |          Grammar tok True (List1 a)
  77 |   some p = pure (!p ::: !(many p))
  78 | 
  79 |   ||| Parse zero or more things (may match the empty input)
  80 |   public export
  81 |   many : Grammar tok True a ->
  82 |          Grammar tok False (List a)
  83 |   many p = option [] (forget <$> some p)
  84 | 
  85 | ||| Parse one or more instances of `p`, returning the parsed items and proof
  86 | ||| that the resulting list is non-empty.
  87 | public export
  88 | some' : (p : Grammar tok True a) ->
  89 |         Grammar tok True (xs : List a ** NonEmpty xs)
  90 | some' p = pure (!p :: !(many p) ** IsNonEmpty)
  91 | 
  92 | mutual
  93 |   public export
  94 |   count1 : (q : Quantity) ->
  95 |            (p : Grammar tok True a) ->
  96 |            Grammar tok True (List a)
  97 |   count1 q p = do x <- p
  98 |                   seq (count q p)
  99 |                       (\xs => pure (x :: xs))
 100 | 
 101 |   ||| Parse `p`, repeated as specified by `q`, returning the list of values.
 102 |   public export
 103 |   count : (q : Quantity) ->
 104 |           (p : Grammar tok True a) ->
 105 |           Grammar tok (isSucc (min q)) (List a)
 106 |   count (Qty Z Nothing) p = many p
 107 |   count (Qty Z (Just Z)) _ = pure []
 108 |   count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
 109 |   count (Qty (S min) Nothing) p = count1 (atLeast min) p
 110 |   count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
 111 |   count (Qty (S min) (Just (S max))) p = count1 (between min max) p
 112 | 
 113 | ||| Parse `p` `n` times, returning the vector of values.
 114 | public export
 115 | countExactly : (n : Nat) ->
 116 |                (p : Grammar tok True a) ->
 117 |                Grammar tok (isSucc n) (Vect n a)
 118 | countExactly Z p = Empty []
 119 | countExactly (S k) p = [| p :: countExactly k p |]
 120 | 
 121 | mutual
 122 |   ||| Parse one or more instances of `p` until `end` succeeds, returning the
 123 |   ||| list of values from `p`. Guaranteed to consume input.
 124 |   public export
 125 |   someTill : {c : Bool} ->
 126 |              (end : Grammar tok c e) ->
 127 |              (p : Grammar tok True a) ->
 128 |              Grammar tok True (List1 a)
 129 |   someTill {c} end p = do x <- p
 130 |                           seq (manyTill end p)
 131 |                               (\xs => pure (x ::: xs))
 132 | 
 133 |   ||| Parse zero or more instances of `p` until `end` succeeds, returning the
 134 |   ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
 135 |   public export
 136 |   manyTill : {c : Bool} ->
 137 |              (end : Grammar tok c e) ->
 138 |              (p : Grammar tok True a) ->
 139 |              Grammar tok c (List a)
 140 |   manyTill {c} end p = rewrite sym (andTrueNeutral c) in
 141 |                                map (const []) end <|> (forget <$> someTill end p)
 142 | 
 143 | mutual
 144 |   ||| Parse one or more instance of `skip` until `p` is encountered,
 145 |   ||| returning its value.
 146 |   public export
 147 |   afterSome : {c : Bool} ->
 148 |               (skip : Grammar tok True s) ->
 149 |               (p : Grammar tok c a) ->
 150 |               Grammar tok True a
 151 |   afterSome skip p = do ignore skip
 152 |                         afterMany skip p
 153 | 
 154 |   ||| Parse zero or more instance of `skip` until `p` is encountered,
 155 |   ||| returning its value.
 156 |   public export
 157 |   afterMany : {c : Bool} ->
 158 |               (skip : Grammar tok True s) ->
 159 |               (p : Grammar tok c a) ->
 160 |               Grammar tok c a
 161 |   afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
 162 |                                  p <|> afterSome skip p
 163 | 
 164 | ||| Parse one or more things, each separated by another thing.
 165 | public export
 166 | sepBy1 : {c : Bool} ->
 167 |          (sep : Grammar tok True s) ->
 168 |          (p : Grammar tok c a) ->
 169 |          Grammar tok c (List1 a)
 170 | sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
 171 |                            [| p ::: many (sep *> p) |]
 172 | 
 173 | ||| Parse zero or more things, each separated by another thing. May
 174 | ||| match the empty input.
 175 | public export
 176 | sepBy : {c : Bool} ->
 177 |         (sep : Grammar tok True s) ->
 178 |         (p : Grammar tok c a) ->
 179 |         Grammar tok False (List a)
 180 | sepBy sep p = option [] $ forget <$> sepBy1 sep p
 181 | 
 182 | ||| Parse one or more instances of `p` separated by and optionally terminated by
 183 | ||| `sep`.
 184 | public export
 185 | sepEndBy1 : {c : Bool} ->
 186 |             (sep : Grammar tok True s) ->
 187 |             (p : Grammar tok c a) ->
 188 |             Grammar tok c (List1 a)
 189 | sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
 190 |                               sepBy1 sep p <* optional sep
 191 | 
 192 | ||| Parse zero or more instances of `p`, separated by and optionally terminated
 193 | ||| by `sep`. Will not match a separator by itself.
 194 | public export
 195 | sepEndBy : {c : Bool} ->
 196 |            (sep : Grammar tok True s) ->
 197 |            (p : Grammar tok c a) ->
 198 |            Grammar tok False (List a)
 199 | sepEndBy sep p = option [] $ forget <$> sepEndBy1 sep p
 200 | 
 201 | ||| Parse one or more instances of `p`, separated and terminated by `sep`.
 202 | public export
 203 | endBy1 : {c : Bool} ->
 204 |          (sep : Grammar tok True s) ->
 205 |          (p : Grammar tok c a) ->
 206 |          Grammar tok True (List1 a)
 207 | endBy1 sep p = some $ rewrite sym (orTrueTrue c) in
 208 |                               p <* sep
 209 | 
 210 | public export
 211 | endBy : {c : Bool} ->
 212 |         (sep : Grammar tok True s) ->
 213 |         (p : Grammar tok c a) ->
 214 |         Grammar tok False (List a)
 215 | endBy sep p = option [] $ forget <$> endBy1 sep p
 216 | 
 217 | ||| Parse an instance of `p` that is between `left` and `right`.
 218 | public export
 219 | between : {c : _} ->
 220 |           (left : Grammar tok True l) ->
 221 |           (right : Inf (Grammar tok True r)) ->
 222 |           (p : Inf (Grammar tok c a)) ->
 223 |           Grammar tok True a
 224 | between left right contents = left *> contents <* right
 225 |