0 | ||| This module provides utilities for writing parsers by hand (without
  1 | ||| using the combinators from module `Text.Parse.Core`).
  2 | |||
  3 | ||| Typically, you get the best performance by using direct pattern matches
  4 | ||| and explicit recursion. However, for those cases where performance is
  5 | ||| not the main issue, this module provides some combinators for
  6 | ||| certain reoccuring patterns.
  7 | |||
  8 | ||| It is strongly recommended to use a lexer and probably one or two
  9 | ||| cleanup passes over the sequence of generated tokens before parsing,
 10 | ||| as this can significantly simplify the parsers.
 11 | |||
 12 | ||| Example parsers can be found in sub-packages `parser-json` and
 13 | ||| `parser-toml`.
 14 | |||
 15 | ||| Note: The raison d'etre of this module is that writing provably total
 16 | |||       parsers for (recursive) syntax trees is cumbersome or even impossible
 17 | |||       when using parser combinators. In such cases, you have to arrange
 18 | |||       things manually, using a `SuffixAcc` helper to proof termination.
 19 | |||       For everything else, the combinators in here can make your life
 20 | |||       easier.
 21 | module Text.Parse.Manual
 22 |
 23 | import public Data.Bool.Rewrite
 24 | import public Data.List1
 25 | import public Data.List.Shift
 26 | import public Data.List.Suffix
 27 | import public Data.List.Suffix.Result
 28 | import public Data.List.Suffix.Result0
 29 |
 30 | import public Text.Bounds
 31 | import public Text.FC
 32 | import public Text.ParseError
 33 |
 34 | import public Text.Lex.Manual
 35 | import public Text.Lex.Shift
 36 |
 37 | %default total
 38 |
 39 | public export
 40 | 0 Res :
 41 |      (strict : Bool)
 42 |   -> (t : Type)
 43 |   -> (ts : List $ Bounded t)
 44 |   -> (e,a : Type)
 45 |   -> Type
 46 | Res b t ts e a = Result0 b (Bounded t) ts (Bounded $ InnerError e) a
 47 |
 48 | public export
 49 | 0 Grammar : (strict : Bool) -> (t,e,a : Type) -> Type
 50 | Grammar strict t e a = (ts : List $ Bounded t) -> Res strict t ts e a
 51 |
 52 | public export
 53 | 0 AccGrammar : (strict : Bool) -> (t,e,a : Type) -> Type
 54 | AccGrammar strict t e a =
 55 |      (ts : List $ Bounded t)
 56 |   -> (0 acc : SuffixAcc ts)
 57 |   -> Res strict t ts e a
 58 |
 59 | ||| Converts a grammar requiring a proof of accessibility to a regular
 60 | ||| grammar.
 61 | public export %inline
 62 | acc : AccGrammar b t e a -> Grammar b t e a
 63 | acc f ts = f ts suffixAcc
 64 |
 65 | --------------------------------------------------------------------------------
 66 | --          Conversions
 67 | --------------------------------------------------------------------------------
 68 |
 69 | public export %inline
 70 | swapOr : {0 x,y : _} -> Grammar (x || y) t e a -> Grammar (y || x) t e a
 71 | swapOr = swapOr (\k => Grammar k t e a)
 72 |
 73 | public export %inline
 74 | orSame : {0 x : _} -> Grammar (x || x) t e a -> Grammar x t e a
 75 | orSame = orSame (\k => Grammar k t e a)
 76 |
 77 | public export %inline
 78 | orTrue : {0 x : _} -> Grammar (x || True) t e a -> Grammar True t e a
 79 | orTrue = orTrue (\k => Grammar k t e a)
 80 |
 81 | public export %inline
 82 | orFalse : {0 x : _} -> Grammar (x || False) t e a -> Grammar x t e a
 83 | orFalse = orFalse (\k => Grammar k t e a)
 84 |
 85 | public export %inline
 86 | swapAnd : {0 x,y : _} -> Grammar (x && y) t e a -> Grammar (y && x) t e a
 87 | swapAnd = swapAnd (\k => Grammar k t e a)
 88 |
 89 | public export %inline
 90 | andSame : {0 x : _} -> Grammar (x && x) t e a -> Grammar x t e a
 91 | andSame = andSame (\k => Grammar k t e a)
 92 |
 93 | public export %inline
 94 | andTrue : {0 x : _} -> Grammar (x && True) t e a -> Grammar x t e a
 95 | andTrue = andTrue (\k => Grammar k t e a)
 96 |
 97 | public export %inline
 98 | andFalse : {0 x : _} -> Grammar (x && False) t e a -> Grammar False t e a
 99 | andFalse = andFalse (\k => Grammar k t e a)
100 |
101 | --------------------------------------------------------------------------------
102 | --          Simple Grammars
103 | --------------------------------------------------------------------------------
104 |
105 | ||| Tries to convert the head of the list of tokens.
106 | ||| Fails with appropriate errors if the list is empty or the conversion
107 | ||| fails.
108 | public export
109 | terminal : Interpolation t => (t -> Maybe a) -> Grammar True t e a
110 | terminal f (B v b :: xs) = case f v of
111 |     Just r  => Succ0 r xs
112 |     Nothing => unexpected (B v b)
113 | terminal _ []            = eoi
114 |
115 | ||| Like `terminal` but fails with a custom error if the conversion fails.
116 | public export
117 | terminalE : (t -> Either e a) -> Grammar True t e a
118 | terminalE f (B v b :: xs) = case f v of
119 |     Right r  => Succ0 r xs
120 |     Left err => custom b err
121 | terminalE _ []            = eoi
122 |
123 | ||| Tries to drop the given token from the head of the list of tokens.
124 | ||| Fails with appropriate errors if the list is empty or the token
125 | ||| at the head does not match.
126 | public export
127 | exact : Interpolation t => Eq t => t -> Grammar True t e ()
128 | exact v (x::xs) = if v == x.val then Succ0 () xs else expected x.bounds v "\{x.val}"
129 | exact v []      = expected NoBounds v ""
130 |
131 | ||| Look at the next token without consuming any input.
132 | public export
133 | peek : Grammar False t e t
134 | peek (x::xs) = Succ0 x.val (x::xs)
135 | peek []      = eoi
136 |
137 | ||| Check whether the next token satisfies a predicate. Does not consume.
138 | public export
139 | nextIs : Interpolation t => (t -> Bool) -> Grammar False t e t
140 | nextIs f (x::xs) = if f x.val then Succ0 x.val (x :: xs) else unexpected x
141 | nextIs f []      = eoi
142 |
143 | ||| Check whether the next token equals the given value. Does not consume.
144 | public export
145 | nextEquals : Interpolation t => Eq t => t -> Grammar False t e t
146 | nextEquals v (x::xs) =
147 |   if v == x.val then Succ0 x.val (x::xs) else expected x.bounds v "\{x.val}"
148 | nextEquals v []      = expected NoBounds v ""
149 |
150 | --------------------------------------------------------------------------------
151 | --          Testing Parsers
152 | --------------------------------------------------------------------------------
153 |
154 | ||| Utility for testing a parses and the error messages it produces
155 | ||| at the REPL.
156 | export
157 | testParse :
158 |      {auto _ : Show a}
159 |   -> {auto _ : Interpolation e}
160 |   -> {auto _ : Interpolation t}
161 |   -> (Origin -> String -> Either (ParseError e) a)
162 |   -> String
163 |   -> IO ()
164 | testParse f s = case f Virtual s of
165 |   Right res => putStrLn "Success: \{show res}"
166 |   Left err  => putStrLn $ interpolate err
167 |