From 7535c12bc53ec0a30fabe5f9c34e68cd3084cf47 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Sep 2022 09:08:06 -0700
Subject: [PATCH] test: add frontend meeting examples to test suite

---
 .../lean/run/frontend_meeting_2022_09_13.lean | 107 ++++++++++++++++++
 1 file changed, 107 insertions(+)
 create mode 100644 tests/lean/run/frontend_meeting_2022_09_13.lean

diff --git a/tests/lean/run/frontend_meeting_2022_09_13.lean b/tests/lean/run/frontend_meeting_2022_09_13.lean
new file mode 100644
index 0000000000..15be176891
--- /dev/null
+++ b/tests/lean/run/frontend_meeting_2022_09_13.lean
@@ -0,0 +1,107 @@
+import Lean
+
+/-
+(1) How are the source information, comments etc stored in the Syntax tree? In particular, how can one recreate the original source?
+-/
+
+elab "#reprint" e:term : command => do
+  let some val := e.raw.reprint | throwError "failed to reprint"
+  IO.println val
+
+#reprint
+  let x : Nat := 3 -- My comment 1
+  x + 2 /- another comment here -/
+
+elab "#repr" e:term : command => do
+  IO.println (repr e)
+
+#check Lean.SourceInfo
+
+#repr
+  let x : Nat := 3 -- My comment 1
+  x + 2 /- another comment here -/
+
+/-
+(2) I am comfortable with the usual token level parsers but could not understand the code for `commentBody` and such parsers. How does one parse at character level?
+
+-/
+
+section
+open Lean Parser
+partial def commandCommentBodyFn (c : ParserContext) (s : ParserState) : ParserState :=
+  go s
+where
+  go (s : ParserState) : ParserState := Id.run do
+    let input := c.input
+    let i     := s.pos
+    if input.atEnd i then return s.mkUnexpectedError "unterminated command comment"
+    let curr := input.get i
+    let i    := input.next i
+    if curr != '-' then return go (s.setPos i)
+    let curr := input.get i
+    let i    := input.next i
+    if curr != '/' then return go (s.setPos i)
+    let curr := input.get i
+    let i    := input.next i
+    if curr != '/' then return go (s.setPos i)
+    -- Found '-//'
+    return s.setPos i
+
+def commandCommentBody : Parser :=
+  { fn := rawFn commandCommentBodyFn (trailingWs := true) }
+
+@[combinatorParenthesizer commandCommentBody] def commandCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+@[combinatorFormatter commandCommentBody] def commandCommentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
+
+@[commandParser] def commandComment := leading_parser "//-" >> commandCommentBody >> ppLine
+
+end
+
+open Lean Elab Command in
+@[commandElab commandComment] def elabCommandComment : CommandElab := fun stx => do
+   let .atom _ val := stx[1] | return ()
+   let str := val.extract 0 (val.endPos - ⟨3⟩)
+   IO.println s!"str := {repr str}"
+
+//- My command comment hello world -//
+
+/-
+(3) How does one split a `tacticSeq` into individual tactics, with the goal of running them one by one logging state along the way?
+-/
+section
+open Lean Parser Elab Tactic
+
+def getTactics (s : TSyntax ``tacticSeq) : Array Syntax :=
+  match s with
+  | `(tacticSeq| { $[$t:tactic $[;]?]* }) => t
+  | `(tacticSeq| $[$t:tactic $[;]?]*) => t
+  | _ => #[]
+
+elab "seq" s:tacticSeq : tactic => do
+  -- IO.println s
+  let tacs := getTactics s
+  for tac in tacs do
+    let gs ← getUnsolvedGoals
+    withRef tac <| Meta.withPPForTacticGoal <| addRawTrace (goalsToMessageData gs)
+    evalTactic tac
+
+example (h : x = y) : 0 + x = y := by
+  seq rw [h]; rw [Nat.zero_add]
+  done
+
+example (h : x = y) : 0 + x = y := by
+  seq rw [h]
+      rw [Nat.zero_add]
+  done
+
+example (h : x = y) : 0 + x = y := by
+  seq { rw [h]; rw [Nat.zero_add] }
+  done
+
+end
+
+/-
+(4) Related to the above, how does one parse and run all the commands in a file updating the environment, with modifications to the running in some cases (specifically when running a `tacticSeq` log state at each step)?
+-/
+
+#check Lean.Elab.runFrontend