max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/syntax): add and test reprinter

Browse source
This commit is contained in:
Sebastian Ullrich 2018-07-06 16:00:12 +02:00
parent b2f9b2c180
commit 6fa4e56fbe
2 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/init/lean/parser/syntax.lean
View file

@ -87,6 +87,20 @@ with to_format : syntax → format
with to_format_lst : list syntax → list format
| [] := []
| (s::ss) := to_format s :: to_format_lst ss
def reprint_with_info : option source_info → string → string
| (some info) inner := info.leading.to_string ++ inner ++ info.trailing.to_string
| none inner := inner
mutual def reprint, reprint_lst
with reprint : syntax → string
| (ident id) := reprint_with_info id.info id.name.to_string
| (atom ⟨info, atomic_val.string s⟩) := reprint_with_info info s
| (atom ⟨info, atomic_val.name n⟩) := reprint_with_info info n.to_string
| (node n) := reprint_lst n.args
with reprint_lst : list syntax → string
| [] := ""
| (s::ss) := reprint s ++ reprint_lst ss
end syntax
instance : has_to_format syntax := ⟨syntax.to_format⟩

5
tests/lean/reader1.lean
View file

@ -4,7 +4,10 @@ open lean.parser.reader
def show_result (p : lean.parser.reader) (s : string) : io unit :=
match p.parse ⟨⟩ s with
| except.ok a := io.print_ln "result: " >> io.print_ln (to_string a)
| except.ok stx := do
guard $ stx.reprint = s,
io.print_ln "result: ",
io.print_ln (to_string stx)
| except.error e := io.print_ln (e.to_string s)
#eval show_result module.reader "prelude"