trace_parse/Examples.lean at main · whxvd/trace_parse · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
import TraceParse
open Lean Parser

-- Examples of what `#parse` can do more than `#trace_parse`

-- Info or error with final state when parser succeeds

/--
info: Parser succeeded, had arity 1 and produced:
  x
Parsing ended at input:1:2 and left
  "x"
unparsed.
-/
#guard_msgs (info, drop trace) in
#parse : ident "x x"

/--
error: Parser failed with arity 1 and error:
  expected term
Parsing ended at input:1:0 and left
  ":"
unparsed.
-/
#guard_msgs (error, drop trace) in
#parse ":"

-- Choice between pp, format, and repr for the parse results

/--
info: Parser succeeded, had arity 1 and produced:
  Lean.Syntax.ident (Lean.SourceInfo.none) "x".toRawSubstring `x []
Input was consumed completely.
-/
#guard_msgs (info, drop trace) in
#parse : ident +repr "x"

-- Parsing of arbitraty expressions of type `Parser`

/--
info: Parser succeeded, had arity 2 and produced:
  "a"
  "a"
Input was consumed completely.
-/
#guard_msgs (info, drop trace) in
#parse : ("a" >> "a") +format "a a"

-- Factored-out
--
-- - `Lean.Parser.Parser.traceParse` and
-- - `resolveParser : Ident → CommandElabM Parser`
--
-- for things the `#parse` syntax does not (yet) account for or for custom
-- experiments and exploration.

def myFrequentOmits : List Name := [`token]
/--
info: Parser succeeded, had arity 2 and produced:
  x
  x
Parsing ended at input:1:4 and left
  "x"
unparsed.
---
trace: [debug] Syntax: `x
[debug] Syntax: `x
-/
#guard_msgs in
run_cmd (ident >> ident).traceParse "x x x" myFrequentOmits