From 9023e93b3e66ce686f45e2c43582f394b4474f4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Nov 2020 10:31:06 -0800 Subject: [PATCH] refactor: move `Array.set` to `Prelude` --- src/Init/Data/Array/Basic.lean | 10 --------- src/Init/Data/List/Basic.lean | 5 ----- src/Init/Meta.lean | 4 ---- src/Init/Notation.lean | 15 +++++++------- src/Init/Prelude.lean | 34 +++++++++++++++++++++++++++++++ src/Lean/Elab/Tactic/Rewrite.lean | 2 +- src/Lean/Syntax.lean | 17 ++-------------- 7 files changed, 45 insertions(+), 42 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index a333445404..0aa19fa240 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/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 diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 453b3dd72d..eb5201d6eb 100644 --- a/src/Init/Data/List/Basic.lean +++ b/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 diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index c1a60b0723..c060538ac7 100644 --- a/src/Init/Meta.lean +++ b/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) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 12f252491a..1b948172bd 100644 --- a/src/Init/Notation.lean +++ b/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 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 8041380948..04e0cf8781 100644 --- a/src/Init/Prelude.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 8cef19f4a5..b1ca62d072 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/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 diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index cdb3e99ce9..896d46d4b7 100644 --- a/src/Lean/Syntax.lean +++ b/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