From 9f0640ab94741d1d369d089fec763c9156d6be4f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 19 Mar 2020 15:20:13 +0000
Subject: Lower case folders

---
 src/common/Helper.v  | 39 +++++++++++++++++++++++++++++++++
 src/common/Show.v    | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/common/Tactics.v | 29 +++++++++++++++++++++++++
 src/common/dune      |  3 +++
 4 files changed, 132 insertions(+)
 create mode 100644 src/common/Helper.v
 create mode 100644 src/common/Show.v
 create mode 100644 src/common/Tactics.v
 create mode 100644 src/common/dune

(limited to 'src/common')

diff --git a/src/common/Helper.v b/src/common/Helper.v
new file mode 100644
index 0000000..d23dbe4
--- /dev/null
+++ b/src/common/Helper.v
@@ -0,0 +1,39 @@
+(* 
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Module Option.
+
+Definition default {T : Type} (x : T) (u : option T) : T :=
+  match u with
+  | Some y => y
+  | _ => x
+  end.
+
+Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
+  match u with
+  | Some y => Some (f y)
+  | _ => None
+  end.
+
+Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T :=
+  match a with
+  | Some x => map (f x) b
+  | _ => None
+  end.
+
+End Option.
diff --git a/src/common/Show.v b/src/common/Show.v
new file mode 100644
index 0000000..8f9ec36
--- /dev/null
+++ b/src/common/Show.v
@@ -0,0 +1,61 @@
+(* 
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+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.
+Export Show.
diff --git a/src/common/Tactics.v b/src/common/Tactics.v
new file mode 100644
index 0000000..967c642
--- /dev/null
+++ b/src/common/Tactics.v
@@ -0,0 +1,29 @@
+(* 
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Ltac unfold_rec c := unfold c; fold c.
+
+Ltac solve_by_inverts n :=
+  match goal with | H : ?T |- _ =>
+    match type of T with Prop =>
+      inversion H;
+      match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end
+    end
+  end.
+
+Ltac solve_by_invert := solve_by_inverts 1.
diff --git a/src/common/dune b/src/common/dune
new file mode 100644
index 0000000..de481e2
--- /dev/null
+++ b/src/common/dune
@@ -0,0 +1,3 @@
+(library
+ (name Common)
+ (public_name coqup.common))
-- 
cgit