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

refactor(library/init/data/array): new name convention for Array functions

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-01 16:46:05 -07:00
parent 411f397654
commit fdab3b90b9
33 changed files with 207 additions and 203 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

102
library/init/data/array/basic.lean
View file

@ -65,7 +65,7 @@ def singleton (v : α) : Array α :=
mkArray 1 v
@[extern c inline "lean_array_fget(#2, #3)"]
def fget (a : @& Array α) (i : @& Fin a.size) : α :=
def get (a : @& Array α) (i : @& Fin a.size) : α :=
a.data i
/- Low-level version of `fget` which is as fast as a C array read.
@ -73,25 +73,25 @@ a.data i
`fget` may be slightly slower than `uget`. -/
@[extern c inline "lean_array_uget(#2, #3)"]
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a.fget ⟨i.toNat, h⟩
a.get ⟨i.toNat, h⟩
/- "Comfortable" version of `fget`. It performs a bound check at runtime. -/
@[extern c inline "lean_array_get(#2, #3, #4)"]
def get [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
if h : i < a.size then a.fget ⟨i, h⟩ else default α
def get! [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
if h : i < a.size then a.get ⟨i, h⟩ else default α
def back [Inhabited α] (a : Array α) : α :=
a.get (a.size - 1)
a.get! (a.size - 1)
def getOpt (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some (a.fget ⟨i, h⟩) else none
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some (a.get ⟨i, h⟩) else none
@[extern c inline "lean_array_fset(#2, #3, #4)"]
def fset (a : Array α) (i : @& Fin a.size) (v : α) : Array α :=
def set (a : Array α) (i : @& Fin a.size) (v : α) : Array α :=
{ sz := a.sz,
data := fun j => if h : i = j then v else a.data j }
theorem szFSetEq (a : Array α) (i : Fin a.size) (v : α) : (fset a i v).size = a.size :=
theorem szFSetEq (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
rfl
theorem szPushEq (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@ -102,39 +102,43 @@ rfl
`fset` may be slightly slower than `uset`. -/
@[extern c inline "lean_array_uset(#2, #3, #4)"]
def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
a.fset ⟨i.toNat, h⟩ v
a.set ⟨i.toNat, h⟩ v
/- "Comfortable" version of `fset`. It performs a bound check at runtime. -/
@[extern c inline "lean_array_set(#2, #3, #4)"]
def set (a : Array α) (i : @& Nat) (v : α) : Array α :=
if h : i < a.size then a.fset ⟨i, h⟩ v else a
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 c inline "lean_array_fswap(#2, #3, #4)"]
def fswap (a : Array α) (i j : @& Fin a.size) : Array α :=
let v₁ := a.fget i;
let v₂ := a.fget j;
let a := a.fset i v₂;
a.fset j v₁
def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
let v₁ := a.get i;
let v₂ := a.get j;
let a := a.set i v₂;
a.set j v₁
@[extern c inline "lean_array_swap(#2, #3, #4)"]
def swap (a : Array α) (i j : @& Nat) : Array α :=
def swap! (a : Array α) (i j : @& Nat) : Array α :=
if h₁ : i < a.size then
if h₂ : j < a.size then fswap a ⟨i, h₁⟩ ⟨j, h₂⟩
else a
else a
if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
else panic! "index out of bounds"
else panic! "index out of bounds"
@[inline] def fswapAt {α : Type} (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
let e := a.fget i;
let a := a.fset i v;
@[inline] def swapAt {α : Type} (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
let e := a.get i;
let a := a.set i v;
(e, a)
@[inline] def swapAt {α : Type} (a : Array α) (i : Nat) (v : α) : α × Array α :=
if h : i < a.size then fswapAt a ⟨i, h⟩ v else (v, a)
-- TODO: delete as soon as we can define local instances
@[neverExtract] private def swapAtPanic! [Inhabited α] (i : Nat) : α × Array α :=
panic! ("index " ++ toString i ++ " out of bounds")
@[inline] def swapAt! {α : Type} (a : Array α) (i : Nat) (v : α) : α × Array α :=
if h : i < a.size then swapAt a ⟨i, h⟩ v else @swapAtPanic! _ ⟨v⟩ i
@[extern c inline "lean_array_pop(#2)"]
def pop (a : Array α) : Array α :=
{ sz := Nat.pred a.size,
data := fun ⟨j, h⟩ => a.fget ⟨j, Nat.ltOfLtOfLe h (Nat.predLe _)⟩ }
data := fun ⟨j, h⟩ => a.get ⟨j, Nat.ltOfLtOfLe h (Nat.predLe _)⟩ }
-- TODO(Leo): justify termination using wf-rec
partial def shrink : Array α → Nat → Array α
@ -149,7 +153,7 @@ variables {β : Type v} {σ : Type u}
| i, b =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
f idx (a.fget idx) b >>= miterateAux (i+1)
f idx (a.get idx) b >>= miterateAux (i+1)
else pure b
@[inline] def miterate (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
@ -168,7 +172,7 @@ miterateAux a (fun _ b a => f a b) ini b
let idx₁ : Fin a₁.size := ⟨i, h₁⟩;
if h₂ : i < a₂.size then
let idx₂ : Fin a₂.size := ⟨i, h₂⟩;
f idx₁ (a₁.fget idx₁) (a₂.fget idx₂) b >>= miterate₂Aux (i+1)
f idx₁ (a₁.get idx₁) (a₂.get idx₂) b >>= miterate₂Aux (i+1)
else pure b
else pure b
@ -184,7 +188,7 @@ miterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
| i =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
do r ← f (a.fget idx);
do r ← f (a.get idx);
match r with
| some v => pure r
| none => mfindAux (i+1)
@ -200,7 +204,7 @@ mfindAux a f 0
have i - 1 < a.size from Nat.ltOfLtOfLe this h;
let idx : Fin a.size := ⟨i - 1, this⟩;
do
r ← f (a.fget idx);
r ← f (a.get idx);
match r with
| some v => pure r
| none =>
@ -248,7 +252,7 @@ variables {m : Type → Type w} [Monad m]
| i =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
do b ← p (a.fget idx);
do b ← p (a.get idx);
match b with
| true => pure true
| false => anyMAux (i+1)
@ -275,7 +279,7 @@ variable {β : Type v}
| 0, h, b => pure b
| j+1, h, b => do
let i : Fin a.size := ⟨j, h⟩;
b ← f i (a.fget i) b;
b ← f i (a.get i) b;
miterateRevAux j (Nat.leOfLt h) b
@[inline] def miterateRev (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
@ -309,9 +313,9 @@ variable {β:Type u}
| i, a =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
let v : α := a.fget idx;
let a := a.fset idx (@unsafeCast _ _ ⟨v⟩ ());
do newV ← f i v; ummapAux (i+1) (a.fset idx (@unsafeCast _ _ ⟨v⟩ newV))
let v : α := a.get idx;
let a := a.set idx (@unsafeCast _ _ ⟨v⟩ ());
do newV ← f i v; ummapAux (i+1) (a.set idx (@unsafeCast _ _ ⟨v⟩ newV))
else
pure (unsafeCast a)
@ -334,10 +338,10 @@ variable {β:Type u}
@[inline] def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α :=
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
let v := a.fget idx;
let a := a.fset idx (default α);
let v := a.get idx;
let a := a.set idx (arbitrary α);
let v := f v;
a.fset idx v
a.set idx v
else
a
@ -357,7 +361,7 @@ partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α)
| i =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
let v : α := a.fget idx;
let v : α := a.get idx;
f v *> mforAux (i+1)
else
pure ⟨⟩
@ -372,7 +376,7 @@ partial def extractAux (a : Array α) : Nat → ∀ (e : Nat), e ≤ a.size →
| i, e, hle, r =>
if hlt : i < e then
let idx : Fin a.size := ⟨i, Nat.ltOfLtOfLe hlt hle⟩;
extractAux (i+1) e hle (r.push (a.fget idx))
extractAux (i+1) e hle (r.push (a.get idx))
else r
def extract (a : Array α) (b e : Nat) : Array α :=
@ -391,7 +395,7 @@ partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α →
if h : i < a.size then
let aidx : Fin a.size := ⟨i, h⟩;
let bidx : Fin b.size := ⟨i, hsz ▸ h⟩;
match p (a.fget aidx) (b.fget bidx) with
match p (a.get aidx) (b.get bidx) with
| true => isEqvAux (i+1)
| false => false
else
@ -411,7 +415,7 @@ partial def reverseAux : Array α → Nat → Array α
| a, i =>
let n := a.size;
if i < n / 2 then
reverseAux (a.swap i (n - i - 1)) (i+1)
reverseAux (a.swap! i (n - i - 1)) (i+1)
else
a
@ -422,9 +426,9 @@ reverseAux a 0
@[specialize] partial def filterAux (p : α → Bool) : Array α → Nat → Nat → Array α
| a, i, j =>
if h₁ : i < a.size then
if p (a.fget ⟨i, h₁⟩) then
if p (a.get ⟨i, h₁⟩) then
if h₂ : j < i then
filterAux (a.fswap ⟨i, h₁⟩ ⟨j, Nat.ltTrans h₂ h₁⟩) (i+1) (j+1)
filterAux (a.swap ⟨i, h₁⟩ ⟨j, Nat.ltTrans h₂ h₁⟩) (i+1) (j+1)
else
filterAux a (i+1) (j+1)
else
@ -439,7 +443,7 @@ partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option
| i =>
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
if a.fget idx == v then some idx
if a.get idx == v then some idx
else indexOfAux (i+1)
else none
@ -451,7 +455,7 @@ partial def eraseIdxAux {α} : Nat → Array α → Array α
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;
let idx1 : Fin a.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
eraseIdxAux (i+1) (a.fswap idx idx1)
eraseIdxAux (i+1) (a.swap idx idx1)
else
a.pop
@ -461,7 +465,7 @@ eraseIdxAux (i.val + 1) a
def eraseIdx {α} (a : Array α) (i : Nat) : Array α :=
if i < a.size then eraseIdxAux (i+1) a else a
theorem szFSwapEq (a : Array α) (i j : Fin a.size) : (a.fswap i j).size = a.size :=
theorem szFSwapEq (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size :=
rfl
theorem szPopEq (a : Array α) : a.pop.size = a.size - 1 :=
@ -478,7 +482,7 @@ partial def eraseIdxSzAux {α} (a : Array α) : ∀ (i : Nat) (r : Array α), r.
if h : i < r.size then
let idx : Fin r.size := ⟨i, h⟩;
let idx1 : Fin r.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
eraseIdxSzAux (i+1) (r.fswap idx idx1) ((szFSwapEq r idx idx1).trans heq)
eraseIdxSzAux (i+1) (r.swap idx idx1) ((szFSwapEq r idx idx1).trans heq)
else
⟨r.pop, (szPopEq r).trans (heq ▸ rfl)⟩
end

2
library/init/data/array/binsearch.lean
View file

@ -15,7 +15,7 @@ namespace Array
| lo, hi =>
if lo <= hi then
let m := (lo + hi)/2;
let a := as.get m;
let a := as.get! m;
if lt a k then binSearchAux (m+1) hi
else if lt k a then
if m == 0 then found none

14
library/init/data/array/qsort.lean
View file

@ -13,21 +13,21 @@ namespace Array
@[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Nat) (pivot : α) : Array α → Nat → Nat → Nat × Array α
| as, i, j =>
if j < hi then
if lt (as.get j) pivot then
let as := as.swap i j;
if lt (as.get! j) pivot then
let as := as.swap! i j;
partitionAux as (i+1) (j+1)
else
partitionAux as i (j+1)
else
let as := as.swap i hi;
let as := as.swap! i hi;
(i, as)
@[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
let mid := (lo + hi) / 2;
let as := if lt (as.get mid) (as.get lo) then as.swap lo mid else as;
let as := if lt (as.get hi) (as.get lo) then as.swap lo hi else as;
let as := if lt (as.get mid) (as.get hi) then as.swap mid hi else as;
let pivot := as.get hi;
let as := if lt (as.get! mid) (as.get! lo) then as.swap! lo mid else as;
let as := if lt (as.get! hi) (as.get! lo) then as.swap! lo hi else as;
let as := if lt (as.get! mid) (as.get! hi) then as.swap! mid hi else as;
let pivot := as.get! hi;
partitionAux lt hi pivot as lo lo
@[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Nat → Nat → Array α

10
library/init/data/bytearray/basic.lean
View file

@ -33,12 +33,12 @@ def size : (@& ByteArray) → Nat
| ⟨bs⟩ => bs.size
@[extern "lean_byte_array_get"]
def get : (@& ByteArray) → (@& Nat) → UInt8
| ⟨bs⟩, i => bs.get i
def get! : (@& ByteArray) → (@& Nat) → UInt8
| ⟨bs⟩, i => bs.get! i
@[extern "lean_byte_array_set"]
def set : ByteArray → (@& Nat) → UInt8 → ByteArray
| ⟨bs⟩, i, b => ⟨bs.set i b⟩
def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
| ⟨bs⟩, i, b => ⟨bs.set! i b⟩
def isEmpty (s : ByteArray) : Bool :=
s.size == 0
@ -46,7 +46,7 @@ s.size == 0
partial def toListAux (bs : ByteArray) : Nat → List UInt8 → List UInt8
| i, r =>
if i < bs.size then
toListAux (i+1) (bs.get i :: r)
toListAux (i+1) (bs.get! i :: r)
else
r.reverse

4
library/init/data/hashmap/basic.lean
View file

@ -71,9 +71,9 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash
| i, source, target =>
if h : i < source.size then
let idx : Fin source.size := ⟨i, h⟩;
let es : AssocList α β := source.fget idx;
let es : AssocList α β := source.get idx;
-- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
let source := source.fset idx AssocList.nil;
let source := source.set idx AssocList.nil;
let target := es.foldl (reinsertAux hash) target;
moveEntries (i+1) source target
else target

22
library/init/data/persistentarray/basic.lean
View file

@ -58,12 +58,12 @@ abbrev div2Shift (i : USize) (shift : USize) : USize := USize.shift_right i shif
abbrev mod2Shift (i : USize) (shift : USize) : USize := USize.land i ((USize.shift_left 1 shift) - 1)
partial def getAux [Inhabited α] : PersistentArrayNode α → USize → USize → α
| node cs, i, shift => getAux (cs.get (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift)
| leaf cs, i, _ => cs.get i.toNat
| node cs, i, shift => getAux (cs.get! (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift)
| leaf cs, i, _ => cs.get! i.toNat
def get [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
if i >= t.tailOff then
t.tail.get (i - t.tailOff)
t.tail.get! (i - t.tailOff)
else
getAux t.root (USize.ofNat i) t.shift
@ -73,11 +73,11 @@ partial def setAux : PersistentArrayNode α → USize → USize → α → Persi
let i := mod2Shift i shift;
let shift := shift - initShift;
node $ cs.modify j.toNat $ fun c => setAux c i shift a
| leaf cs, i, _, a => leaf (cs.set i.toNat a)
| leaf cs, i, _, a => leaf (cs.set! i.toNat a)
def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α :=
if i >= t.tailOff then
{ tail := t.tail.set (i - t.tailOff) a, .. t }
{ tail := t.tail.set! (i - t.tailOff) a, .. t }
else
{ root := setAux t.root (USize.ofNat i) t.shift a, .. t }
@ -145,8 +145,8 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
| n@(node cs) =>
if h : cs.size ≠ 0 then
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩;
let last := cs.fget idx;
let cs := cs.fset idx (default _);
let last := cs.get idx;
let cs := cs.set idx (default _);
match popLeaf last with
| (none, _) => (none, emptyArray)
| (some l, newLast) =>
@ -154,7 +154,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
let cs := cs.pop;
if cs.isEmpty then (some l, emptyArray) else (some l, cs)
else
(some l, cs.fset idx (node newLast))
(some l, cs.set idx (node newLast))
else
(none, emptyArray)
| leaf vs => (some vs, emptyArray)
@ -169,8 +169,8 @@ else
let last := last.pop;
let newSize := t.size - 1;
let newTailOff := newSize - last.size;
if newRoots.size == 1 && (newRoots.get 0).isNode then
{ root := newRoots.get 0,
if newRoots.size == 1 && (newRoots.get! 0).isNode then
{ root := newRoots.get! 0,
shift := t.shift - initShift,
size := newSize,
tail := last,
@ -216,7 +216,7 @@ do b ← t.tail.mfindRev f;
partial def mfoldlFromAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
| node cs, i, shift, b => do
let j := (div2Shift i shift).toNat;
b ← mfoldlFromAux (cs.get j) (mod2Shift i shift) (shift - initShift) b;
b ← mfoldlFromAux (cs.get! j) (mod2Shift i shift) (shift - initShift) b;
cs.mfoldlFrom (fun b c => mfoldlAux f c b) b (j+1)
| leaf vs, i, _, b => vs.mfoldlFrom f b i.toNat

40
library/init/data/persistenthashmap/basic.lean
View file

@ -68,10 +68,10 @@ inductive IsEntriesNode : Node α β → Prop
abbrev EntriesNode (α β) := { n : Node α β // IsEntriesNode n }
private theorem fsetSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
: (ks.fset i k).size = (vs.fset j v).size :=
have h₁ : (ks.fset i k).size = ks.size from Array.szFSetEq _ _ _;
have h₂ : (vs.fset j v).size = vs.size from Array.szFSetEq _ _ _;
private theorem setSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
: (ks.set i k).size = (vs.set j v).size :=
have h₁ : (ks.set i k).size = ks.size from Array.szFSetEq _ _ _;
have h₂ : (vs.set j v).size = vs.size from Array.szFSetEq _ _ _;
(h₁.trans h).trans h₂.symm
private theorem pushSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (k : α) (v : β) : (ks.push k).size = (vs.push v).size :=
@ -84,10 +84,10 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat
| n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
if h : i < keys.size then
let idx : Fin keys.size := ⟨i, h⟩;
let k' := keys.fget idx;
let k' := keys.get idx;
if k == k' then
let j : Fin vals.size := ⟨i, heq ▸ h⟩;
⟨Node.collision (keys.fset idx k) (vals.fset j v) (fsetSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
⟨Node.collision (keys.set idx k) (vals.set j v) (setSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
else insertAtCollisionNodeAux n (i+1) k v
else
⟨Node.collision (keys.push k) (vals.push v) (pushSizeEq heq k v), IsCollisionNode.mk _ _ _⟩
@ -116,7 +116,7 @@ partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize
| ⟨Node.collision keys vals heq, _⟩ =>
let entries : Node α β := mkEmptyEntries;
keys.iterate entries $ fun i k entries =>
let v := vals.fget ⟨i.val, heq ▸ i.isLt⟩;
let v := vals.get ⟨i.val, heq ▸ i.isLt⟩;
let h := hash k;
-- dbgTrace ("toCollision " ++ toString i ++ ", h: " ++ toString h ++ ", depth: " ++ toString depth ++ ", h': " ++
-- toString (div2Shift h (shift * (depth - 1)))) $ fun _ =>
@ -138,15 +138,15 @@ def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β →
partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
| i, k =>
if h : i < keys.size then
let k' := keys.fget ⟨i, h⟩;
if k == k' then some (vals.fget ⟨i, heq ▸ h⟩)
let k' := keys.get ⟨i, h⟩;
if k == k' then some (vals.get ⟨i, heq ▸ h⟩)
else findAtAux (i+1) k
else none
partial def findAux [HasBeq α] : Node α β → USize → α → Option β
| Node.entries entries, h, k =>
let j := (mod2Shift h shift).toNat;
match entries.get j with
match entries.get! j with
| Entry.null => none
| Entry.ref node => findAux node (div2Shift h shift) k
| Entry.entry k' v => if k == k' then some v else none
@ -161,7 +161,7 @@ def find [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option
partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
| i, k =>
if h : i < keys.size then
let k' := keys.fget ⟨i, h⟩;
let k' := keys.get ⟨i, h⟩;
if k == k' then true
else containsAtAux (i+1) k
else false
@ -169,7 +169,7 @@ partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq :
partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
| Node.entries entries, h, k =>
let j := (mod2Shift h shift).toNat;
match entries.get j with
match entries.get! j with
| Entry.null => false
| Entry.ref node => containsAux node (div2Shift h shift) k
| Entry.entry k' v => k == k'
@ -181,7 +181,7 @@ def contains [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Bool
partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Option (α × β) → Option (α × β)
| i, acc =>
if h : i < a.size then
match a.fget ⟨i, h⟩ with
match a.get ⟨i, h⟩ with
| Entry.null => isUnaryEntries (i+1) acc
| Entry.ref _ => none
| Entry.entry k v =>
@ -195,7 +195,7 @@ def isUnaryNode : Node α β → Option (α × β)
| Node.collision keys vals heq =>
if h : 1 = keys.size then
have 0 < keys.size from h ▸ (Nat.zeroLtSucc _);
some (keys.fget ⟨0, this⟩, vals.fget ⟨0, heq ▸ this⟩)
some (keys.get ⟨0, this⟩, vals.get ⟨0, heq ▸ this⟩)
else
none
@ -210,18 +210,18 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
| none => (n, false)
| n@(Node.entries entries), h, k =>
let j := (mod2Shift h shift).toNat;
let entry := entries.get j;
let entry := entries.get! j;
match entry with
| Entry.null => (n, false)
| Entry.entry k' v =>
if k == k' then (Node.entries (entries.set j Entry.null), true) else (n, false)
if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
| Entry.ref node =>
let entries := entries.set j Entry.null;
let entries := entries.set! j Entry.null;
let (newNode, deleted) := eraseAux node (div2Shift h shift) k;
if !deleted then (n, false)
else match isUnaryNode newNode with
| none => (Node.entries (entries.set j (Entry.ref newNode)), true)
| some (k, v) => (Node.entries (entries.set j (Entry.entry k v)), true)
| none => (Node.entries (entries.set! j (Entry.ref newNode)), true)
| some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
| { root := n, size := sz }, k =>
@ -234,7 +234,7 @@ variables {m : Type w → Type w'} [Monad m]
variables {σ : Type w}
@[specialize] partial def mfoldlAux (f : σ → α → β → m σ) : Node α β → σ → m σ
| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.fget ⟨i.val, heq ▸ i.isLt⟩)
| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
| Node.entries entries, acc => entries.mfoldl (fun acc entry =>
match entry with
| Entry.null => pure acc

2
library/init/lean/attributes.lean
View file

@ -309,7 +309,7 @@ end EnumAttributes
def attrParamSyntaxToIdentifier (s : Syntax) : Option Name :=
match s with
| Syntax.node k args =>
if k == nullKind && args.size == 1 then match args.get 0 with
if k == nullKind && args.size == 1 then match args.get! 0 with
| Syntax.ident _ _ id _ => some id
| _ => none
else

12
library/init/lean/compiler/externattr.lean
View file

@ -41,18 +41,18 @@ instance ExternAttrData.inhabited : Inhabited ExternAttrData := ⟨{ entries :=
private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List ExternEntry → Except String (List ExternEntry)
| i, entries =>
if i == a.size then Except.ok entries
else match a.get i with
else match a.get! i with
| Syntax.ident _ _ backend _ =>
let i := i + 1;
if i == a.size then Except.error "string or identifier expected"
else match (a.get i).isIdOrAtom with
else match (a.get! i).isIdOrAtom with
| some "adhoc" => syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries)
| some "inline" =>
let i := i + 1;
match (a.get i).isStrLit with
match (a.get! i).isStrLit with
| some pattern => syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries)
| none => Except.error "string literal expected"
| _ => match (a.get i).isStrLit with
| _ => match (a.get! i).isStrLit with
| some fn => syntaxToExternEntries (i+1) (ExternEntry.standard backend fn :: entries)
| none => Except.error "string literal expected"
| _ => Except.error "identifier expected"
@ -63,10 +63,10 @@ match s with
| Syntax.node _ args =>
if args.size == 0 then Except.error "unexpected kind of argument"
else
let (arity, i) : Option Nat × Nat := match (args.get 0).isNatLit with
let (arity, i) : Option Nat × Nat := match (args.get! 0).isNatLit with
| some arity => (some arity, 1)
| none => (none, 0);
match (args.get i).isStrLit with
match (args.get! i).isStrLit with
| some str =>
if args.size == i+1 then
Except.ok { arity := arity, entries := [ ExternEntry.standard `all str ] }

2
library/init/lean/compiler/ir/basic.lean
View file

@ -342,7 +342,7 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
if i == 0 then b
else
let i := i - 1;
let (curr, a) := a.swapAt i (default _);
let (curr, a) := a.swapAt! i (default _);
let b := curr.setBody b;
reshapeAux a i b

8
library/init/lean/compiler/ir/borrow.lean
View file

@ -190,8 +190,8 @@ match s.map.find k with
/- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
xs.size.mfor $ fun i => do
let x := xs.get i;
let p := ps.get i;
let x := xs.get! i;
let p := ps.get! i;
unless p.borrow $ ownArg x
/- For each xs[i], if xs[i] is owned, then mark ps[i] as owned.
@ -201,8 +201,8 @@ xs.size.mfor $ fun i => do
"break" the tail call. -/
def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit :=
xs.size.mfor $ fun i => do
let x := xs.get i;
let p := ps.get i;
let x := xs.get! i;
let p := ps.get! i;
match x with
| Arg.var x => mwhen (isOwned x) $ ownVar p.x
| _ => pure ()

6
library/init/lean/compiler/ir/boxing.lean
View file

@ -57,8 +57,8 @@ qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.o
(newVDecls, xs) ← qs.size.mfold
(fun i (r : Array FnBody × Array Arg) =>
let (newVDecls, xs) := r;
let p := ps.get i;
let q := qs.get i;
let p := ps.get! i;
let q := qs.get! i;
if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
else do
x ← mkFresh;
@ -242,7 +242,7 @@ xs.miterate (Array.empty, Array.empty) $ fun i (x : Arg) (r : Array Arg × Array
pure (xs.push (Arg.var y), bs.push b)
@[inline] def castArgsIfNeeded (xs : Array Arg) (ps : Array Param) (k : Array Arg → M FnBody) : M FnBody :=
do (ys, bs) ← castArgsIfNeededAux xs (fun i => (ps.get i).ty);
do (ys, bs) ← castArgsIfNeededAux xs (fun i => (ps.get! i).ty);
b ← k ys;
pure (reshape bs b)

36
library/init/lean/compiler/ir/emitc.lean
View file

@ -104,7 +104,7 @@ unless (ps.isEmpty) $ do {
else
ps.size.mfor $ fun i => do {
when (i > 0) (emit ", ");
emit (toCType (ps.get i).ty)
emit (toCType (ps.get! i).ty)
};
emit ")"
};
@ -257,8 +257,8 @@ else
def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
if alts.size != 2 then none
else match alts.get 0 with
| Alt.ctor c b => some (c.cidx, b, (alts.get 1).body)
else match alts.get! 0 with
| Alt.ctor c b => some (c.cidx, b, (alts.get! 1).body)
| _ => none
def emitIf (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (tag : Nat) (t : FnBody) (e : FnBody) : M Unit :=
@ -330,8 +330,8 @@ do
ps ← getJPParams j;
unless (xs.size == ps.size) (throw "invalid goto");
xs.size.mfor $ fun i => do {
let p := ps.get i;
let x := xs.get i;
let p := ps.get! i;
let x := xs.get! i;
emit p.x; emit " = "; emitArg x; emitLn ";"
};
emit "goto "; emit j; emitLn ";"
@ -342,7 +342,7 @@ do emit z; emit " = "
def emitArgs (ys : Array Arg) : M Unit :=
ys.size.mfor $ fun i => do
when (i > 0) (emit ", ");
emitArg (ys.get i)
emitArg (ys.get! i)
def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit :=
if usize == 0 then emit ssize
@ -356,7 +356,7 @@ emitCtorScalarSize c.usize c.ssize; emitLn ");"
def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
ys.size.mfor $ fun i => do
emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get i); emitLn ");"
emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get! i); emitLn ");"
def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit :=
do
@ -426,7 +426,7 @@ decl ← getDecl f;
let arity := decl.params.size;
emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
ys.size.mfor $ fun i => do {
let y := ys.get i;
let y := ys.get! i;
emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
}
@ -545,8 +545,8 @@ That is, we have
def overwriteParam (ps : Array Param) (ys : Array Arg) : Bool :=
let n := ps.size;
n.any $ fun i =>
let p := ps.get i;
(i+1, n).anyI $ fun j => paramEqArg p (ys.get j)
let p := ps.get! i;
(i+1, n).anyI $ fun j => paramEqArg p (ys.get! j)
def emitTailCall (v : Expr) : M Unit :=
match v with
@ -557,22 +557,22 @@ match v with
if overwriteParam ps ys then do {
emitLn "{";
ps.size.mfor $ fun i => do {
let p := ps.get i;
let y := ys.get i;
let p := ps.get! i;
let y := ys.get! i;
unless (paramEqArg p y) $ do {
emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
}
};
ps.size.mfor $ fun i => do {
let p := ps.get i;
let y := ys.get i;
let p := ps.get! i;
let y := ys.get! i;
unless (paramEqArg p y) (do emit p.x; emit " = _tmp_"; emit i; emitLn ";")
};
emitLn "}"
} else do {
ys.size.mfor $ fun i => do {
let p := ps.get i;
let y := ys.get i;
let p := ps.get! i;
let y := ys.get! i;
unless (paramEqArg p y) (do emit p.x; emit " = "; emitArg y; emitLn ";")
}
};
@ -627,7 +627,7 @@ unless (hasInitAttr env d.name) $
else
xs.size.mfor $ fun i => do {
when (i > 0) (emit ", ");
let x := xs.get i;
let x := xs.get! i;
emit (toCType x.ty); emit " "; emit x.x
};
emit ")"
@ -637,7 +637,7 @@ unless (hasInitAttr env d.name) $
emitLn " {";
when (xs.size > closureMaxArgs && isBoxedName d.name) $
xs.size.mfor $ fun i => do {
let x := xs.get i;
let x := xs.get! i;
emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
};
emitLn "_start:";

8
library/init/lean/compiler/ir/expandresetreuse.lean
View file

@ -67,7 +67,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
| (FnBody.vdecl _ _ (Expr.uproj _ _) _) => keepInstr b
| (FnBody.inc z n c p _) =>
if n == 0 then done () else
let b' := bs.get (bs.size - 2);
let b' := bs.get! (bs.size - 2);
match b' with
| (FnBody.vdecl w _ (Expr.proj i x) _) =>
if w == z && y == x then
@ -79,7 +79,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
We keep `proj`, and `inc` when `n > 1`
-/
let bs := bs.pop.pop;
let mask := mask.set i (some z);
let mask := mask.set! i (some z);
let keep := keep.push b';
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil);
eraseProjIncForAux bs mask keep
@ -142,7 +142,7 @@ modifyGet $ fun n => ({ idx := n }, n + 1)
def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
mask.size.mfold
(fun i b =>
match mask.get i with
match mask.get! i with
| some _ => pure b -- code took ownership of this field
| none => do
fld ← mkFresh;
@ -151,7 +151,7 @@ mask.size.mfold
def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
zs.size.fold
(fun i b => FnBody.set y i (zs.get i) b)
(fun i b => FnBody.set y i (zs.get! i) b)
b
/- Given `set x[i] := y`, return true iff `y := proj[i] x` -/

2
library/init/lean/compiler/ir/pushproj.lean
View file

@ -21,7 +21,7 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array
let push (x : VarId) (t : IRType) (v : Expr) :=
if !ctxF.contains x.idx then
let alts := alts.mapIdx $ fun i alt => alt.modifyBody $ fun b' =>
if (altsF.get i).contains x.idx then b.setBody b'
if (altsF.get! i).contains x.idx then b.setBody b'
else b';
let altsF := altsF.map $ fun s => if s.contains x.idx then b.collectFreeIndices s else s;
pushProjs bs alts altsF ctx ctxF

16
library/init/lean/compiler/ir/rc.lean
View file

@ -77,21 +77,21 @@ caseLiveVars.fold
/- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/
private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool :=
let x := xs.get i;
i.all $ fun j => xs.get j != x
let x := xs.get! i;
i.all $ fun j => xs.get! j != x
/- Return true if `x` also occurs in `ys` in a position that is not consumed.
That is, it is also passed as a borrow reference. -/
@[specialize]
private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool :=
ys.size.any $ fun i =>
let y := ys.get i;
let y := ys.get! i;
match y with
| Arg.irrelevant => false
| Arg.var y => x == y && !consumeParamPred i
private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool :=
isBorrowParamAux x ys (fun i => !(ps.get i).borrow)
isBorrowParamAux x ys (fun i => not (ps.get! i).borrow)
/-
Return `n`, the number of times `x` is consumed.
@ -102,7 +102,7 @@ Return `n`, the number of times `x` is consumed.
private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat :=
ys.size.fold
(fun i n =>
let y := ys.get i;
let y := ys.get! i;
match y with
| Arg.irrelevant => n
| Arg.var y => if x == y && consumeParamPred i then n+1 else n)
@ -112,7 +112,7 @@ ys.size.fold
private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
xs.size.fold
(fun i b =>
let x := xs.get i;
let x := xs.get! i;
match x with
| Arg.irrelevant => b
| Arg.var x =>
@ -133,13 +133,13 @@ xs.size.fold
b
private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
addIncBeforeAux ctx xs (fun i => !(ps.get i).borrow) b liveVarsAfter
addIncBeforeAux ctx xs (fun i => not (ps.get! i).borrow) b liveVarsAfter
/- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application. -/
private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
xs.size.fold
(fun i b =>
match xs.get i with
match xs.get! i with
| Arg.irrelevant => b
| Arg.var x =>
/- We must add a `dec` if `x` must be consumed, it is alive after the application,

8
library/init/lean/compiler/ir/simpcase.lean
View file

@ -19,14 +19,14 @@ else
alts.push (Alt.default last.body)
private def getOccsOf (alts : Array Alt) (i : Nat) : Nat :=
let aBody := (alts.get i).body;
let aBody := (alts.get! i).body;
alts.iterateFrom 1 (i + 1) $ fun _ a' n =>
if a'.body == aBody then n+1 else n
private def maxOccs (alts : Array Alt) : Alt × Nat :=
alts.iterateFrom (alts.get 0, getOccsOf alts 0) 1 $ fun i a p =>
alts.iterateFrom (alts.get! 0, getOccsOf alts 0) 1 $ fun i a p =>
let noccs := getOccsOf alts i.val;
if noccs > p.2 then (alts.fget i, noccs) else p
if noccs > p.2 then (alts.get i, noccs) else p
private def addDefault (alts : Array Alt) : Array Alt :=
if alts.size <= 1 || alts.any Alt.isDefault then alts
@ -43,7 +43,7 @@ let alts := addDefault alts;
if alts.size == 0 then
FnBody.unreachable
else if alts.size == 1 then
(alts.get 0).body
(alts.get! 0).body
else
FnBody.case tid x xType alts

4
library/init/lean/elaborator/preterm.lean
View file

@ -75,11 +75,11 @@ partial def toLevel : Syntax Expr → Elab Level
| `Lean.Parser.Level.paren => toLevel $ stx.getArg 1
| `Lean.Parser.Level.max => do
let args := (stx.getArg 1).getArgs;
first ← toLevel (args.get 0);
first ← toLevel (args.get! 0);
args.mfoldlFrom (fun r arg => Level.max r <$> toLevel arg) first 1
| `Lean.Parser.Level.imax => do
let args := (stx.getArg 1).getArgs;
first ← toLevel (args.get 0);
first ← toLevel (args.get! 0);
args.mfoldlFrom (fun r arg => Level.imax r <$> toLevel arg) first 1
| `Lean.Parser.Level.hole => pure $ Level.mvar Name.anonymous
| `Lean.Parser.Level.num => pure $ Level.ofNat $ (stx.getArg 0).toNat

20
library/init/lean/environment.lean
View file

@ -128,13 +128,13 @@ structure EnvExtension (σ : Type) :=
namespace EnvExtension
unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
{ extensions := env.extensions.set ext.idx (unsafeCast s), .. env }
{ extensions := env.extensions.set! ext.idx (unsafeCast s), .. env }
@[implementedBy setStateUnsafe]
constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := default _
unsafe def getStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :=
let s : EnvExtensionState := env.extensions.get ext.idx;
let s : EnvExtensionState := env.extensions.get! ext.idx;
@unsafeCast _ _ ⟨ext.stateInh⟩ s
@[implementedBy getStateUnsafe]
@ -232,7 +232,7 @@ instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (Pe
namespace PersistentEnvExtension
def getModuleEntries {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) (m : ModuleIdx) : Array α :=
(ext.toEnvExtension.getState env).importedEntries.get m
(ext.toEnvExtension.getState env).importedEntries.get! m
def addEntry {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) (a : α) : Environment :=
ext.toEnvExtension.modifyState env $ fun s =>
@ -347,11 +347,11 @@ unsafe def registerCPPExtension (initial : CPPExtensionState) : Option Nat :=
@[export lean_set_extension]
unsafe def setCPPExtensionState (env : Environment) (idx : Nat) (s : CPPExtensionState) : Option Environment :=
(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).setState env s)).toOption
(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get! idx).setState env s)).toOption
@[export lean_get_extension]
unsafe def getCPPExtensionState (env : Environment) (idx : Nat) : Option CPPExtensionState :=
(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).getState env)).toOption
(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get! idx).getState env)).toOption
end
/- Legacy support for Modification objects -/
@ -407,9 +407,9 @@ do
pExts ← persistentEnvExtensionsRef.get;
let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
(fun i result =>
let state := (pExts.get i).getState env;
let exportEntriesFn := (pExts.get i).exportEntriesFn;
let extName := (pExts.get i).name;
let state := (pExts.get! i).getState env;
let exportEntriesFn := (pExts.get! i).exportEntriesFn;
let extName := (pExts.get! i).name;
result.push (extName, exportEntriesFn state))
Array.empty;
bytes ← serializeModifications (modListExtension.getState env);
@ -440,7 +440,7 @@ partial def importModulesAux : List Name → (NameSet × Array ModuleData) → I
private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionState
| i =>
if i < mod.entries.size then
let curr := mod.entries.get i;
let curr := mod.entries.get! i;
if curr.1 == extId then curr.2 else getEntriesFor (i+1)
else
Array.empty
@ -531,7 +531,7 @@ env.addAux cinfo
def displayStats (env : Environment) : IO Unit :=
do
pExtDescrs ← persistentEnvExtensionsRef.get;
let numModules := ((pExtDescrs.get 0).toEnvExtension.getState env).importedEntries.size;
let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
IO.println ("direct imports: " ++ toString env.header.imports);
IO.println ("number of imported modules: " ++ toString numModules);
IO.println ("number of consts: " ++ toString env.constants.size);

2
library/init/lean/localcontext.lean
View file

@ -237,7 +237,7 @@ isSubPrefixOfAux lctx₁.decls lctx₂.decls 0 0
@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
let b := b.abstract xs;
xs.size.foldRev (fun i b =>
let x := xs.get i;
let x := xs.get! i;
match lctx.findFVar x with
| some (LocalDecl.cdecl _ _ n ty bi) =>
let ty := ty.abstractRange i xs;

2
library/init/lean/parser/parser.lean
View file

@ -1564,7 +1564,7 @@ variables {α β : Type} {m : Type → Type} [Monad m]
@[specialize] partial def mfoldArgsAux (delta : Nat) (s : Array (Syntax α)) (f : Syntax α → β → m β) : Nat → β → m β
| i, b =>
if h : i < s.size then do
let curr := s.fget ⟨i, h⟩;
let curr := s.get ⟨i, h⟩;
b ← f curr b;
mfoldArgsAux (i+delta) b
else

4
library/init/lean/parser/transform.lean
View file

@ -16,13 +16,13 @@ match stx with
match prevArg.getTailInfo with
| some info =>
let prevArg := prevArg.setTailInfo info.truncateTrailing;
let newArgs := newArgs.set (newArgs.size - 1) prevArg;
let newArgs := newArgs.set! (newArgs.size - 1) prevArg;
let newArgs := newArgs.push (atom info sepTk);
newArgs.push arg
| none =>
let newArgs := newArgs.push (atom none sepTk);
newArgs.push arg)
(Array.singleton (args.get 0))
(Array.singleton (args.get! 0))
1;
node k args
| stx => stx

8
library/init/lean/position.lean
View file

@ -62,12 +62,12 @@ private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos
/- Remark: `pos` is in `[ps.get b, ps.get e]` and `b < e` -/
private partial def toPositionAux (str : String) (ps : Array Nat) (lines : Array Nat) (pos : String.Pos) : Nat → Nat → Position
| b, e =>
let posB := ps.get b;
if e == b + 1 then { line := lines.get b, column := toColumnAux str posB pos posB 0 }
let posB := ps.get! b;
if e == b + 1 then { line := lines.get! b, column := toColumnAux str posB pos posB 0 }
else
let m := (b + e) / 2;
let posM := ps.get m;
if pos == posM then { line := lines.get m, column := 0 }
let posM := ps.get! m;
if pos == posM then { line := lines.get! m, column := 0 }
else if pos > posM then toPositionAux m e
else toPositionAux b m

18
library/init/lean/syntax.lean
View file

@ -91,7 +91,7 @@ match n with
withArgs n $ fun args => args.size
@[inline] def getArg {α} (n : SyntaxNode α) (i : Nat) : Syntax α :=
withArgs n $ fun args => args.get i
withArgs n $ fun args => args.get! i
@[inline] def getArgs {α} (n : SyntaxNode α) : Array (Syntax α) :=
withArgs n $ fun args => args
@ -167,7 +167,7 @@ match stx with
def setArg {α} (stx : Syntax α) (i : Nat) (arg : Syntax α) : Syntax α :=
match stx with
| node k args => node k (args.set i arg)
| node k args => node k (args.set! i arg)
| stx => stx
@[inline] def modifyArg {α} (stx : Syntax α) (i : Nat) (fn : Syntax α → Syntax α) : Syntax α :=
@ -239,8 +239,8 @@ partial def updateTrailing {α} (trailing : Substring) : Syntax α → Syntax α
if args.size == 0 then n
else
let i := args.size - 1;
let last := updateTrailing (args.get i);
let args := args.set i last;
let last := updateTrailing (args.get! i);
let args := args.set! i last;
Syntax.node k args
| s => s
@ -265,9 +265,9 @@ partial def getTailInfo {α} : Syntax α → Option SourceInfo
if i == 0 then none
else
let i := i - 1;
let v := a.get i;
let v := a.get! i;
match f v with
| some v => some $ a.set i v
| some v => some $ a.set! i v
| none => updateLast i
partial def setTailInfoAux {α} (info : Option SourceInfo) : Syntax α → Option (Syntax α)
@ -295,7 +295,7 @@ partial def reprint {α} : Syntax α → Option String
if kind == choiceKind then
if args.size == 0 then failure
else do
s ← reprint (args.get 0);
s ← reprint (args.get! 0);
args.mfoldlFrom (fun s stx => do s' ← reprint stx; guard (s == s'); pure s) s 1
else args.mfoldl (fun r stx => do s ← reprint stx; pure $ r ++ s) ""
| _ => ""
@ -379,7 +379,7 @@ namespace Syntax
def isStrLit {α} : Syntax α → Option String
| Syntax.node k args =>
if k == strLitKind && args.size == 1 then
match args.get 0 with
match args.get! 0 with
| (Syntax.atom _ val) => some val
| _ => none
else
@ -448,7 +448,7 @@ else
def isNatLitAux {α} (nodeKind : SyntaxNodeKind) : Syntax α → Option Nat
| Syntax.node k args =>
if k == nodeKind && args.size == 1 then
match args.get 0 with
match args.get! 0 with
| (Syntax.atom _ val) => decodeNatLitVal val
| _ => none
else

16
tests/bench/qsort.lean
View file

@ -10,7 +10,7 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
| i =>
if i < a.size - 1 then do
unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted");
unless (a.get! i <= a.get! (i+1)) $ throw (IO.userError "array is not sorted");
checkSortedAux (i+1)
else
pure ()
@ -23,21 +23,21 @@ prefix `↑`:max := coe
@[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
| as, i, j =>
if j < hi then
if lt (as.get ↑j) pivot then
let as := as.swap ↑i ↑j;
if lt (as.get! ↑j) pivot then
let as := as.swap! ↑i ↑j;
partitionAux as (i+1) (j+1)
else
partitionAux as i (j+1)
else
let as := as.swap ↑i ↑hi;
let as := as.swap! ↑i ↑hi;
(i, as)
@[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Idx) : Idx × Array α :=
let mid := (lo + hi) / 2;
let as := if lt (as.get ↑mid) (as.get ↑lo) then as.swap ↑lo ↑mid else as;
let as := if lt (as.get ↑hi) (as.get ↑lo) then as.swap ↑lo ↑hi else as;
let as := if lt (as.get ↑mid) (as.get ↑hi) then as.swap ↑mid ↑hi else as;
let pivot := as.get ↑hi;
let as := if lt (as.get! ↑mid) (as.get! ↑lo) then as.swap! ↑lo ↑mid else as;
let as := if lt (as.get! ↑hi) (as.get! ↑lo) then as.swap! ↑lo ↑hi else as;
let as := if lt (as.get! ↑mid) (as.get! ↑hi) then as.swap! ↑mid ↑hi else as;
let pivot := as.get! ↑hi;
partitionAux lt hi pivot as lo lo
@[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Idx → Idx → Array α

12
tests/bench/unionfind.lean
View file

@ -47,10 +47,10 @@ def findEntryAux : Nat → Node → M nodeData
| i+1, n =>
do s ← read;
if h : n < s.size then
do { let e := s.fget ⟨n, h⟩;
do { let e := s.get ⟨n, h⟩;
if e.find = n then pure e
else do e₁ ← findEntryAux i e.find;
updt (fun s => s.set n e₁);
updt (fun s => s.set! n e₁);
pure e₁ }
else error "invalid Node"
@ -71,11 +71,11 @@ do r₁ ← findEntry n₁;
r₂ ← findEntry n₂;
if r₁.find = r₂.find then pure ()
else updt $ fun s =>
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
if r₁.rank < r₂.rank then s.set! r₁.find { find := r₂.find }
else if r₁.rank = r₂.rank then
let s₁ := s.set r₁.find { find := r₂.find };
s₁.set r₂.find { rank := r₂.rank + 1, .. r₂}
else s.set r₂.find { find := r₁.find }
let s₁ := s.set! r₁.find { find := r₂.find };
s₁.set! r₂.find { rank := r₂.rank + 1, .. r₂}
else s.set! r₂.find { find := r₁.find }
def mkNodes : Nat → M Unit

2
tests/compiler/bytearray_bug.lean
View file

@ -1,4 +1,4 @@
def main (xs : List String) : IO Unit :=
let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10));
let v := arr.data.get 0;
let v := arr.data.get! 0;
IO.println v

6
tests/compiler/phashmap.lean
View file

@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
| Node.collision keys vals _ => Format.sbracket $
keys.size.fold
(fun i fmt =>
let k := keys.get i;
let v := vals.get i;
let k := keys.get! i;
let v := vals.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
Format.nil
| Node.entries entries => Format.sbracket $
entries.size.fold
(fun i fmt =>
let entry := entries.get i;
let entry := entries.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++
match entry with

6
tests/compiler/phashmap2.lean
View file

@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
| Node.collision keys vals _ => Format.sbracket $
keys.size.fold
(fun i fmt =>
let k := keys.get i;
let v := vals.get i;
let k := keys.get! i;
let v := vals.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
Format.nil
| Node.entries entries => Format.sbracket $
entries.size.fold
(fun i fmt =>
let entry := entries.get i;
let entry := entries.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++
match entry with

6
tests/compiler/phashmap3.lean
View file

@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
| Node.collision keys vals _ => Format.sbracket $
keys.size.fold
(fun i fmt =>
let k := keys.get i;
let v := vals.get i;
let k := keys.get! i;
let v := vals.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
Format.nil
| Node.entries entries => Format.sbracket $
entries.size.fold
(fun i fmt =>
let entry := entries.get i;
let entry := entries.get! i;
let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
p ++
match entry with

4
tests/lean/bytearray.lean
View file

@ -3,9 +3,9 @@ do
let bs := [1, 2, 3].toByteArray;
IO.println bs;
let bs := bs.push 4;
let bs := bs.set 1 20;
let bs := bs.set! 1 20;
IO.println bs;
let bs₁ := bs.set 2 30;
let bs₁ := bs.set! 2 30;
IO.println bs₁;
IO.println bs;
IO.println bs.size;

2
tests/lean/ref1.lean
View file

@ -9,7 +9,7 @@ n.mfor $ fun i => do
def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
do a ← r.swap ∅;
a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get i)));
a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
r.swap a;
pure ()

4
tests/lean/repr_issue.lean
View file

@ -1,7 +1,7 @@
def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
catch (do modify $ fun (a : Array Nat) => a.set 0 33;
catch (do modify $ fun (a : Array Nat) => a.set! 0 33;
throw "error")
(fun _ => do a ← get; pure $ a.get 0)
(fun _ => do a ← get; pure $ a.get! 0)
def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
foo