max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/syntax): improve syntax.get_pos for more error positions

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-22 10:27:15 +01:00
parent 099354eb5f
commit 9f90dbfd3d
2 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/lean/parser/syntax.lean
View file

@ -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,

2
tests/lean/parser1.lean.expected.out
View file

@ -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 ?
<stdin>:1:0: error: unknown declaration 'sorry_ax'
<stdin>:10:0: error: unknown declaration 'sorry_ax'
<stdin>:1:0: parser cache hit rate: 169/196
<stdin>:1:0: parser cache hit rate: 67/78
parser1.lean:102:0: warning: using 'exit' to interrupt Lean