From f95ed029990060794dc522e51629846040bbd006 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Jul 2019 15:11:54 -0700
Subject: [PATCH] feat(library/init/lean/parser/parser): add `withPosition` and
 `checkColGe` parsers

---
 library/init/lean/parser/parser.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index a65caba737..16d73c6a6d 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -745,6 +745,15 @@ let sym := sym.trim;
 @[inline] def symbol {k : ParserKind} (sym : String) (lbp : Nat) : Parser k :=
 symbolAux sym lbp
 
+@[inline] def checkColGeFn (col : Nat) (errorMsg : String) : BasicParserFn :=
+fun c s =>
+  let pos := c.fileMap.toPosition s.pos;
+  if pos.column ≥ col then s
+  else s.mkError errorMsg
+
+@[inline] def checkColGe {k : ParserKind} (col : Nat) (errorMsg : String) : Parser k :=
+{ fn := fun _ => checkColGeFn col errorMsg }
+
 partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
 | j c s :=
   if sym.atEnd j then s
@@ -971,6 +980,12 @@ def anyOfFn {k : ParserKind} : List (Parser k) → ParserFn k
 | [p]     a c s := p.fn a c s
 | (p::ps) a c s := orelseFn p.fn (anyOfFn ps) a c s
 
+@[inline] def withPosition {k : ParserKind} (p : Position → Parser k) : Parser k :=
+{ info := (p { line := 1, column := 0 }).info,
+  fn   := fun a c s =>
+   let pos := c.fileMap.toPosition s.pos;
+   (p pos).fn a c s }
+
 /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
 def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt