perf(library/init/data): mark usize, uint16, uint32 and uint64 as [irreducible]

Without these annotations, Lean will timeout when trying to synthesize
the type class instance `decidable_eq uint32`. The type class resolution
problem will produce the unification problem:
```
decidable (@eq uint32 a b) =?= decidable (@eq usize ?x ?y)
```
which Lean tries to solve by assigning `?x := a`.
During the assignment, the types of `?x` and `a` are unified with "full
force". Thus, we get the constraint
```
usize_sz =?= uint32_sz
```
which will take forever to be solved when peforming the computation in
unary arithmetic.

Remark: this commit also makes sure that `type_context` will not unfold
irreducible definitions when trying to unify/match the types.

The new test `type_class_performance1.lean` exposes the problem fixed
by this commit.

library/init/data/array/basic.lean

@@ -56,20 +56,20 @@ def write' (a : array α) (i : nat) (v : α) : array α :=
 if h : i < a.sz then a.write ⟨i, h⟩ v else a
 
 /- TODO: add builtin -/
-def uread (a : array α) (i : usize) (h : i.val < a.sz) : α :=
-a.read ⟨i.val, h⟩
+def uread (a : array α) (i : usize) (h : i.to_nat < a.sz) : α :=
+a.read ⟨i.to_nat, h⟩
 
 /- TODO: add builtin -/
-def uwrite (a : array α) (i : usize) (v : α) (h : i.val < a.sz) : array α :=
-a.write ⟨i.val, h⟩ v
+def uwrite (a : array α) (i : usize) (v : α) (h : i.to_nat < a.sz) : array α :=
+a.write ⟨i.to_nat, h⟩ v
 
 /- TODO: add builtin -/
 def uread' [inhabited α] (a : array α) (i : usize) : α :=
-if h : i.val < a.sz then a.read ⟨i.val, h⟩ else default α
+if h : i.to_nat < a.sz then a.read ⟨i.to_nat, h⟩ else default α
 
 /- TODO: add builtin -/
 def uwrite' (a : array α) (i : usize) (v : α) : array α :=
-if h : i.val < a.sz then a.write ⟨i.val, h⟩ v else a
+if h : i.to_nat < a.sz then a.write ⟨i.to_nat, h⟩ v else a
 
 /- TODO: mark as builtin -/
 def push (a : array α) (v : α) : array α :=

library/init/data/hashmap/basic.lean

