From abf33a4075c2008bfcac3b04ad3b4dc1c57a4efd Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 17 Feb 2020 18:06:37 +0000
Subject: Add pretty printing for Verilog integrated with CompCert

---
 src/Common/Helper.v  | 21 +++++++++++++++++++++
 src/Common/Show.v    | 43 +++++++++++++++++++++++++++++++++++++++++++
 src/Common/Tactics.v | 16 ++++++++++++++++
 src/Common/dune      |  3 +++
 4 files changed, 83 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..292d011
--- /dev/null
+++ b/src/Common/Helper.v
@@ -0,0 +1,21 @@
+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..83ec5bc
--- /dev/null
+++ b/src/Common/Show.v
@@ -0,0 +1,43 @@
+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..5978d49
--- /dev/null
+++ b/src/Common/Tactics.v
@@ -0,0 +1,16 @@
+Module Tactics.
+
+  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.
+  
+End Tactics.
+Export Tactics.
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