From 1cdf13821c8ae03a46bd0b8e261de0ad2438f582 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Mar 2017 16:14:16 -0800 Subject: [PATCH] feat(library/init/data/unsigned): add basic unsigned operations --- library/init/data/basic.lean | 2 +- library/init/data/default.lean | 2 +- library/init/data/fin/default.lean | 7 +++++++ library/init/data/to_string.lean | 2 +- .../{unsigned.lean => unsigned/basic.lean} | 9 ++------- library/init/data/unsigned/default.lean | 7 +++++++ library/init/data/unsigned/ops.lean | 19 +++++++++++++++++++ library/init/meta/name.lean | 2 +- library/init/meta/quote.lean | 2 +- library/init/native/anf.lean | 2 +- library/init/native/cf.lean | 2 +- library/init/native/default.lean | 2 +- 12 files changed, 43 insertions(+), 15 deletions(-) create mode 100644 library/init/data/fin/default.lean rename library/init/data/{unsigned.lean => unsigned/basic.lean} (81%) create mode 100644 library/init/data/unsigned/default.lean create mode 100644 library/init/data/unsigned/ops.lean diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean index 58e83b0185..b82e69fb22 100644 --- a/library/init/data/basic.lean +++ b/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 diff --git a/library/init/data/default.lean b/library/init/data/default.lean index 630d705457..d6b0d3eb85 100644 --- a/library/init/data/default.lean +++ b/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 diff --git a/library/init/data/fin/default.lean b/library/init/data/fin/default.lean new file mode 100644 index 0000000000..582dedbc68 --- /dev/null +++ b/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 diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 98cff7368b..b601d4c313 100644 --- a/library/init/data/to_string.lean +++ b/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 diff --git a/library/init/data/unsigned.lean b/library/init/data/unsigned/basic.lean similarity index 81% rename from library/init/data/unsigned.lean rename to library/init/data/unsigned/basic.lean index db6da9a261..5455772b4b 100644 --- a/library/init/data/unsigned.lean +++ b/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 diff --git a/library/init/data/unsigned/default.lean b/library/init/data/unsigned/default.lean new file mode 100644 index 0000000000..76bee50c3c --- /dev/null +++ b/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 diff --git a/library/init/data/unsigned/ops.lean b/library/init/data/unsigned/ops.lean new file mode 100644 index 0000000000..fe0691c00f --- /dev/null +++ b/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 diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index 79edef8413..7274b086ea 100644 --- a/library/init/meta/name.lean +++ b/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 diff --git a/library/init/meta/quote.lean b/library/init/meta/quote.lean index 39b3d551ff..4b9f8813f9 100644 --- a/library/init/meta/quote.lean +++ b/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) diff --git a/library/init/native/anf.lean b/library/init/native/anf.lean index 8fcc9b57d4..677f410dc2 100644 --- a/library/init/native/anf.lean +++ b/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 diff --git a/library/init/native/cf.lean b/library/init/native/cf.lean index 5528ee7788..de058db705 100644 --- a/library/init/native/cf.lean +++ b/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 diff --git a/library/init/native/default.lean b/library/init/native/default.lean index 6f181db5d2..78111aeec6 100644 --- a/library/init/native/default.lean +++ b/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