From d22d850b2814360eacbb5d4f10d6a8d1596db0c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 May 2016 14:11:24 -0700
Subject: [PATCH] refactor(library): redefine string and char

---
 library/data/list/basic.lean                  |  4 ---
 library/data/{fin.lean => old_fin.lean}       |  0
 library/data/{string.lean => old_string.lean} |  0
 library/init/char.lean                        | 13 +++++++
 library/init/datatypes.lean                   | 11 +++---
 library/init/default.lean                     |  2 +-
 library/init/fin.lean                         | 34 +++++++++++++++++++
 library/init/string.lean                      | 12 +++++++
 library/init/tactic.lean                      |  2 +-
 9 files changed, 65 insertions(+), 13 deletions(-)
 rename library/data/{fin.lean => old_fin.lean} (100%)
 rename library/data/{string.lean => old_string.lean} (100%)
 create mode 100644 library/init/char.lean
 create mode 100644 library/init/fin.lean
 create mode 100644 library/init/string.lean

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index eb7908b5d0..43250c6a2d 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -8,10 +8,6 @@ Basic properties of lists.
 import logic tools.helper_tactics data.nat.order data.nat.sub
 open eq.ops nat prod function option
 
-inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons   : T → list T → list T
-
 protected definition list.is_inhabited [instance] (A : Type) : inhabited (list A) :=
 inhabited.mk list.nil
 
diff --git a/library/data/fin.lean b/library/data/old_fin.lean
similarity index 100%
rename from library/data/fin.lean
rename to library/data/old_fin.lean
diff --git a/library/data/string.lean b/library/data/old_string.lean
similarity index 100%
rename from library/data/string.lean
rename to library/data/old_string.lean
diff --git a/library/init/char.lean b/library/init/char.lean
new file mode 100644
index 0000000000..9b7ca797fe
--- /dev/null
+++ b/library/init/char.lean
@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.fin
+open nat
+
+definition char := fin 256
+
+definition char.of_nat (n : nat) : char :=
+if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index cbd5e1e0bc..d6d34cd9d9 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -101,17 +101,14 @@ inductive bool : Type :=
 | ff : bool
 | tt : bool
 
-inductive char : Type :=
-mk : bool → bool → bool → bool → bool → bool → bool → bool → char
-
-inductive string : Type :=
-| empty : string
-| str   : char → string → string
-
 inductive option (A : Type) : Type :=
 | none {} : option A
 | some    : A → option A
 
+inductive list (T : Type) : Type :=
+| nil {} : list T
+| cons   : T → list T → list T
+
 -- Remark: we manually generate the nat.rec_on, nat.induction_on, nat.cases_on and nat.no_confusion.
 -- We do that because we want 0 instead of nat.zero in these eliminators.
 set_option inductive.rec_on   false
diff --git a/library/init/default.lean b/library/init/default.lean
index 4c3570cfc4..b32de2fe63 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -8,4 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
-import init.monad
+import init.monad init.fin init.char init.string
diff --git a/library/init/fin.lean b/library/init/fin.lean
new file mode 100644
index 0000000000..57ba076a40
--- /dev/null
+++ b/library/init/fin.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.nat
+open nat
+
+structure fin (n : nat) := (val : nat) (is_lt : val < n)
+
+namespace fin
+
+attribute fin.val [coercion]
+
+variable {n : nat}
+
+lemma eq_of_veq : ∀ {i j : fin n}, (val i) = j → i = j
+| (mk iv ilt) (mk jv jlt) := assume (veq : iv = jv), sorry -- begin congruence, assumption end
+
+lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = j
+| (mk iv ilt) (mk jv jlt) := assume Peq,
+  show iv = jv, from fin.no_confusion Peq (λ Pe Pqe, Pe)
+
+lemma eq_iff_veq {i j : fin n} : (val i) = j ↔ i = j :=
+iff.intro eq_of_veq veq_of_eq
+
+end fin
+
+open decidable fin
+
+protected definition fin.has_decidable_eq [instance] (n : nat) : ∀ (i j : fin n), decidable (i = j)
+| (mk ival ilt) (mk jval jlt) :=
+  decidable_of_decidable_of_iff (nat.has_decidable_eq ival jval) eq_iff_veq
diff --git a/library/init/string.lean b/library/init/string.lean
new file mode 100644
index 0000000000..b108395655
--- /dev/null
+++ b/library/init/string.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.char
+
+definition string := list char
+
+definition string.empty : string := list.nil
+definition string.str : char → string → string := list.cons
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 9d54fc421d..fa367f2058 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -85,7 +85,7 @@ definition exact      (e : expr)         : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type
 definition rexact     (e : expr)         : tactic := builtin
 definition check_expr (e : expr)         : tactic := builtin
-definition trace      (s : string)       : tactic := builtin
+-- definition trace      (s : string)       : tactic := builtin
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.