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

refactor: add implicitLambda argument

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-08 15:21:32 -08:00
parent f321ad213f
commit 0c4d72c1d5
2 changed files with 9 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/App.lean
View file

@ -918,8 +918,8 @@ private def elabAtom : TermElab := fun stx expectedType? =>
match stx with
| `(@$id:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$id:ident.{$us,*}) => elabAtom stx expectedType?
| `(@($t)) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax
@[builtinTermElab choice] def elabChoice : TermElab := elabAtom

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

@ -1042,15 +1042,12 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
and returned.
The option `catchExPostpone == false` is used to implement `resumeElabTerm`
to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone true stx) (mkTermInfo stx)
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx) (mkTermInfo stx)
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
let e ← elabTerm stx expectedType? catchExPostpone
withRef stx $ ensureHasType expectedType? e errorMsgHeader?
def elabTermWithoutImplicitLambdas (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := do
elabTermAux expectedType? catchExPostpone false stx
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
withRef stx <| ensureHasType expectedType? e errorMsgHeader?
/-- Adapt a syntax transformation to a regular, term-producing elaborator. -/
def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expectedType? => do
@ -1407,12 +1404,12 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
| some msg => do
let refTerm ← elabTerm stx[1] none
let refTermType ← inferType refTerm
elabTermEnsuringType stx[3] refTermType true msg
elabTermEnsuringType stx[3] refTermType (errorMsgHeader? := msg)
@[builtinTermElab ensureExpectedType] def elabEnsureExpectedType : TermElab := fun stx expectedType? =>
match stx[1].isStrLit? with
| none => throwIllFormedSyntax
| some msg => elabTermEnsuringType stx[2] expectedType? true msg
| some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
@[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
let openDecls ← elabOpenDecl stx[1]