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