From 9f90dbfd3d3583ac888fa8b684e531f33fe9d872 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Jan 2019 10:27:15 +0100 Subject: [PATCH] feat(library/init/lean/parser/syntax): improve `syntax.get_pos` for more error positions --- library/init/lean/parser/syntax.lean | 10 ++++++---- tests/lean/parser1.lean.expected.out | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index 14b1c05484..ebceebd1c1 100644 --- a/library/init/lean/parser/syntax.lean +++ b/library/init/lean/parser/syntax.lean @@ -173,13 +173,15 @@ def update_leading (source : string) : syntax → syntax := λ stx, prod.fst $ (mreplace update_leading_aux stx).run source.mk_iterator /-- Retrieve the left-most leaf's info in the syntax tree. -/ -def get_head_info : syntax → option source_info +mutual def get_head_info, get_head_info_lst +with get_head_info : syntax → option source_info | (atom a) := a.info | (ident id) := id.info --- TODO: handle case where `n` is an empty `syntax_node` --- We will have to create a mutual recursion here Arghhhh -| (raw_node {args:=n::ns, ..}) := n.get_head_info +| (raw_node n) := get_head_info_lst n.args | _ := none +with get_head_info_lst : list syntax → option source_info +| [] := none +| (stx::stxs) := get_head_info stx <|> get_head_info_lst stxs def get_pos (stx : syntax) : option parsec.position := do i ← stx.get_head_info, diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index 9cd39c9559..19474a4763 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -104,7 +104,7 @@ parser1.lean:78:0: error: unknown declaration 'sorry_ax' parser1.lean:1:0: error: don't know how to synthesize placeholder context: ⊢ Sort ? -:1:0: error: unknown declaration 'sorry_ax' +:10:0: error: unknown declaration 'sorry_ax' :1:0: parser cache hit rate: 169/196 :1:0: parser cache hit rate: 67/78 parser1.lean:102:0: warning: using 'exit' to interrupt Lean