Henrik Böving
723c340a8b
perf: fix linearity in (HashSet|HashMap).erase ( #3887 )
...
Fixes linearity issues in HashSet/HashMap erase functions.
IR before patch:
```
def Lean.HashMapImp.erase._rarg (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) : obj :=
let x_5 : obj := proj[0] x_3;
inc x_5;
let x_6 : obj := proj[1] x_3;
inc x_6;
let x_7 : obj := Array.size ◾ x_6;
inc x_4;
let x_8 : obj := app x_2 x_4;
let x_9 : u64 := unbox x_8;
dec x_8;
let x_10 : usize := _private.Lean.Data.HashMap.0.Lean.HashMapImp.mkIdx x_7 x_9 ◾ ;
let x_11 : obj := Array.uget ◾ x_6 x_10 ◾ ;
inc x_11;
inc x_4;
inc x_1;
let x_12 : u8 := Lean.AssocList.contains._rarg x_1 x_4 x_11;
case x_12 : u8 of
Bool.false →
dec x_11;
dec x_6;
dec x_5;
dec x_4;
dec x_1;
ret x_3
Bool.true →
let x_13 : u8 := isShared x_3;
case x_13 : u8 of
Bool.false →
let x_14 : obj := proj[1] x_3;
dec x_14;
let x_15 : obj := proj[0] x_3;
dec x_15;
let x_16 : obj := 1;
let x_17 : obj := Nat.sub x_5 x_16;
dec x_5;
let x_18 : obj := Lean.AssocList.erase._rarg x_1 x_4 x_11;
let x_19 : obj := Array.uset ◾ x_6 x_10 x_18 ◾ ;
set x_3[1] := x_19;
set x_3[0] := x_17;
ret x_3
Bool.true →
dec x_3;
let x_20 : obj := 1;
let x_21 : obj := Nat.sub x_5 x_20;
dec x_5;
let x_22 : obj := Lean.AssocList.erase._rarg x_1 x_4 x_11;
let x_23 : obj := Array.uset ◾ x_6 x_10 x_22 ◾ ;
let x_24 : obj := ctor_0[Lean.HashMapImp.mk] x_21 x_23;
ret x_24
```
IR after the patch:
```
def Lean.HashMapImp.erase._rarg (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) : obj :=
let x_5 : u8 := isShared x_3;
case x_5 : u8 of
Bool.false →
let x_6 : obj := proj[0] x_3;
let x_7 : obj := proj[1] x_3;
let x_8 : obj := Array.size ◾ x_7;
inc x_4;
let x_9 : obj := app x_2 x_4;
let x_10 : u64 := unbox x_9;
dec x_9;
let x_11 : usize := _private.Lean.Data.HashMap.0.Lean.HashMapImp.mkIdx x_8 x_10 ◾ ;
let x_12 : obj := Array.uget ◾ x_7 x_11 ◾ ;
inc x_12;
inc x_4;
inc x_1;
let x_13 : u8 := Lean.AssocList.contains._rarg x_1 x_4 x_12;
case x_13 : u8 of
Bool.false →
dec x_12;
dec x_4;
dec x_1;
ret x_3
Bool.true →
let x_14 : obj := 1;
let x_15 : obj := Nat.sub x_6 x_14;
dec x_6;
let x_16 : obj := Lean.AssocList.erase._rarg x_1 x_4 x_12;
let x_17 : obj := Array.uset ◾ x_7 x_11 x_16 ◾ ;
set x_3[1] := x_17;
set x_3[0] := x_15;
ret x_3
Bool.true →
let x_18 : obj := proj[0] x_3;
let x_19 : obj := proj[1] x_3;
inc x_19;
inc x_18;
dec x_3;
let x_20 : obj := Array.size ◾ x_19;
inc x_4;
let x_21 : obj := app x_2 x_4;
let x_22 : u64 := unbox x_21;
dec x_21;
let x_23 : usize := _private.Lean.Data.HashMap.0.Lean.HashMapImp.mkIdx x_20 x_22 ◾ ;
let x_24 : obj := Array.uget ◾ x_19 x_23 ◾ ;
inc x_24;
inc x_4;
inc x_1;
let x_25 : u8 := Lean.AssocList.contains._rarg x_1 x_4 x_24;
case x_25 : u8 of
Bool.false →
dec x_24;
dec x_4;
dec x_1;
let x_26 : obj := ctor_0[Lean.HashMapImp.mk] x_18 x_19;
ret x_26
Bool.true →
let x_27 : obj := 1;
let x_28 : obj := Nat.sub x_18 x_27;
dec x_18;
let x_29 : obj := Lean.AssocList.erase._rarg x_1 x_4 x_24;
let x_30 : obj := Array.uset ◾ x_19 x_23 x_29 ◾ ;
let x_31 : obj := ctor_0[Lean.HashMapImp.mk] x_28 x_30;
ret x_31
```
Previously `x_6` (the buckets array) always gets `inc`remented, now only
if the HashMap itself is shared.
2024-04-12 08:54:21 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Scott Morrison
a4e27d3090
chore: upstream HashSet.merge ( #3357 )
2024-02-16 01:38:16 +00:00
Joachim Breitner
368ead54b2
refactor: termination_by changes in stdlib
2024-01-10 17:27:35 +01:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM ( #2363 )
2023-07-30 10:39:40 +02:00
Leonardo de Moura
bebf1927f8
chore: remove workarounds
2023-06-21 20:35:33 -07:00
Scott Morrison
a3dfa5516d
feat: add HashSet.insertMany
2022-11-28 06:59:21 -08:00
Leonardo de Moura
25beba6624
feat: avoid modulo in HashMap and HashSet
...
closes #609
Context: trying to improve Lean startup time.
Remark: it didn't seem to make a difference in practice. We should
investigate more.
cc @kha @gebener
2022-10-27 18:54:56 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Mario Carneiro
97bcc7fd7c
feat: add ForM -> ForIn adapter
2022-09-25 06:40:56 -07:00
Mario Carneiro
ebb5b97d73
chore: move Bootstrap.Data -> Lean.Data
2022-08-31 11:48:57 -07:00
