0 | module Text.Parse.Syntax
  1 |
  2 | import Text.Parse.Manual
  3 |
  4 | %default total
  5 |
  6 | %hide Prelude.(*>)
  7 | %hide Prelude.(<*)
  8 | %hide Prelude.(<*>)
  9 | %hide Prelude.pure
 10 |
 11 | --------------------------------------------------------------------------------
 12 | --          Applicative Syntax
 13 | --------------------------------------------------------------------------------
 14 |
 15 | public export %inline
 16 | pure : a -> Grammar False t e a
 17 | pure v xs = Succ0 v xs
 18 |
 19 | public export %inline
 20 | (<*>) : Grammar b1 t e (a -> b) -> Grammar b2 t e a -> Grammar (b1 || b2) t e b
 21 | (<*>) gf ga xs =
 22 |   let Succ0 f r1 @{p} := gf xs | Fail0 err => Fail0 err
 23 |       Succ0 v r2 @{q} := ga r1 | Fail0 err => Fail0 err
 24 |    in Succ0 (f v) r2 @{swapOr $ trans q p}
 25 |
 26 | public export %inline
 27 | (*>) : Grammar b1 t e () -> Grammar b2 t e a -> Grammar (b1 || b2) t e a
 28 | (*>) g1 g2 xs =
 29 |   let Succ0 () r1 @{p} := g1 xs | Fail0 err => Fail0 err
 30 |       Succ0 v  r2 @{q} := g2 r1 | Fail0 err => Fail0 err
 31 |    in Succ0 v r2 @{swapOr $ trans q p}
 32 |
 33 | ||| Version of `(*>)` specialized for strict second grammars
 34 | public export %inline
 35 | seqt : Grammar b t e () -> Grammar True t e a -> Grammar True t e a
 36 | seqt x y = orTrue $ x *> y
 37 |
 38 | public export %inline
 39 | (<*) : Grammar b1 t e a -> Grammar b2 t e () -> Grammar (b1 || b2) t e a
 40 | (<*) g1 g2 xs =
 41 |   let Succ0 v  r1 @{p} := g1 xs | Fail0 err => Fail0 err
 42 |       Succ0 () r2 @{q} := g2 r1 | Fail0 err => Fail0 err
 43 |    in Succ0 v r2 @{swapOr $ trans q p}
 44 |
 45 | --------------------------------------------------------------------------------
 46 | --          Parentheses
 47 | --------------------------------------------------------------------------------
 48 |
 49 | ||| Drops the given token after parsing the given grammar
 50 | public export %inline
 51 | before : Interpolation t => Eq t => Grammar b t e a -> (c : t) -> Grammar True t e a
 52 | before f c = orTrue $ f <* exact c
 53 |
 54 | ||| Drops the given token before parsing the given grammar
 55 | public export %inline
 56 | after : Interpolation t => Eq t => (o : t) -> Grammar b t e a -> Grammar True t e a
 57 | after o f = exact o *> f
 58 |
 59 | ||| Wrapps the given grammar between an opening and closing token.
 60 | |||
 61 | ||| Note: This fails with an `Unclosed` exception if the end of
 62 | |||       input is reached without closing the opening token.
 63 | public export %inline
 64 | between : Interpolation t => Eq t => (o,c : t) -> Grammar b t e a -> Grammar True t e a
 65 | between o c f (B x b :: xs) = case o == x of
 66 |   False => expected b o "\{x}"
 67 |   True  =>
 68 |     let Succ0 v (B y b2 :: ys) := succT (f xs) | res => failInParen b x res
 69 |      in if c == y then Succ0 v ys else unexpected (B y b2)
 70 | between o c f [] = eoi
 71 |
 72 | --------------------------------------------------------------------------------
 73 | --          Lists
 74 | --------------------------------------------------------------------------------
 75 |
 76 | public export
 77 | optional : Grammar b t e a -> Grammar False t e (Maybe a)
 78 | optional f ts = weaken $ (Just <$> f ts) <|> Succ0 Nothing ts @{Same}
 79 |
 80 | public export
 81 | manyOnto :
 82 |      (fatal : InnerError e -> Bool)
 83 |   -> Grammar True t e a
 84 |   -> SnocList a
 85 |   -> AccGrammar False t e (List a)
 86 | manyOnto fatal f sx ts (SA r) = case f ts of
 87 |   Succ0 v ys => succF $ manyOnto fatal f (sx :< v) ys r 
 88 |   Fail0 x    => if fatal x.val then Fail0 x else Succ0 (sx <>> []) ts
 89 |
 90 | ||| Runs the given parser zero or more times, accumulating the
 91 | ||| results in a list.
 92 | |||
 93 | ||| Note: This will fail in case of a fatal error, which allows for
 94 | |||       more fine-grained control over whether a parser is successful
 95 | |||       or not.
 96 | public export %inline
 97 | manyF :
 98 |      (fatal : InnerError e -> Bool)
 99 |   -> Grammar True t e a
