From c1dccb8154734309ffe90e67ba6779d216cb611a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2020 15:48:39 -0700 Subject: [PATCH] feat: `stx[i]` as notation for `stx.getArg i` --- src/Init/LeanInit.lean | 4 ++++ src/Lean/Elab/Tactic/Basic.lean | 16 ++++++++-------- src/Lean/Elab/Tactic/Binders.lean | 2 +- src/Lean/Elab/Tactic/Generalize.lean | 8 ++++---- src/Lean/Elab/Tactic/Induction.lean | 26 +++++++++++++------------- src/Lean/Elab/Tactic/Injection.lean | 6 +++--- src/Lean/Elab/Tactic/Location.lean | 6 +++--- src/Lean/Elab/Tactic/Match.lean | 8 ++++---- src/Lean/Elab/Tactic/Rewrite.lean | 12 ++++++------ 9 files changed, 46 insertions(+), 42 deletions(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 3cc1a1b422..74e1f7adf9 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -248,6 +248,10 @@ match stx with | Syntax.node _ args => args.get! i | _ => Syntax.missing -- panic! "Syntax.getArg: not a node" +-- Add `stx[i]` as sugar for `stx.getArg i` +@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax := +self.getArg idx + def getArgs (stx : Syntax) : Array Syntax := match stx with | Syntax.node _ args => args diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index f7381ca0ed..a8e7afe846 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -249,22 +249,22 @@ modifyMCtx fun mctx => do pure mctx @[builtinTactic seq1] def evalSeq1 : Tactic := -fun stx => (stx.getArg 0).forSepArgsM evalTactic +fun stx => stx[0].forSepArgsM evalTactic @[builtinTactic paren] def evalParen : Tactic := -fun stx => evalSeq1 (stx.getArg 1) +fun stx => evalSeq1 stx[1] @[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := -fun stx => stx.getArg 0 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0) +fun stx => stx[0].forArgsM fun seqElem => evalTactic seqElem[0] @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := -fun stx => withRef (stx.getArg 2) $ focus $ stx.getArg 1 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0) +fun stx => withRef stx[2] $ focus $ stx[1].forArgsM fun seqElem => evalTactic seqElem[0] @[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := -fun stx => focus $ evalTactic (stx.getArg 1) +fun stx => focus $ evalTactic stx[1] @[builtinTactic tacticSeq] def evalTacticSeq : Tactic := -fun stx => evalTactic (stx.getArg 0) +fun stx => evalTactic stx[0] partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit | i => @@ -284,7 +284,7 @@ fun stx => pure () @[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do - let tactic := stx.getArg 1 + let tactic := stx[1] if (← do try evalTactic tactic; pure true catch _ => pure false) then throwError "tactic succeeded" @@ -318,7 +318,7 @@ fun stx => match_syntax stx with @[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do - let matchAlts := stx.getArg 1 + let matchAlts := stx[1] let stxNew ← liftMacroM $ Term.expandMatchAltsIntoMatchTactic stx matchAlts withMacroExpansion stx stxNew $ evalTactic stxNew diff --git a/src/Lean/Elab/Tactic/Binders.lean b/src/Lean/Elab/Tactic/Binders.lean index bdad0da0d1..10a779b6a5 100644 --- a/src/Lean/Elab/Tactic/Binders.lean +++ b/src/Lean/Elab/Tactic/Binders.lean @@ -24,7 +24,7 @@ fun stx => do @[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro := fun stx => - let type := stx.getArg 1 + let type := stx[1] `(tactic| refine (show $type from ?_)) end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean index 8745396da1..de79bb1ad2 100644 --- a/src/Lean/Elab/Tactic/Generalize.lean +++ b/src/Lean/Elab/Tactic/Generalize.lean @@ -13,11 +13,11 @@ namespace Lean.Elab.Tactic open Meta private def getAuxHypothesisName (stx : Syntax) : Option Name := -if (stx.getArg 1).isNone then none -else some ((stx.getArg 1).getIdAt 0) +if stx[1].isNone then none +else some stx[1][0].getId private def getVarName (stx : Syntax) : Name := -stx.getIdAt 4 +stx[4].getId private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do let tag ← Meta.getMVarTag mvarId @@ -68,7 +68,7 @@ match h? with fun stx => do let h? := getAuxHypothesisName stx let x := getVarName stx - let e ← elabTerm (stx.getArg 2) none + let e ← elabTerm stx[2] none evalGeneralizeAux h? e x end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 98a7249bc8..05bc249cf3 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -17,13 +17,13 @@ open Meta -- Recall that -- majorPremise := parser! optional (try (ident >> " : ")) >> termParser private def getAuxHypothesisName (stx : Syntax) : Option Name := -if stx.getArg 1 $.getArg 0 $.isNone then +if stx[1][0].isNone then none else - some $ stx.getArg 1 $.getArg 0 $.getIdAt 0 + some stx[1][0][0].getId private def getMajor (stx : Syntax) : Syntax := -stx.getArg 1 $.getArg 1 +stx[1][1] private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do match h? with @@ -57,12 +57,12 @@ match major with `stx` is syntax for `induction`. -/ private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) := withRef stx $ -let generalizingStx := stx.getArg 3 +let generalizingStx := stx[3] if generalizingStx.isNone then pure #[] else withMainMVarContext do trace `Elab.induction fun _ => generalizingStx - let vars := (generalizingStx.getArg 1).getArgs + let vars := generalizingStx[1].getArgs getFVarIds vars -- process `generalizingVars` subterm of induction Syntax `stx`. @@ -75,16 +75,16 @@ liftMetaTacticAux fun mvarId => do pure (fvarIds.size, [mvarId']) private def getAlts (withAlts : Syntax) : Array Syntax := -withAlts.getArg 2 $.getSepArgs +withAlts[2].getSepArgs /- Given an `inductionAlt` of the form ``` nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser ``` -/ -private def getAltName (alt : Syntax) : Name := (alt.getArg 0).getId.eraseMacroScopes -private def getAltVarNames (alt : Syntax) : Array Name := (alt.getArg 1).getArgs.map Syntax.getId -private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3 +private def getAltName (alt : Syntax) : Name := alt[0].getId.eraseMacroScopes +private def getAltVarNames (alt : Syntax) : Array Name := alt[1].getArgs.map Syntax.getId +private def getAltRHS (alt : Syntax) : Syntax := alt[3] /- Given alts of the form @@ -98,7 +98,7 @@ for alt in alts do let n := getAltName alt withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}" unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do - throwErrorAt! (alt.getArg 0) "invalid constructor name '{n}'" + throwErrorAt! alt[0] "invalid constructor name '{n}'" structure RecInfo := (recName : Name) @@ -199,8 +199,8 @@ else ``` -/ private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx do -let usingRecStx := stx.getArg 2 -let withAlts := stx.getArg 4 +let usingRecStx := stx[2] +let withAlts := stx[4] if usingRecStx.isNone then let (rinfo, _) ← getRecInfoDefault major withAlts false pure rinfo @@ -317,7 +317,7 @@ fun stx => focusAux do let major ← elabMajor h? (getMajor stx) let major ← generalizeMajor major let (mvarId, _) ← getMainGoal - let withAlts := stx.getArg 2 + let withAlts := stx[2] let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true let result ← Meta.cases mvarId major.fvarId! recInfo.altVars checkCasesResult result ctorNames recInfo.altRHSs diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean index f901be49a4..cbf17344a9 100644 --- a/src/Lean/Elab/Tactic/Injection.lean +++ b/src/Lean/Elab/Tactic/Injection.lean @@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic -- optional (" with " >> many1 ident') private def getInjectionNewIds (stx : Syntax) : List Name := if stx.isNone then [] -else stx.getArg 1 $.getArgs.toList.map Syntax.getId +else stx[1].getArgs.toList.map Syntax.getId private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := do unless unusedIds.isEmpty do @@ -20,8 +20,8 @@ unless unusedIds.isEmpty do @[builtinTactic «injection»] def evalInjection : Tactic := fun stx => do -- parser! nonReservedSymbol "injection " >> termParser >> withIds - let fvarId ← elabAsFVar (stx.getArg 1) - let ids := getInjectionNewIds (stx.getArg 2) + let fvarId ← elabAsFVar stx[1] + let ids := getInjectionNewIds stx[2] liftMetaTactic fun mvarId => do match ← Meta.injection mvarId fvarId ids (!ids.isEmpty) with | Meta.InjectionResult.solved => checkUnusedIds mvarId ids; pure [] diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean index 693d297e62..f25437d59e 100644 --- a/src/Lean/Elab/Tactic/Location.lean +++ b/src/Lean/Elab/Tactic/Location.lean @@ -21,13 +21,13 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <| ``` -/ def expandLocation (stx : Syntax) : Location := -let arg := stx.getArg 1 +let arg := stx[1] if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target -else Location.localDecls $ arg.getArg 0 $.getArgs.map fun stx => stx.getId +else Location.localDecls $ arg[0].getArgs.map fun stx => stx.getId def expandOptLocation (stx : Syntax) : Location := if stx.isNone then Location.target -else expandLocation $ stx.getArg 0 +else expandLocation stx[0] end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean index 03adc4ff4a..ea0d5b695c 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/src/Lean/Elab/Tactic/Match.lean @@ -15,11 +15,11 @@ structure AuxMatchTermState := (cases : Array Syntax := #[]) private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do -let matchAlts := matchTac.getArg 4 -let alts := matchAlts.getArg 1 $.getArgs +let matchAlts := matchTac[4] +let alts := matchAlts[1].getArgs let newAlts ← alts.mapSepElemsM fun alt => do let alt := alt.updateKind `Lean.Parser.Term.matchAlt - let holeOrTacticSeq := alt.getArg 2 + let holeOrTacticSeq := alt[2] if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then pure alt else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then @@ -30,7 +30,7 @@ let newAlts ← alts.mapSepElemsM fun alt => do pure $ alt.setArg 2 newHole else withFreshMacroScope do let newHole ← `(?rhs) - let newHoleId := newHole.getArg 1 + let newHoleId := newHole[1] let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq ) modify fun s => { s with cases := s.cases.push newCase } pure $ alt.setArg 2 newHole diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index e36db19082..a7b6db7a95 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -14,8 +14,8 @@ open Meta @[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro := fun stx => - let seq := ((stx.getArg 1).getArg 1).getSepArgs - let loc := stx.getArg 2 + let seq := stx[1][1].getSepArgs + let loc := stx[2] pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[mkAtomFrom rwRule "rewrite ", rwRule, loc] def rewriteTarget (stx : Syntax) (symm : Bool) : TacticM Unit := do @@ -59,10 +59,10 @@ def «rewrite» := parser! "rewrite" >> rwRule >> optional location -/ @[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic := fun stx => do - let rule := stx.getArg 1 - let symm := !(rule.getArg 0).isNone - let term := rule.getArg 1 - let loc := expandOptLocation $ stx.getArg 2 + let rule := stx[1] + let symm := !rule[0].isNone + let term := rule[1] + let loc := expandOptLocation stx[2] match loc with | Location.target => rewriteTarget term symm | Location.localDecls userNames => userNames.forM (rewriteLocalDecl term symm)