d85c30fde1
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.
40 lines
1.2 KiB
Text
40 lines
1.2 KiB
Text
/-
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import init.data.uint init.platform init.data.fin
|
|
|
|
def usize_sz : nat := (2:nat) ^ system.platform.nbits
|
|
def usize : Type := fin usize_sz
|
|
|
|
instance : decidable_eq usize :=
|
|
fin.decidable_eq usize_sz
|
|
|
|
theorem usize_sz_pos : usize_sz > 0 :=
|
|
show 0 < (2:nat) ^ system.platform.nbits, from
|
|
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⟩
|
|
instance : has_sub usize := ⟨fin.sub⟩
|
|
instance : has_mul usize := ⟨fin.mul⟩
|
|
instance : has_mod usize := ⟨fin.mod⟩
|
|
instance : has_modn usize := ⟨fin.modn⟩
|
|
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
|