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

feat: adapt elaborator to preceding change

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-27 15:22:54 +01:00
parent ada5e76f03
commit 78a8bc7b7e
2 changed files with 7 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -401,14 +401,8 @@ def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := fals
def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltNumPatterns matchAlts) #[]
@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => do
-- "fun " >> ((many1 funBinder >> darrow >> termParser) <|> matchAlts)
if stx[1].isOfKind `Lean.Parser.Term.matchAlts then
let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx stx[1]
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
else
let binders := stx[1].getArgs
let body := stx[3]
@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match_syntax stx with
| `(fun $binders* => $body) => do
let (binders, body, expandedPattern) ← expandFunBinders binders body
if expandedPattern then
let newStx ← `(fun $binders* => $body)
@ -420,6 +414,10 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
and another instance for the dependent version. -/
let e ← elabTermEnsuringType body expectedType?
mkLambdaFVars xs e
| `(fun $m:matchAlts) => do
let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| _ => throwUnsupportedSyntax
/- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
Otherwise, we create a term of the form `(fun (x : type) => body) val`

2
src/Lean/Parser/Term.lean
View file

@ -141,7 +141,7 @@ def funImplicitBinder := «try» (lookahead ("{" >> many1 binderIdent >> (" : "
def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
-- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (checkInsideQuot >> basicFun <|> checkOutsideQuot >> (many1 (ppSpace >> funBinder) >> darrow >> termParser) <|> matchAlts false)
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false)
def optExprPrecedence := optional («try» ":" >> termParser maxPrec)
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser