refactor: move Array.set to Prelude

src/Init/Data/Array/Basic.lean

@@ -52,11 +52,6 @@ def getD (a : Array α) (i : Nat) (v₀ : α) : α :=
 abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
   a.get ⟨i, h₁.symm ▸ h₂⟩
 
-@[extern "lean_array_fset"]
-def set (a : Array α) (i : @& Fin a.size) (v : α) : Array α := {
-  data := a.data.set i v
-}
-
 theorem sizeSetEq (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
  List.lengthSetEq ..
 
@@ -70,11 +65,6 @@ theorem sizePushEq (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
-/- "Comfortable" version of `fset`. It performs a bound check at runtime. -/
-@[extern "lean_array_set"]
-def set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
-  if h : i < a.size then a.set ⟨i, h⟩ v else panic! "index out of bounds"
-
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let v₁ := a.get i

src/Init/Data/List/Basic.lean

@@ -71,11 +71,6 @@ def isEmpty : List α → Bool
   | []     => true
   | _ :: _ => false
 
-def set : List α → Nat → α → List α
-  | a::as, 0,   b => b::as
-  | a::as, n+1, b => a::(set as n b)
-  | [],    _,   _ => []
-
 @[specialize] def map (f : α → β) : List α → List β
   | []    => []
   | a::as => f a :: map f as

src/Init/Meta.lean

@@ -231,10 +231,6 @@ def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
 def mkCIdent (c : Name) : Syntax :=
   mkCIdentFrom Syntax.missing c
 
-def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
-  let info := src.getHeadInfo.getD {}
-  Syntax.atom info val
-
 def Syntax.identToAtom (stx : Syntax) : Syntax :=
   match stx with
   | Syntax.ident info _ val _ => Syntax.atom info (toString val.eraseMacroScopes)

src/Init/Notation.lean

@@ -144,14 +144,15 @@ syntax[rewrite] "rewrite " rwRule (location)? : tactic
 syntax[rewriteSeq, 1] "rewrite " rwRuleSeq (location)? : tactic
 
 syntax[rw] "rw " rwRule (location)? : tactic
-macro_rules
-  | `(tactic| rw $rule:rwRule) => `(tactic| rewrite $rule:rwRule)
-  | `(tactic| rw $rule:rwRule $loc:location) => `(tactic| rewrite $rule:rwRule $loc:location)
-
 syntax[rwSeq, 1] "rw " rwRuleSeq (location)? : tactic
-macro_rules
-  | `(tactic| rw $rule:rwRuleSeq) => `(tactic| rewrite $rule:rwRuleSeq)
-  | `(tactic| rw $rule:rwRuleSeq $loc:location) => `(tactic| rewrite $rule:rwRuleSeq $loc:location)
+
+@[macro rw]
+def expandRw : Macro :=
+  fun stx => return stx.setKind `Lean.Parser.Tactic.rewrite |>.setArg 0 (mkAtomFrom stx "rewrite")
+
+@[macro rwSeq]
+def expandRwSeq : Macro :=
+  fun stx => return stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite")
 
 syntax:2[orelse] tactic "<|>" tactic:1 : tactic
 

src/Init/Prelude.lean

@@ -873,6 +873,11 @@ def List.foldl {α β} (f : α → β → α) : (init : α) → List β → α
   | a, nil      => a
   | a, cons b l => foldl f (f a b) l
 
+def List.set : List α → Nat → α → List α
+  | cons a as, 0,          b => cons b as
+  | cons a as, Nat.succ n, b => cons a (set as n b)
+  | nil,       _,          _ => nil
+
 def List.lengthAux {α : Type u} : List α → Nat → Nat
   | nil,       n => n
   | cons a as, n => lengthAux as (Nat.succ n)
@@ -991,6 +996,15 @@ def Array.push {α : Type u} (a : Array α) (v : α) : Array α := {
   data := List.concat a.data v
 }
 
+@[extern "lean_array_fset"]
+def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α := {
+  data := a.data.set i.val v
+}
+
+@[extern "lean_array_set"]
+def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
+  dite (Less i a.size) (fun h => a.set ⟨i, h⟩ v) (fun _ => @panic _ ⟨a⟩ "index out of bounds at 'Array.set!'")
+
 -- Slower `Array.append` used in quotations.
 protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
   let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=
@@ -1538,6 +1552,21 @@ def getArgs (stx : Syntax) : Array Syntax :=
   | Syntax.node _ args => args
   | _                  => Array.empty
 
+def getNumArgs (stx : Syntax) : Nat :=
+  match stx with
+  | Syntax.node _ args => args.size
+  | _                  => 0
+
+def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
+  match stx with
+  | node k _ => node k args
+  | stx      => stx
+
+def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
+  match stx with
+  | node k args => node k (args.set! i arg)
+  | stx         => stx
+
 /-- Retrieve the left-most leaf's info in the Syntax tree. -/
 partial def getHeadInfo : Syntax → Option SourceInfo
   | atom info _      => some info
@@ -1559,6 +1588,11 @@ def getPos (stx : Syntax) : Option String.Pos :=
 
 end Syntax
 
+def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
+  match src.getHeadInfo with
+  | some info => Syntax.atom info val
+  | none      => Syntax.atom {} val
+
 /- Parser descriptions -/
 
 inductive ParserDescr where

src/Lean/Elab/Tactic/Rewrite.lean

@@ -14,7 +14,7 @@ open Meta
 @[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro := fun stx =>
   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]
+  return 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
   let (g, gs) ← getMainGoal

src/Lean/Syntax.lean

@@ -97,32 +97,19 @@ def asNode : Syntax → SyntaxNode
   | Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩
   | _                     => ⟨Syntax.node nullKind #[], IsNode.mk nullKind #[]⟩
 
-def getNumArgs (stx : Syntax) : Nat :=
-  stx.asNode.getNumArgs
-
-def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
-  match stx with
-  | node k _ => node k args
-  | stx      => stx
+def getIdAt (stx : Syntax) (i : Nat) : Name :=
+  (stx.getArg i).getId
 
 @[inline] def modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) : Syntax :=
   match stx with
   | node k args => node k (fn args)
   | stx         => stx
 
-def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
-  match stx with
-  | node k args => node k (args.set! i arg)
-  | stx         => stx
-
 @[inline] def modifyArg (stx : Syntax) (i : Nat) (fn : Syntax → Syntax) : Syntax :=
   match stx with
   | node k args => node k (args.modify i fn)
   | stx         => stx
 
-def getIdAt (stx : Syntax) (i : Nat) : Name :=
-  (stx.getArg i).getId
-
 @[specialize] partial def replaceM {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m (Syntax)
   | stx@(node kind args) => do
     match (← fn stx) with