@@ -1,192 +1,276 @@
1−Elaborator Reflection - Identity Example
2−========================================
1+Parser
2+======
33
4−.. list-table::
4+On the previous page we implemented a lexer to lex a very simple expression, on this
5+page we will go on to implement a parser for it.
56
6− * - This example of elaborator reflection steps through this metaprogram that generates the identity function:
7− - .. code-block:: idris
7+To run our parser we call 'doParse'. This requires the output from the lexer (a list of tokens) and a Grammar.
88
9− %language ElabReflection
9+.. code-block:: idris
1010
11− idNat : Nat -> Nat
12− idNat = %runElab (do intro `{{x}}
13− fill (Var `{{x}})
14− solve)
11+ doParse : {c : Bool} ->
12+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
13+ ParseResult xs c ty
1514
16−.. list-table::
17− :widths: 200 100
15+So we need to define the Grammar for our parser
1816
19− * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
17+.. code-block:: idris
2018
21− As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body.
22− - .. image:: ../image/tree.png
23− :width: 119px
24− :height: 109px
19+ ||| Description of a language's grammar. The `tok` parameter is the type
20+ ||| of tokens, and the `consumes` flag is True if the language is guaranteed
21+ ||| to be non-empty - that is, successfully parsing the language is guaranteed
22+ ||| to consume some input.
23+ public export
24+ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
25+ Empty : (val : ty) -> Grammar tok False ty
26+ Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
27+ NextIs : String -> (tok -> Bool) -> Grammar tok False tok
28+ EOF : Grammar tok False ()
2529
26−The following is a walkthough looking at the state after each tactic:
30+ Fail : Bool -> String -> Grammar tok c ty
31+ Commit : Grammar tok False ()
32+ MustWork : Grammar tok c a -> Grammar tok c a
2733
28−.. list-table::
34+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
35+ Grammar tok True b
36+ SeqEmpty : {c1, c2 : Bool} ->
37+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
38+ Grammar tok (c1 || c2) b
39+ Alt : {c1, c2 : Bool} ->
40+ Grammar tok c1 ty -> Grammar tok c2 ty ->
41+ Grammar tok (c1 && c2) ty
2942
30− * - Start with the type signature like this:
31− - .. code-block:: idris
43+.. code-block:: idris
3244
33− %language ElabReflection
45+ -- from Idris2/src/Parser/Support.idr
46+ public export
47+ Rule : Type -> Type
48+ Rule ty = Grammar (TokenData ExpressionToken) True ty
3449
35− idNat : Nat -> Nat
36− idNat = %runElab (do
50+.. code-block:: idris
3751
38− * - In order to investigate how the program works this table shows the proof state at each stage as the tactics are applied. So here is the proof state at the start:
39− - .. image:: ../image/elabProofStateEx1_1.png
40− :width: 310px
41− :height: 115px
52+ export
53+ intLiteral : Rule Integer
54+ intLiteral
55+ = terminal --"Expected integer literal"
56+ (\x => case tok x of
57+ Number i => Just i
58+ _ => Nothing)
59+
60+In order to try this out, here is a temporary function, this calls
61+parse which takes two parameters:
62+* The grammar (in this case intLiteral)
63+* The token list from the lexer.
64+
65+.. code-block:: idris
66+
67+ test1 : String -> Either (ParseError (TokenData ExpressionToken))
68+ (Integer, List (TokenData ExpressionToken))
69+ test1 s = parse intLiteral (fst (lex expressionTokens s))
70+
71+As required, if we pass it a string which is a number literal then it will return the
72+number in the 'Right' option.
73+
74+.. code-block:: idris
75+
76+ *parserEx> test1 "123"
77+ Right (123, []) : Either (ParseError (TokenData ExpressionToken))
78+ (Integer, List (TokenData ExpressionToken))
79+
80+If we pass it a string which is not a number literal then it will return an
81+error message.
82+
83+.. code-block:: idris
84+
85+ *parserEx> test1 "a"
86+ Left (Error "End of input"
87+ []) : Either (ParseError (TokenData ExpressionToken))
88+ (Integer, List (TokenData ExpressionToken))
89+
90+If we pass it a number followed by something else, then it will still be
91+successful, this is because we are not specifically checking for end-of-file.
92+
93+.. code-block:: idris
94+
95+ *parserEx> test1 "123a"
96+ Right (123, []) : Either (ParseError (TokenData ExpressionToken))
97+ (Integer, List (TokenData ExpressionToken))
98+ *parserEx>
99+
100+.. code-block:: idris
101+
102+ ||| Succeeds if running the predicate on the next token returns Just x,
103+ ||| returning x. Otherwise fails.
104+ export
105+ terminal : (tok -> Maybe a) -> Grammar tok True a
106+ terminal = Terminal
107+
108+.. code-block:: idris
109+
110+ openParen : Rule Integer
111+ openParen = terminal (\x => case tok x of
112+ OParen => Just 0
113+ _ => Nothing)
114+
115+.. code-block:: idris
116+
117+ test2 : String -> Either (ParseError (TokenData ExpressionToken))
118+ (Integer, List (TokenData ExpressionToken))
119+ test2 s = parse openParen (fst (lex expressionTokens s))
120+
121+.. code-block:: idris
122+
123+ *parserEx> test2 "("
124+ Right (0, []) : Either (ParseError (TokenData ExpressionToken))
125+ (Integer, List (TokenData ExpressionToken))
126+ *parserEx> test2 "123"
127+ Left (Error "Unrecognised token"
128+ [MkToken 0
129+ 0
130+ (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
131+ (Integer,
132+ List (TokenData ExpressionToken))
133+ *parserEx>
134+
135+.. code-block:: idris
136+
137+ test3 : String -> Either (ParseError (TokenData ExpressionToken))
138+ (Integer, List (TokenData ExpressionToken))
139+ test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
140+
141+.. code-block:: idris
142+
143+ *parserEx> test3 "(123"
144+ Right (0, []) : Either (ParseError (TokenData ExpressionToken))
145+ (Integer, List (TokenData ExpressionToken))
146+ *parserEx> test3 "(("
147+ Left (Error "Unrecognised token"
148+ [MkToken 0
149+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
150+ "(" of
151+ (incol, "") => c + cast (length incol)
152+ (incol, b) => cast (length incol))
153+ OParen]) : Either (ParseError (TokenData ExpressionToken))
154+ (Integer, List (TokenData ExpressionToken))
155+
156+ *parserEx> test3 "123"
157+ Left (Error "Unrecognised token"
158+ [MkToken 0
159+ 0
160+ (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
161+ (Integer,
162+ List (TokenData ExpressionToken))
163+ *parserEx> test3 "123("
164+ Left (Error "Unrecognised token"
165+ [MkToken 0 0 (Number 123),
166+ MkToken 0
167+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
168+ "321" of
169+ (incol, "") => c + cast (length incol)
170+ (incol, b) => cast (length incol))
171+ OParen]) : Either (ParseError (TokenData ExpressionToken))
172+ (Integer, List (TokenData ExpressionToken))
173+ *parserEx>
174+
175+.. code-block:: idris
176+
177+ closeParen : Rule Integer
178+ closeParen = terminal (\x => case tok x of
179+ CParen => Just 0
180+ _ => Nothing)
181+
182+.. code-block:: idris
183+
184+ ||| Matches if this is an operator token and string matches, that is,
185+ ||| it is the required type of operator.
186+ op : String -> Rule Integer
187+ op s = terminal (\x => case tok x of
188+ (Operator s1) => if s==s1 then Just 0 else Nothing
189+ _ => Nothing)
190+
191+.. code-block:: idris
192+
193+ paren : Rule Integer -> Rule Integer
194+ paren exp = openParen *> exp <* closeParen
195+
196+.. code-block:: idris
197+
198+ addInt : Integer -> Integer -> Integer
199+ addInt a b = a+b
200+
201+ export
202+ add : Grammar tok c1 Integer ->
203+ Grammar tok c2 Integer ->
204+ Grammar tok c3 Integer ->
205+ Grammar tok ((c1 || c2) || c3) Integer
206+ add x y z = map addInt (x *> y) <*> z
207+
208+.. code-block:: idris
209+
210+ subInt : Integer -> Integer -> Integer
211+ subInt a b = a-b
212+
213+ export
214+ sub : Grammar tok c1 Integer ->
215+ Grammar tok c2 Integer ->
216+ Grammar tok c3 Integer ->
217+ Grammar tok ((c1 || c2) || c3) Integer
218+ sub x y z = map subInt (x *> y) <*> z
219+
220+
221+ multInt : Integer -> Integer -> Integer
222+ multInt a b = a*b
223+
224+ export
225+ mult : Grammar tok c1 Integer ->
226+ Grammar tok c2 Integer ->
227+ Grammar tok c3 Integer ->
228+ Grammar tok ((c1 || c2) || c3) Integer
229+ mult x y z = map multInt (x *> y) <*> z
230+
231+.. code-block:: idris
232+
233+ partial
234+ expr : Rule Integer
235+ expr = (add (op "+") expr expr)
236+ <|> (sub (op "-") expr expr)
237+ <|> (mult (op "*") expr expr)
238+ <|> intLiteral <|> (paren expr)
239+
240+.. code-block:: idris
241+
242+ *parserEx> parse expr (fst (lex expressionTokens "(1)"))
243+ Right (1, []) : Either (ParseError (TokenData ExpressionToken))
244+ (Integer, List (TokenData ExpressionToken))
245+ *parserEx>
246+
247+.. code-block:: idris
248+
249+ parse : (act : Grammar tok c ty) -> (xs : List tok)
250+
251+ parse intLiteral (fst (lex expressionTokens "1"))
252+
253+.. code-block:: idris
254+
255+ *parserEx> parse expr (fst (lex expressionTokens "1+2"))
256+ Right (1,
257+ [MkToken 0
258+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
259+ (incol, "") => c + cast (length incol)
260+ (incol, b) => cast (length incol))
261+ (Operator "+"),
262+ MkToken 0
263+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
264+ (incol, "") => c + cast (length incol)
265+ (incol, b) => cast (length incol))
266+ (Number 2)]) : Either (ParseError (TokenData ExpressionToken))
267+ (Integer, List (TokenData ExpressionToken))
268+ *parserEx>
42269
43− * - This table shows the hole types and what they depend on. The aim is to illustrate the types by analogy with proofs, as a line with the premises above it and the conclusion below it.
44− - .. image:: ../image/elabLogicEx1_1.png
45− :width: 277px
46− :height: 15px
270+.. code-block:: idris
47271
48− * - The term is:
49− - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
272+ partial
273+ test : String -> Either (ParseError (TokenData ExpressionToken))
274+ (Integer, List (TokenData ExpressionToken))
275+ test s = parse expr (fst (lex expressionTokens s))
50276
51− * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles.
52−
53− - The output of these calls contain structures with TT code. To show the results I hacked this: `my code`_. TT code is not really designed to be readable by humans, all the names are fully expanded, everything has a type down to universes (type of types). This is shown here to illustrate the information available.
54−
55− .. code-block:: idris
56−
57− getEnv=[]
58−
59− getGoal=(hole_2, __pi_arg:(Nat.["Nat", "Prelude"]:{
60− type constructor tag=8 number=0}.Type:U=(20:./Prelude/Nat.idr)->.
61− {name ref{type constructor tag=8 number=0}Nat.["Nat","Prelude"]:
62− Type:U=(20:./Prelude/Nat.idr)
63− })
64− })
65−
66− getHoles=[{hole_2},{hole_0}]
67−
68− * - getGuess
69− - error no guess
70−
71− * - Introduce a lambda binding around the current hole and focus on the body.
72− - intro \`{{x}}
73−
74− * - The state now looks like this:
75− - .. image:: ../image/elabProofStateEx1_2.png
76− :width: 312px
77− :height: 84px
78−
79− * - The hole types now looks like this:
80− - .. image:: ../image/elabLogicEx1_2.png
81− :width: 279px
82− :height: 26px
83−
84− * - The term now looks like this:
85− - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
86−
87− * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
88−
89− - .. code-block:: idris
90−
91− getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:{
92− type constructor tag=8 number=0}).
93− Type:U=(20:./Prelude/Nat.idr)
94− })]
95−
96− getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
97− Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
98− })
99−
100− getHoles=[{hole_2},{hole_0}]
101−
102− * - getGuess
103− - error no guess
104−
105− * - Place a term into a hole, unifying its type
106− - fill (Var \`{{x}})
107−
108− * - The state still looks like this:
109− - .. image:: ../image/elabProofStateEx1_3.png
110− :width: 312px
111− :height: 57px
112−
113− * - The hole types now looks like this:
114− - .. image:: ../image/elabLogicEx1_3.png
115− :width: 290px
116− :height: 26px
117−
118− * - The term now looks like this:
119− - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
120−
121− * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
122−
123− - .. code-block:: idris
124−
125− getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:
126− {type constructor tag=8 number=0}).
127− Type:U=(20:./Prelude/Nat.idr)
128− })]
129−
130− getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
131− Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
132− })
133−
134− getHoles=[{hole_2}, {hole_0}]
135−
136− * - getGuess
137− - .. code-block:: idris
138−
139− {name ref bound x:
140− {name ref{type constructor tag=8 number=0}
141− Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
142− }
143− }
144−
145− * - Substitute a guess into a hole.
146− - solve
147−
148− * - The hole types now looks like this:
149− - .. image:: ../image/elabLogicEx1_4.png
150− :width: 131px
151− :height: 14px
152−
153− * - The term now looks like this:
154− - ?{hole_0} ≈ λ x . x . {hole_0}
155−
156− * - getEnv
157−
158− getGoal
159−
160− getHoles
161−
162− - .. code-block:: idris
163−
164− getEnv=[]
165−
166− getGoal=(hole_0, __pi_arg:(Nat.["Nat", "Prelude"]:{
167− type constructor tag=8 number=0}.
168− Type:U=(20:./Prelude/Nat.idr)
169− ->.{name ref
170− {type constructor tag=8 number=0}
171− Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
172− })
173− })
174−
175− getHoles=[{hole_0}]
176−
177− * - getGuess
178− - .. code-block:: idris
179−
180− x:({λ (Nat.["Nat", "Prelude"]:{
181− type constructor tag=8 number=0}).
182− Type:U=(20:./Prelude/Nat.idr)
183− }.{
184− name ref bound
185− x:{name ref {type constructor tag=8 number=0}
186− Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
187− }
188− })
189− }
190−
191−.. target-notes::
192−.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr