Add show typeclass

1 files changed, 42 insertions, 0 deletions

diff --git a/src/CoqUp/Show.v b/src/CoqUp/Show.v
new file mode 100644
index 0000000..953a5ec
--- /dev/null
+++ b/src/CoqUp/Show.v
@@ -0,0 +1,42 @@
+From Coq Require Import
+    Strings.String
+    Bool.Bool
+    Arith.Arith.
+
+Local Open Scope string.
+
+Module Show.
+  Class Show A : Type :=
+    {
+      show : A -> string
+    }.
+
+  Instance showBool : Show bool :=
+    {
+      show := fun b:bool => if b then "true" else "false"
+    }.
+
+  Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
+    let d := match n mod 10 with
+             | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5"
+             | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
+             end in
+    let acc' := d ++ acc in
+    match time with
+    | 0 => acc'
+    | S time' =>
+      match n / 10 with
+      | 0 => acc'
+      | n' => string_of_nat_aux time' n' acc'
+      end
+    end.
+
+  Definition string_of_nat (n : nat) : string :=
+    string_of_nat_aux n n "".
+
+  Instance showNat : Show nat :=
+    {
+      show := string_of_nat
+    }.
+
+End Show.