100 |   -> Grammar False t e (List a)
101 | manyF fatal f ts = manyOnto fatal f [<] ts suffixAcc
102 |
103 | ||| Runs the given parser zero or more times, accumulating the
104 | ||| results in a list.
105 | |||
106 | ||| Note: This will never fail, even if the given parser fails
107 | |||       with an error that should be fatal. User `manyF` to
108 | |||       have the ability to specify fatal errors.
109 | public export %inline
110 | many : Grammar True t e a -> Grammar False t e (List a)
111 | many = manyF (const False)
112 |
113 | ||| Runs the given parser one or more times, accumulating the
114 | ||| results in a non-empty list.
115 | |||
116 | ||| Note: This will fail in case of a fatal error, even when parsing
117 | |||       the tail of the list, which allows for
118 | |||       more fine-grained control over whether a parser is successful
119 | |||       or not.
120 | public export %inline
121 | someF :
122 |      (fatal : InnerError e -> Bool)
123 |   -> Grammar True t e a
124 |   -> Grammar True t e (List1 a)
125 | someF fatal f = [| f ::: manyF fatal f|]
126 |
127 | ||| Runs the given parser one or more times, accumulating the
128 | ||| results in a non-empty list.
129 | |||
130 | ||| Note: User `manyF` for the ability to specify fatal errors.
131 | public export %inline
132 | some : Grammar True t e a -> Grammar True t e (List1 a)
133 | some = someF (const False)
134 |
135 | ||| Runs the given parser one or more times, separating occurences with
136 | ||| the given separator.
137 | |||
138 | ||| Note: This will fail in case of a fatal error, even when parsing
139 | |||       the tail of the list, which allows for
140 | |||       more fine-grained control over whether a parser is successful
141 | |||       or not.
142 | |||
143 | |||       Consider using `sepByExact1` for better error behavior,
144 | |||       if the separator consists of a single, constant token.
145 | public export %inline
146 | sepByF1 :
147 |      (fatal : InnerError e -> Bool)
148 |   -> (sep : Grammar b t e ())
149 |   -> Grammar True t e a
150 |   -> Grammar True t e (List1 a)
151 | sepByF1 fatal sep f = [| f ::: manyF fatal (seqt sep f)|]
152 |
153 | ||| Like `sepBy1` but with better error behavior:
154 | ||| If the separator was recognized, this fails instead of
155 | ||| aborting with a partial list.
156 | public export %inline
157 | sepByExact1 :
158 |      Interpolation t
159 |   => Eq t
160 |   => Eq e
161 |   => (sep : t)
162 |   -> Grammar True t e a
163 |   -> Grammar True t e (List1 a)
164 | sepByExact1 sep = sepByF1 isExp (exact sep)
165 |   where
166 |     isExp : InnerError e -> Bool
167 |     isExp (Expected [s] _) = s == interpolate sep
168 |     isExp _                = False
169 |