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

refactor: use quotations & implicit token positions from getRef to clean up a bit

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-21 17:31:04 +01:00
parent 856559a983
commit cf73233dd2
4 changed files with 55 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Meta.lean
View file

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

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

@ -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) #[]

63
src/Lean/Elab/MutualDef.lean
View file

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

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

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