From cf73233dd24a6f3bed4dc2784dd649ffb453200a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Dec 2020 17:31:04 +0100 Subject: [PATCH] refactor: use quotations & implicit token positions from `getRef` to clean up a bit --- src/Init/Meta.lean | 4 +++ src/Lean/Elab/Binders.lean | 65 +++++++++++------------------------- src/Lean/Elab/MutualDef.lean | 63 +++++++++++++--------------------- src/Lean/Parser/Term.lean | 14 ++++---- 4 files changed, 55 insertions(+), 91 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index a5e9d492dc..cf38df5d3b 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -276,6 +276,10 @@ def mkSep (a : Array Syntax) (sep : Syntax) : Syntax := def SepArray.ofElems {sep} (elems : Array Syntax) : SepArray sep := ⟨mkSepArray elems (mkAtom sep)⟩ +def SepArray.ofElemsUsingRef [Monad m] [MonadRef m] {sep} (elems : Array Syntax) : m (SepArray sep) := do + let ref ← getRef; + return ⟨mkSepArray elems (mkAtomFrom ref sep)⟩ + instance (sep) : Coe (Array Syntax) (SepArray sep) where coe := SepArray.ofElems diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 10abbdabc3..8d1a59a1c8 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -357,52 +357,27 @@ private def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat := let pats := alt0[1].getSepArgs pats.size -private def mkMatch (ref : Syntax) (discrs : Array Syntax) (matchAlts : Syntax) (matchTactic := false) : Syntax := - Syntax.node (if matchTactic then `Lean.Parser.Tactic.match else `Lean.Parser.Term.match) - #[mkAtomFrom ref "match ", mkNullNode discrs, mkNullNode, mkAtomFrom ref " with ", matchAlts] +def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax := + match whereDecls with + | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body) + | _ => unreachable! -private def addDiscr (ref : Syntax) (discrs : Array Syntax) (discrTerm : Syntax) : Array Syntax := - let discrs := if discrs.isEmpty then discrs else discrs.push $ mkAtomFrom ref ", " - discrs.push <| Syntax.node `Lean.Parser.Term.matchDiscr #[mkNullNode, discrTerm] - -/- -Recall that -``` -def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", " -def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser -``` - -The argument `letRecDecls` is an array of syntax terms of the form `(group (optional «attributes» >> letDecl))` --/ -def mkLetRec (ref : Syntax) (letRecDecls : Array Syntax) (body : Syntax) : Syntax := - Syntax.node `Lean.Parser.Term.letrec #[ - mkNullNode #[mkAtomFrom ref "let ", mkAtomFrom ref "rec "], - Syntax.mkSep letRecDecls (mkAtomFrom ref ","), - mkNullNode, -- optional ";" - body - ] - -/- Recall that - ``` - whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";")) - ``` -/ -def expandWhereDecls (ref : Syntax) (whereDecls : Syntax) (body : Syntax) : Syntax := - let letRecDecls := whereDecls[1].getArgs.map fun stx => mkNullNode #[stx[0], stx[1]] -- drop (optional ";") - return mkLetRec ref letRecDecls body - -def expandWhereDeclsOpt (ref : Syntax) (whereDeclsOpt : Syntax) (body : Syntax) : Syntax := +def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax := if whereDeclsOpt.isNone then body else - expandWhereDecls ref whereDeclsOpt[0] body + expandWhereDecls whereDeclsOpt[0] body /- Helper function for `expandMatchAltsIntoMatch` -/ -private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (matchTactic : Bool) : Nat → Array Syntax → MacroM Syntax - | 0, discrs => - return mkMatch ref discrs matchAlts matchTactic +private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (matchTactic : Bool) : Nat → Array Syntax → MacroM Syntax + | 0, discrs => do + if matchTactic then + `(tactic|match $[$discrs:term],* with $matchAlts:matchAlts) + else + `(match $[$discrs:term],* with $matchAlts:matchAlts) | n+1, discrs => withFreshMacroScope do let x ← `(x) - let body ← expandMatchAltsIntoMatchAux ref matchAlts matchTactic n (addDiscr ref discrs x) + let body ← expandMatchAltsIntoMatchAux matchAlts matchTactic n (discrs.push x) if matchTactic then `(tactic| intro $x:term; $body:tactic) else @@ -431,10 +406,10 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat ``` -/ def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := false) : MacroM Syntax := - expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[] + withRef ref <| expandMatchAltsIntoMatchAux matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[] def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax := - expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltsNumPatterns matchAlts) #[] + withRef ref <| expandMatchAltsIntoMatchAux matchAlts true (getMatchAltsNumPatterns matchAlts) #[] /-- Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause. @@ -464,20 +439,20 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM | i, _ => ... f i + g i ... ``` -/ -def expandMatchAltsWhereDecls (ref : Syntax) (matchAltsWhereDecls : Syntax) : MacroM Syntax := +def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax := let matchAlts := matchAltsWhereDecls[0] let whereDeclsOpt := matchAltsWhereDecls[1] let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax := match i with - | 0 => - let matchStx := mkMatch ref discrs matchAlts + | 0 => do + let matchStx ← `(match $[$discrs:term],* with $matchAlts:matchAlts) if whereDeclsOpt.isNone then return matchStx else - expandWhereDeclsOpt ref whereDeclsOpt matchStx + expandWhereDeclsOpt whereDeclsOpt matchStx | n+1 => withFreshMacroScope do let x ← `(x) - let body ← loop n (addDiscr ref discrs x) + let body ← loop n (discrs.push x) `(@fun $x => $body) loop (getMatchAltsNumPatterns matchAlts) #[] diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 3a62ad9ccc..8d854b1b1a 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -8,8 +8,10 @@ import Lean.Meta.Check import Lean.Elab.Command import Lean.Elab.DefView import Lean.Elab.PreDefinition +import Lean.Parser.Term namespace Lean.Elab +open Lean.Parser.Term /- DefView after elaborating the header. -/ structure DefViewElabHeader where @@ -125,43 +127,24 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) ( k fvars loop 0 #[] -private def expandWhereDeclsAsStructInst (whereDecls : Syntax) : MacroM Syntax := do - /- def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";")) -/ - let letDecls ← whereDecls[1].getArgs.mapM fun stx => do - unless stx[0].isNone do - Macro.throwErrorAt stx "attributes are 'where' elements are currently not supported here" - let mut letDecl := stx[1] - if letDecl[0].isOfKind `Lean.Parser.Term.letPatDecl then - Macro.throwErrorAt stx "patterns are not allowed here" - if letDecl[0].getKind == `Lean.Parser.Term.letEqnsDecl then - letDecl := letDecl.setArg 0 (← expandLetEqnsDecl letDecl[0]) - pure letDecl - let structInstFields ← letDecls.mapM fun letDecl => do - let letIdDecl := letDecl[0] - let fieldId := letIdDecl[0] - let mut val := letIdDecl[4] - let optType := letIdDecl[2] - let binders := letIdDecl[1] - unless optType.isNone do - let type := optType[0][1] - val ← `(($val : $type)) - unless binders.isNone do - let binders := binders.getArgs - val ← `(fun $binders* => $val:term) - val := val.copyInfo letIdDecl - return Syntax.node `Lean.Parser.Term.structInstField #[ - Syntax.node ``Parser.Term.structInstLVal #[fieldId, mkNullNode], mkAtomFrom fieldId ":=", val - ] - let ref := whereDecls - let structInst := Syntax.node `Lean.Parser.Term.structInst #[ - mkAtomFrom ref "{", - mkNullNode, - mkNullNode <| structInstFields.map fun field => mkNullNode #[field, mkNullNode], - mkNullNode, - mkNullNode, - mkAtomFrom ref "}" - ] - return structInst +private def expandWhereDeclsAsStructInst : Macro + | `(whereDecls|where $[$decls:letRecDecl$[;]?]*) => do + let letIdDecls ← decls.mapM fun stx => match stx with + | `(letRecDecl|$attrs:attributes $decl:letDecl) => Macro.throwErrorAt stx "attributes are 'where' elements are currently not supported here" + | `(letRecDecl|$decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here" + | `(letRecDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl + | `(letRecDecl|$decl:letIdDecl) => pure decl + | _ => unreachable! + let structInstFields ← letIdDecls.mapM fun + | stx@`(letIdDecl|$id:ident $[$binders]* $[: $ty?]? := $val) => withRef stx do + let mut val := val + if let some ty := ty? then + val ← `(($val : $ty)) + val ← `(fun $[$binders]* => $val:term) + `(structInstField|$id:ident := $val) + | _ => unreachable! + `({ $[$structInstFields,]* }) + | _ => unreachable! /- Recall that @@ -171,11 +154,11 @@ def declValEqns := parser! Term.matchAltsWhereDecls def declVal := declValSimple <|> declValEqns <|> Term.whereDecls ``` -/ -private def declValToTerm (declVal : Syntax) : MacroM Syntax := +private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do if declVal.isOfKind `Lean.Parser.Command.declValSimple then - return expandWhereDeclsOpt declVal declVal[2] declVal[1] + expandWhereDeclsOpt declVal[2] declVal[1] else if declVal.isOfKind `Lean.Parser.Command.declValEqns then - expandMatchAltsWhereDecls declVal declVal[0] + expandMatchAltsWhereDecls declVal[0] else if declVal.isOfKind `Lean.Parser.Term.whereDecls then expandWhereDeclsAsStructInst declVal else diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index f4bb2d0f20..1c0b16a814 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -140,13 +140,14 @@ def optExprPrecedence := optional (atomic ":" >> termParser maxPrec) @[builtinTermParser] def quotedName := parser! nameLit @[builtinTermParser] def doubleQuotedName := parser! "`" >> checkNoWsBefore >> nameLit -def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binderIdent >> pushNone) +def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" `Lean.Parser.Term.simpleBinder (anonymous := true) + (many1 binderIdent >> pushNone) /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType -def letIdDecl := node `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser -def letPatDecl := node `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser -def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts +def letIdDecl := nodeWithAntiquot "letIdDecl" `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser +def letPatDecl := nodeWithAntiquot "letPatDecl" `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser +def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl` def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)) @[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser @@ -158,12 +159,13 @@ def attrKind := parser! optional («scoped» <|> «local») def attrInstance := ppGroup $ parser! attrKind >> attrParser def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]" -def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", " +def letRecDecl := parser! optional «attributes» >> letDecl +def letRecDecls := sepBy1 letRecDecl ", " @[builtinTermParser] def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser @[runBuiltinParserAttributeHooks] -def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";")) +def whereDecls := parser! "where " >> many1Indent (group (letRecDecl >> optional ";")) @[runBuiltinParserAttributeHooks] def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls