feat(library/init/data/unsigned): add basic unsigned operations

library/init/data/basic.lean

@@ -9,4 +9,4 @@ import init.data.nat.basic init.data.prod init.data.sum.basic
 import init.data.num.basic init.data.sigma.basic init.data.subtype.basic
 import init.data.fin.basic init.data.list.basic init.data.char.basic
 import init.data.string.basic init.data.option.basic init.data.set
-import init.data.unsigned init.data.ordering init.data.to_string
+import init.data.unsigned.basic init.data.ordering init.data.to_string

library/init/data/default.lean

@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string
 import init.data.list init.data.sum init.data.subtype init.data.int init.data.array
-import init.data.bool init.data.fin
+import init.data.bool init.data.fin init.data.unsigned

library/init/data/fin/default.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.data.fin.basic init.data.fin.ops

library/init/data/to_string.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.string.basic init.data.bool.basic init.data.subtype.basic
-import init.data.unsigned init.data.prod init.data.sum.basic init.data.nat.div
+import init.data.unsigned.basic init.data.prod init.data.sum.basic init.data.nat.div
 open sum subtype nat
 
 universes u v

library/init/data/unsigned/basic.lean

@@ -9,7 +9,6 @@ import init.data.fin.basic
 open nat
 def unsigned_sz : nat := succ 4294967295
 
-attribute [reducible]
 def unsigned := fin unsigned_sz
 
 namespace unsigned
@@ -17,19 +16,15 @@ namespace unsigned
 private lemma zero_lt_unsigned_sz : 0 < unsigned_sz :=
 zero_lt_succ _
 
-def of_nat (n : nat) : unsigned :=
+/- Later, we define of_nat using mod, the following version is used to define the metaprogramming system. -/
+protected def of_nat' (n : nat) : unsigned :=
 if h : n < unsigned_sz then fin.mk n h else fin.mk 0 zero_lt_unsigned_sz
 
 def to_nat (c : unsigned) : nat :=
 fin.val c
 
-def succ (i : unsigned) :=
-of_nat i^.to_nat^.succ
-
 end unsigned
 
-instance : has_zero unsigned := ⟨unsigned.of_nat 0⟩
-
 instance : decidable_eq unsigned :=
 have decidable_eq (fin unsigned_sz), from fin.decidable_eq _,
 this

library/init/data/unsigned/default.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2017 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.unsigned.basic init.data.unsigned.ops

library/init/data/unsigned/ops.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2017 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.unsigned.basic init.data.fin.ops
+
+namespace unsigned
+def of_nat (n : nat) : unsigned := fin.of_nat n
+instance : has_zero unsigned := ⟨fin.of_nat 0⟩
+instance : has_one unsigned  := ⟨fin.of_nat 1⟩
+instance : has_add unsigned  := ⟨fin.add⟩
+instance : has_sub unsigned  := ⟨fin.sub⟩
+instance : has_mul unsigned  := ⟨fin.mul⟩
+instance : has_mod unsigned  := ⟨fin.mod⟩
+instance : has_lt unsigned   := ⟨fin.lt⟩
+instance : has_le unsigned   := ⟨fin.le⟩
+end unsigned

library/init/meta/name.lean

@@ -26,7 +26,7 @@ def mk_str_name (n : name) (s : string) : name :=
 name.mk_string s n
 
 def mk_num_name (n : name) (v : nat) : name :=
-name.mk_numeral (unsigned.of_nat v) n
+name.mk_numeral (unsigned.of_nat' v) n
 
 def mk_simple_name (s : string) : name :=
 mk_str_name name.anonymous s

library/init/meta/quote.lean

@@ -23,7 +23,7 @@ meta instance : has_quote char :=
 ⟨λ ⟨n, pr⟩, ``(char.of_nat %%(quote n))⟩
 
 meta instance : has_quote unsigned :=
-⟨λ ⟨n, pr⟩, ``(unsigned.of_nat %%(quote n))⟩
+⟨λ ⟨n, pr⟩, ``(unsigned.of_nat' %%(quote n))⟩
 
 meta def name.quote : name → pexpr
 | name.anonymous        := ``(name.anonymous)

library/init/native/anf.lean

@@ -61,7 +61,7 @@ private meta def enter_scope (action : anf_monad expr) : anf_monad expr := do
 private meta def fresh_name : anf_monad name := do
   (ss, count) ← state.read,
   -- need to replace this with unique prefix as per our earlier conversation
-  n ← pure $ name.mk_numeral (unsigned.of_nat count) `_anf_,
+  n ← pure $ name.mk_numeral (unsigned.of_nat' count) `_anf_,
   state.write (ss, count + 1),
   return n
 

library/init/native/cf.lean

@@ -43,7 +43,7 @@ meta def trace_cf (s : string) : cf_monad unit :=
 meta def fresh_name : cf_monad name := do
   (config, count) ← state.read,
   -- need to replace this with unique prefix as per our earlier conversation
-  n ← pure $ name.mk_numeral (unsigned.of_nat count) `_anf_,
+  n ← pure $ name.mk_numeral (unsigned.of_nat' count) `_anf_,
   state.write (config, count + 1),
   return n
 

library/init/native/default.lean

@@ -92,7 +92,7 @@ private meta def take_arguments' : expr → list name → (list name × expr)
 
 meta def fresh_name : ir_compiler name := do
   (conf, map, counter) ← lift state.read,
-  let fresh := name.mk_numeral (unsigned.of_nat counter) `native._ir_compiler_,
+  let fresh := name.mk_numeral (unsigned.of_nat' counter) `native._ir_compiler_,
   lift $ state.write (conf, map, counter + 1),
   return fresh