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

fix: position information for implicit type

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-26 08:07:16 -07:00
parent 1ede4843e3
commit efa5db197e
4 changed files with 22 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Elab/Binders.lean
View file

@ -107,25 +107,24 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
if k == ``Lean.Parser.Term.simpleBinder then
-- binderIdent+ >> optType
let ids ← getBinderIds stx[0]
let type := expandOptType (mkNullNode ids) stx[1]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
let optType := stx[1]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandOptType id optType, bi := BinderInfo.default }
else if k == ``Lean.Parser.Term.explicitBinder then
-- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
let ids ← getBinderIds stx[1]
let type := expandBinderType (mkNullNode ids) stx[2]
let type := stx[2]
let optModifier := stx[3]
let type ← expandBinderModifier type optModifier
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := BinderInfo.default }
else if k == ``Lean.Parser.Term.implicitBinder then
-- `{` binderIdent+ binderType `}`
let ids ← getBinderIds stx[1]
let type := expandBinderType (mkNullNode ids) stx[2]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.implicit }
let type := stx[2]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.implicit }
else if k == ``Lean.Parser.Term.strictImplicitBinder then
-- `⦃` binderIdent+ binderType `⦄`
let ids ← getBinderIds stx[1]
let type := expandBinderType (mkNullNode ids) stx[2]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.strictImplicit }
let type := stx[2]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.strictImplicit }
else if k == ``Lean.Parser.Term.instBinder then
-- `[` optIdent type `]`
let id ← expandOptIdent stx[1]

4
tests/lean/holes.lean.expected.out
View file

@ -20,7 +20,7 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
context:
x : Nat
⊢ Type
holes.lean:13:8-13:11: error: failed to infer binder type
holes.lean:13:10-13:11: error: failed to infer binder type
holes.lean:15:16-15:17: error: failed to infer binder type
holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
@f Nat (?m _) a
@ -28,6 +28,6 @@ context:
a : Nat
f : {α : Type} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a
⊢ ?m a (α := Nat)
holes.lean:18:7-18:10: error: failed to infer binder type
holes.lean:18:9-18:10: error: failed to infer binder type
holes.lean:21:25-22:4: error: failed to infer definition type
holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

7
tests/lean/implicitTypePos.lean Normal file
View file

@ -0,0 +1,7 @@
def f x y := 0
def g (x y z) := 0 + x + z
def h {α β} (a : α) := a
def r {{α β}} (a : α) := a

5
tests/lean/implicitTypePos.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
implicitTypePos.lean:7:10-7:11: error: failed to infer binder type