@@ -11,7 +11,7 @@ universes u v w
 def bucket_array (α : Type u) (β : α → Type v) :=
 { b : array (list (Σ a, β a)) // b.sz > 0 }
 
-def bucket_array.uwrite {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : usize) (d : list (Σ a, β a)) (h : i.val < data.val.sz) : bucket_array α β :=
+def bucket_array.uwrite {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : usize) (d : list (Σ a, β a)) (h : i.to_nat < data.val.sz) : bucket_array α β :=
 ⟨ data.val.uwrite i d h,
   calc (data.val.uwrite i d h).sz = data.val.sz : array.sz_write_eq _ _ _
                      ...          > 0           : data.property ⟩
@@ -35,8 +35,8 @@ let n := if nbuckets = 0 then 8 else nbuckets in
 namespace hashmap_imp
 variables {α : Type u} {β : α → Type v}
 
-def mk_idx {n : nat} (h : n > 0) (u : usize) : { u : usize // u.val < n } :=
-⟨u %ₙ n, fin.modn_lt _ h⟩
+def mk_idx {n : nat} (h : n > 0) (u : usize) : { u : usize // u.to_nat < n } :=
+⟨u %ₙ n, usize.modn_lt _ h⟩
 
 def reinsert_aux (hash_fn : α → usize) (data : bucket_array α β) (a : α) (b : β a) : bucket_array α β :=
 let ⟨i, h⟩ := mk_idx data.property (hash_fn a) in

library/init/data/repr.lean

@@ -130,10 +130,10 @@ instance : has_repr string.iterator :=
 instance (n : nat) : has_repr (fin n) :=
 ⟨λ f, repr (fin.val f)⟩
 
-instance : has_repr uint16 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr uint32 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr uint64 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr usize  := ⟨λ n, repr (fin.val n)⟩
+instance : has_repr uint16 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr uint32 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr uint64 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr usize  := ⟨λ n, repr n.to_nat⟩
 
 def char.repr (c : char) : string :=
 repr c

library/init/data/to_string.lean

@@ -53,13 +53,13 @@ instance (n : nat) : has_to_string (fin n) :=
 ⟨λ f, to_string (fin.val f)⟩
 
 instance : has_to_string uint16 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance : has_to_string uint32 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance : has_to_string uint64 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
 ⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")"⟩

library/init/data/uint.lean

@@ -57,8 +57,10 @@ instance : has_le uint64    := ⟨fin.le⟩
 instance : inhabited uint64 := ⟨0⟩
 
 def uint16.of_nat (n : nat) : uint16 := fin.of_nat n
-def uint16.to_nat (u : uint16) : nat := fin.val u
+def uint16.to_nat (u : uint16) : nat := u.val
 def uint32.of_nat (n : nat) : uint32 := fin.of_nat n
-def uint32.to_nat (u : uint32) : nat := fin.val u
+def uint32.to_nat (u : uint32) : nat := u.val
 def uint64.of_nat (n : nat) : uint64 := fin.of_nat n
-def uint64.to_nat (u : uint64) : nat := fin.val u
+def uint64.to_nat (u : uint64) : nat := u.val
+
+attribute [irreducible] uint16 uint32 uint64

library/init/data/usize.lean

@@ -19,6 +19,9 @@ nat.pos_pow_of_pos _ (nat.zero_lt_bit0 nat.one_ne_zero)
 def usize.of_nat (a : nat) : usize :=
 ⟨a % usize_sz, nat.mod_lt _ usize_sz_pos⟩
 
+def usize.to_nat (u : usize) : nat :=
+u.val
+
 instance : has_zero usize  := ⟨usize.of_nat 0⟩
 instance : has_one usize   := ⟨usize.of_nat 1⟩
 instance : has_add usize   := ⟨fin.add⟩
@@ -30,3 +33,8 @@ instance : has_div usize   := ⟨fin.div⟩
 instance : has_lt usize    := ⟨fin.lt⟩
 instance : has_le usize    := ⟨fin.le⟩
 instance : inhabited usize := ⟨0⟩
+
+theorem usize.modn_lt {m : nat} (u : usize) (h : m > 0) : (u %ₙ m).val < m :=
+fin.modn_lt u h
+
+attribute [irreducible] usize

library/init/meta/has_reflect.lean

@@ -9,7 +9,7 @@ import init.meta.expr init.util
 @[reducible] meta def {u} has_reflect (α : Sort u) := Π a : α, reflected a
 
 section
-local attribute [semireducible] reflected
+local attribute [semireducible] reflected uint32 uint64
 
 meta instance nat.reflect : has_reflect ℕ
 | n := if n = 0 then `(0 : ℕ)
@@ -22,7 +22,6 @@ meta instance uint32.reflect : has_reflect uint32
 
 meta instance uint64.reflect : has_reflect uint64
 | ⟨n, pr⟩ := `(uint64.of_nat n)
-
 end
 
 /- Instances that [derive] depends on. All other basic instances are defined at the end of

library/init/meta/interactive.lean

@@ -578,7 +578,7 @@ private meta def is_case_simple_tag : tag → bool
 | _                    := ff
 
 private meta def is_case_tag : tag → option nat
-| (name.mk_numeral n `_case :: _) := some n.val
+| (name.mk_numeral n `_case :: _) := some n.to_nat
 | _                               := none
 
 private meta def tag_match (t : tag) (pre : list name) : bool :=

src/library/type_context.cpp

@@ -1982,8 +1982,7 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
     try {
         expr t1 = infer(mvar);
         expr t2 = infer(new_v);
-        /* TODO(Leo): check whether using transparency_mode::All hurts performance.
-           We use Semireducible to make sure we will not fail an unification step
+        /* We use Semireducible to make sure we will not fail an unification step
                    ?m := t
            because we cannot establish that the types of ?m and t are definitionally equal
            due to the current transparency setting.

src/library/type_context.h

@@ -795,7 +795,7 @@ public:
         transparency_scope m_transparency_scope;
         zeta_scope         m_zeta_scope;
         relaxed_scope(type_context_old & ctx):
-            m_transparency_scope(ctx, transparency_mode::All),
+            m_transparency_scope(ctx, transparency_mode::Semireducible),
             m_zeta_scope(ctx, true) {}
     };
 

tests/lean/run/type_class_performance1.lean

@@ -0,0 +1,20 @@
+#print usize
+
+set_option pp.all true
+set_option trace.class_instances true
+set_option trace.type_context.is_def_eq true
+set_option trace.type_context.is_def_eq_detail true
+
+def foo1 (a b : uint64) : bool :=
+a = b
+
+
+#exit
+def foo2 (a b : uint16) : bool :=
+a = b
+
+def foo3 (a b : uint32) : bool :=
+a = b
+
+def foo4 (a b : usize) : bool :=
+a = b