module Text.Parser import Data.Bool.Extraimport Data.List import public Text.Parser.Coreimport public Text.Quantityimport public Text.Token %default total ||| Parse a terminal based on a kind of token.exportmatch : (Eq k, TokenKind k) =>        (kind : k) ->        Grammar (Token k) True (TokType kind)match kind = terminal "Unrecognised input" $  \(Tok kind' text) => if kind' == kind                          then Just $ tokValue kind text                          else Nothing ||| Optionally parse a thing, with a default value if the grammar doesn't||| match. May match the empty input.exportoption : {c : Bool} ->         (def : a) -> (p : Grammar tok c a) ->         Grammar tok False aoption {c = False} def p = p <|> pure defoption {c = True} def p = p <|> pure def ||| Optionally parse a thing.||| To provide a default value, use `option` instead.exportoptional : {c : Bool} ->           (p : Grammar tok c a) ->           Grammar tok False (Maybe a)optional p = option Nothing (map Just p) ||| Try to parse one thing or the other, producing a value that indicates||| which option succeeded. If both would succeed, the left option||| takes priority.exportchoose : {c1, c2 : Bool} ->          (l : Grammar tok c1 a) ->         (r : Grammar tok c2 b) ->         Grammar tok (c1 && c2) (Either a b)choose l r = map Left l <|> map Right r ||| Produce a grammar by applying a function to each element of a container,||| then try each resulting grammar until the first one succeeds. Fails if the||| container is empty.exportchoiceMap : {c : Bool} ->            (a -> Grammar tok c b) ->            Foldable t => t a ->            Grammar tok c bchoiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in                                               f x <|> acc)                           (fail "No more options") xs ||| Try each grammar in a container until the first one succeeds.||| Fails if the container is empty.exportchoice : Foldable t =>          {c : Bool} ->         t (Grammar tok c a) ->         Grammar tok c achoice {c} = choiceMap {c=c} id mutual  ||| Parse one or more things  export  some : Grammar tok True a ->         Grammar tok True (List a)  some p = pure (!p :: !(many p))   ||| Parse zero or more things (may match the empty input)  export  many : Grammar tok True a ->         Grammar tok False (List a)  many p = option [] (some p) ||| Parse one or more instances of `p`, returning the parsed items and proof||| that the resulting list is non-empty.exportsome' : (p : Grammar tok True a) ->        Grammar tok True (xs : List a ** NonEmpty xs)some' p = pure (!p :: !(many p) ** IsNonEmpty) mutual  private  count1 : (q : Quantity) ->           (p : Grammar tok True a) ->           Grammar tok True (List a)  count1 q p = do x <- p                  seq (count q p)                      (\xs => pure (x :: xs))   ||| Parse `p`, repeated as specified by `q`, returning the list of values.  export  count : (q : Quantity) ->          (p : Grammar tok True a) ->          Grammar tok (isSucc (min q)) (List a)  count (Qty Z Nothing) p = many p  count (Qty Z (Just Z)) _ = pure []  count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p  count (Qty (S min) Nothing) p = count1 (atLeast min) p  count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"  count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p mutual  ||| Parse one or more instances of `p` until `end` succeeds, returning the  ||| list of values from `p`. Guaranteed to consume input.  export  someTill : {c : Bool} ->             (end : Grammar tok c e) ->             (p : Grammar tok True a) ->             Grammar tok True (List a)  someTill {c} end p = do x <- p                          seq (manyTill end p)                              (\xs => pure (x :: xs))   ||| Parse zero or more instances of `p` until `end` succeeds, returning the  ||| list of values from `p`. Guaranteed to consume input if `end` consumes.  export  manyTill : {c : Bool} ->             (end : Grammar tok c e) ->             (p : Grammar tok True a) ->             Grammar tok c (List a)  manyTill {c} end p = rewrite sym (andTrueNeutral c) in                               map (const []) end <|> someTill end p ||| Parse one or more instances of `p` until `end` succeeds, returning the||| list of values from `p`, along with a proof that the resulting list is||| non-empty.exportsomeTill' : {c : Bool} ->            (end : Grammar tok c e) ->            (p : Grammar tok True a) ->            Grammar tok True (xs : List a ** NonEmpty xs)someTill' end p  = do x <- p       seq (manyTill end p)           (\xs => pure (x :: xs ** IsNonEmpty)) mutual  ||| Parse one or more instance of `skip` until `p` is encountered,  ||| returning its value.  export  afterSome : {c : Bool} ->              (skip : Grammar tok True s) ->              (p : Grammar tok c a) ->              Grammar tok True a  afterSome skip p = do skip                        afterMany skip p   ||| Parse zero or more instance of `skip` until `p` is encountered,  ||| returning its value.  export  afterMany : {c : Bool} ->              (skip : Grammar tok True s) ->              (p : Grammar tok c a) ->              Grammar tok c a  afterMany {c} skip p = rewrite sym (andTrueNeutral c) in                                 p <|> afterSome skip p ||| Parse one or more things, each separated by another thing.exportsepBy1 : {c : Bool} ->         (sep : Grammar tok True s) ->         (p : Grammar tok c a) ->         Grammar tok c (List a)sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in                           [| p :: many (sep *> p) |] ||| Parse zero or more things, each separated by another thing. May||| match the empty input.exportsepBy : {c : Bool} ->        (sep : Grammar tok True s) ->        (p : Grammar tok c a) ->        Grammar tok False (List a)sepBy sep p = option [] $ sepBy1 sep p ||| Parse one or more instances of `p` separated by `sep`, returning the||| parsed items and proof that the resulting list is non-empty.exportsepBy1' : {c : Bool} ->         (sep : Grammar tok True s) ->         (p : Grammar tok c a) ->         Grammar tok c (xs : List a ** NonEmpty xs)sepBy1' {c} sep p  = rewrite sym (orFalseNeutral c) in            seq p (\x => do xs <- many (sep *> p)                            pure (x :: xs ** IsNonEmpty)) ||| Parse one or more instances of `p` separated by and optionally terminated by||| `sep`.exportsepEndBy1 : {c : Bool} ->            (sep : Grammar tok True s) ->            (p : Grammar tok c a) ->            Grammar tok c (List a)sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in                              sepBy1 sep p <* optional sep ||| Parse zero or more instances of `p`, separated by and optionally terminated||| by `sep`. Will not match a separator by itself.exportsepEndBy : {c : Bool} ->           (sep : Grammar tok True s) ->           (p : Grammar tok c a) ->           Grammar tok False (List a)sepEndBy sep p = option [] $ sepEndBy1 sep p ||| Parse zero or more instances of `p`, separated by and optionally terminated||| by `sep`, returning the parsed items and a proof that the resulting list||| is non-empty.exportsepEndBy1' : {c : Bool} ->             (sep : Grammar tok True s) ->             (p : Grammar tok c a) ->             Grammar tok c (xs : List a ** NonEmpty xs)sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in                               sepBy1' sep p <* optional sep ||| Parse one or more instances of `p`, separated and terminated by `sep`.exportendBy1 : {c : Bool} ->         (sep : Grammar tok True s) ->         (p : Grammar tok c a) ->         Grammar tok True (List a)endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in                                  p <* sep exportendBy : {c : Bool} ->        (sep : Grammar tok True s) ->        (p : Grammar tok c a) ->        Grammar tok False (List a)endBy sep p = option [] $ endBy1 sep p ||| Parse zero or more instances of `p`, separated and terminated by `sep`,||| returning the parsed items and a proof that the resulting list is non-empty.exportendBy1' : {c : Bool} ->          (sep : Grammar tok True s) ->          (p : Grammar tok c a) ->          Grammar tok True (xs : List a ** NonEmpty xs)endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in                                    p <* sep ||| Parse an instance of `p` that is between `left` and `right`.exportbetween : {c : Bool} ->          (left : Grammar tok True l) ->          (right : Grammar tok True r) ->          (p : Grammar tok c a) ->          Grammar tok True abetween left right contents = left *> contents <* right