From 6fa4e56fbed719ac32a258c5a11aa0251630a0bb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 6 Jul 2018 16:00:12 +0200
Subject: [PATCH] feat(library/init/lean/parser/syntax): add and test reprinter

---
 library/init/lean/parser/syntax.lean | 14 ++++++++++++++
 tests/lean/reader1.lean              |  5 ++++-
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
index 08078a97a8..f7fee98535 100644
--- a/library/init/lean/parser/syntax.lean
+++ b/library/init/lean/parser/syntax.lean
@@ -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⟩
diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean
index 6fd6b7f1dc..121fc400c5 100644
--- a/tests/lean/reader1.lean
+++ b/tests/lean/reader1.lean
@@ -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"