chore(tests/playground/parser): missing files and small issues

tests/playground/parser/Makefile

@@ -1,6 +1,6 @@
 LEANC=../../../bin/leanc
 LEAN=../../../bin/lean
-COMMON_SRCS = parser.lean syntax.lean
+COMMON_SRCS = parser.lean syntax.lean filemap.lean
 SRCS = $(COMMON_SRCS) test1.lean test2.lean
 OLEANS = $(SRCS:.lean=.olean)
 CPPS = $(SRCS:.lean=.cpp)
@@ -29,10 +29,10 @@ depends: $(DEPS)
 	$(LEANC) -c $(CPPFLAGS) -o $@ $<
 
 test1: test1.o $(COMMON_OBJS)
-	$(LEANC) -o $@ $?
+	$(LEANC) -o $@ $^
 
 test2: test2.o $(COMMON_OBJS)
-	$(LEANC) -o $@ $?
+	$(LEANC) -o $@ $^
 
 clean:
 	rm -f *.olean

tests/playground/parser/filemap.lean

@@ -0,0 +1,53 @@
+structure Position :=
+(line   : Nat := 1)
+(column : Nat := 0)
+
+instance : Inhabited Position :=
+⟨{}⟩
+
+structure FileMap :=
+(source    : String)
+(positions : Array String.Pos)
+(lines     : Array Nat)
+
+namespace FileMap
+
+instance : Inhabited FileMap :=
+⟨{ source := "", positions := Array.empty, lines := Array.empty }⟩
+
+private partial def ofStringAux (s : String) : String.Pos → Nat → Array String.Pos → Array Nat → FileMap
+| i line ps lines :=
+  if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }
+  else
+    let c := s.get i in
+    let i := s.next i in
+    if c == '\n' then ofStringAux i (line+1) (ps.push i) (lines.push (line+1))
+    else ofStringAux i line ps lines
+
+def ofString (s : String) : FileMap :=
+ofStringAux s 0 1 (Array.empty.push 0) (Array.empty.push 1)
+
+private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos : String.Pos) : String.Pos → Nat → Nat
+| i c :=
+  if i == pos || str.atEnd i then c
+  else toColumnAux (str.next i) (c+1)
+
+/- Remark: `pos` is in `[ps.get b, ps.get e]` and `b < e` -/
+private partial def toPositionAux (str : String) (ps : Array Nat) (lines : Array Nat) (pos : String.Pos) : Nat → Nat → Position
+| b e :=
+  let posB := ps.get b in
+  if e == b + 1 then { line := lines.get b, column := toColumnAux str posB pos posB 0 }
+  else
+    let m := (b + e) / 2 in
+    let posM := ps.get m in
+    if pos == posM then { line := lines.get m, column := 0 }
+    else if pos > posM then toPositionAux m e
+    else toPositionAux b m
+
+def toPosition : FileMap → String.Pos → Position
+| { source := str, positions := ps, lines := lines } pos := toPositionAux str ps lines pos 0 (ps.size-1)
+
+end FileMap
+
+def String.toFileMap (s : String) : FileMap :=
+FileMap.ofString s

tests/playground/parser/syntax.lean

@@ -143,6 +143,10 @@ def MacroScopes.flip : MacroScopes → MacroScopes → MacroScopes
   | []    := [x]
 
 namespace Syntax
+def isOfKind : Syntax → SyntaxNodeKind → Bool
+| (Syntax.node kind _ _) k := k == kind
+| other                  _ := false
+
 def flipScopes (scopes : MacroScopes) : Syntax → Syntax
 | (Syntax.ident info rawVal val pre scopes) := Syntax.ident info rawVal val pre (scopes.flip scopes)
 | (Syntax.node kind args scopes)            := Syntax.node kind args (scopes.flip scopes)
@@ -161,8 +165,8 @@ local attribute [instance] monadInhabited
 @[inline] def replace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) := @mreplace Id _
 
 private def updateInfo : SourceInfo → String.Pos → SourceInfo
-| {leading := {str := s, startPos := sPos, endPos := ePos}, pos := pos, trailing := trailing} last :=
-  {leading := {str := s, startPos := last, endPos := pos}, pos := pos, trailing := trailing}
+| {leading := {str := s, startPos := _, stopPos := _}, pos := pos, trailing := trailing} last :=
+  {leading := {str := s, startPos := last, stopPos := pos}, pos := pos, trailing := trailing}
 
 /- Remark: the State `String.Pos` is the `SourceInfo.trailing.endPos` of the previous token,
    or the beginning of the String. -/
@@ -170,12 +174,12 @@ private def updateInfo : SourceInfo → String.Pos → SourceInfo
 private def updateLeadingAux : Syntax → State String.Pos (Option Syntax)
 | (atom (some info) val) := do
   last ← get,
-  set info.trailing.endPos,
+  set info.trailing.stopPos,
   let newInfo := updateInfo info last in
   pure $ some (atom (some newInfo) val)
 | (ident (some info) rawVal val pre scopes) := do
   last ← get,
-  set info.trailing.endPos,
+  set info.trailing.stopPos,
   let newInfo := updateInfo info last in
   pure $ some (ident (some newInfo) rawVal val pre scopes)
 | _ := pure none