Add pretty printing for Verilog integrated with CompCert

6 files changed, 0 insertions, 397 deletions

diff --git a/src/CoqUp/CompCert.v b/src/CoqUp/CompCert.v
deleted file mode 100644
index c984690..0000000
--- a/src/CoqUp/CompCert.v
+++ /dev/null
@@ -1,79 +0,0 @@
-From compcert.common Require Import
-    Errors
-    Linking.
-
-From compcert.lib Require Import
-    Coqlib.
-
-From compcert.backend Require
-    Selection
-    RTL
-    RTLgen
-    Tailcall
-    Inlining
-    Renumber
-    Constprop
-    CSE
-    Deadcode
-    Unusedglob.
-
-From compcert.cfrontend Require
-    Csyntax
-    SimplExpr
-    SimplLocals
-    Cshmgen
-    Cminorgen.
-
-From compcert.driver Require
-    Compiler.
-
-Notation "a @@@ b" :=
-   (Compiler.apply_partial _ _ a b) (at level 50, left associativity).
-Notation "a @@ b" :=
-   (Compiler.apply_total _ _ a b) (at level 50, left associativity).
-
-Definition transf_frontend (p: Csyntax.program) : res RTL.program :=
-  OK p
-  @@@ SimplExpr.transl_program
-  @@@ SimplLocals.transf_program
-  @@@ Cshmgen.transl_program
-  @@@ Cminorgen.transl_program
-  @@@ Selection.sel_program
-  @@@ RTLgen.transl_program.
-
-Local Open Scope linking_scope.
-
-Definition CompCert's_passes :=
-      mkpass SimplExprproof.match_prog
-  ::: mkpass SimplLocalsproof.match_prog
-  ::: mkpass Cshmgenproof.match_prog
-  ::: mkpass Cminorgenproof.match_prog
-  ::: mkpass Selectionproof.match_prog
-  ::: mkpass RTLgenproof.match_prog
-  ::: pass_nil _.
-
-Definition match_prog: Csyntax.program -> RTL.program -> Prop :=
-  pass_match (compose_passes CompCert's_passes).
-
-Theorem transf_frontend_match:
-  forall p tp,
-    transf_frontend p = OK tp ->
-    match_prog p tp.
-Proof.
-  intros p tp T.
-  unfold transf_frontend in T. simpl in T.
-  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.
-  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.
-  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
-  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
-  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
-  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
-  unfold match_prog; simpl.
-  exists p1; split. apply SimplExprproof.transf_program_match; auto.
-  exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
-  exists p3; split. apply Cshmgenproof.transf_program_match; auto.
-  exists p4; split. apply Cminorgenproof.transf_program_match; auto.
-  exists p5; split. apply Selectionproof.transf_program_match; auto.
-  exists p6; split. apply RTLgenproof.transf_program_match; auto.
-  inversion T. reflexivity.
-Qed.
diff --git a/src/CoqUp/CoqUp.v b/src/CoqUp/CoqUp.v
deleted file mode 100644
index 02d71ee..0000000
--- a/src/CoqUp/CoqUp.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Set Implicit Arguments.
-
-Require Import Bool List String.
-
diff --git a/src/CoqUp/Helper.v b/src/CoqUp/Helper.v
deleted file mode 100644
index 292d011..0000000
--- a/src/CoqUp/Helper.v
+++ /dev/null
@@ -1,21 +0,0 @@
-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/CoqUp/Show.v b/src/CoqUp/Show.v
deleted file mode 100644
index 83ec5bc..0000000
--- a/src/CoqUp/Show.v
+++ /dev/null
@@ -1,43 +0,0 @@
-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/CoqUp/Tactics.v b/src/CoqUp/Tactics.v
deleted file mode 100644
index 5978d49..0000000
--- a/src/CoqUp/Tactics.v
+++ /dev/null
@@ -1,16 +0,0 @@
-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/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
deleted file mode 100644
index 314c95e..0000000
--- a/src/CoqUp/Verilog.v
+++ /dev/null
@@ -1,234 +0,0 @@
-From Coq Require Import Lists.List Strings.String.
-From Coq Require Import
-Structures.OrderedTypeEx
-FSets.FMapList
-Program.Basics
-PeanoNat.
-From CoqUp Require Import Helper Tactics Show.
-
-Import ListNotations.
-
-Module Verilog.
-
-  Module Map := FMapList.Make String_as_OT.
-
-  Inductive value : Type :=
-  | VBool (b : bool)
-  | VArray (l : list value).
-
-  Definition cons_value (a b : value) : value :=
-    match a, b with
-    | VBool _, VArray b' => VArray (a :: b')
-    | VArray a', VBool _ => VArray (List.concat [a'; [b]])
-    | VArray a', VArray b' => VArray (List.concat [a'; b'])
-    | _, _ => VArray [a; b]
-    end.
-
-  (** * Conversion to and from value *)
-
-  Fixpoint nat_to_value' (sz n : nat) : value :=
-    match sz with
-    | 0 => VArray []
-    | S sz' =>
-      if Nat.even n then
-        cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
-      else
-        cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2))
-    end.
-
-  Definition nat_to_value (n : nat) : value :=
-    nat_to_value' ((Nat.log2 n) + 1) n.
-
-  Definition state : Type := Map.t value * Map.t value.
-
-  Inductive binop : Type :=
-  | Plus
-  | Minus
-  | Times
-  | Divide
-  | LT
-  | GT
-  | LE
-  | GE
-  | Eq
-  | And
-  | Or
-  | Xor.
-
-  Inductive expr : Type :=
-  | Lit (n : value)
-  | Var (s : string)
-  | Neg (a : expr)
-  | BinOp (op : binop) (a1 a2 : expr)
-  | Ternary (c t f : expr).
-
-  Inductive stmnt : Type :=
-  | Skip
-  | Block (s : list stmnt)
-  | Cond (c : expr) (st sf : stmnt)
-  | Case (c : expr) (b : list (expr * stmnt))
-  | Blocking (a b : expr)
-  | Nonblocking (a b : expr).
-
-  Inductive verilog : Type := Verilog (s : list stmnt).
-
-  Coercion VBool : bool >-> value.
-  Coercion Lit : value >-> expr.
-  Coercion Var : string >-> expr.
-
-  Definition value_is_bool (v : value) : bool :=
-    match v with
-    | VBool _ => true
-    | VArray _ => false
-    end.
-
-  Definition value_is_array : value -> bool := compose negb value_is_bool.
-
-  Definition flat_value (v : value) : bool :=
-    match v with
-    | VBool _ => true
-    | VArray l => forallb value_is_bool l
-    end.
-
-  Inductive value_is_boolP : value -> Prop :=
-  | ValIsBool : forall b : bool, value_is_boolP (VBool b).
-
-  Inductive value_is_arrayP : value -> Prop :=
-  | ValIsArray : forall v : list value, value_is_arrayP (VArray v).
-
-  Inductive flat_valueP : value -> Prop :=
-  | FLV0 : forall b : bool, flat_valueP (VBool b)
-  | FLVA : forall l : list value,
-      Forall (value_is_boolP) l -> flat_valueP (VArray l).
-
-  Lemma value_is_bool_equiv :
-    forall v, value_is_boolP v <-> value_is_bool v = true.
-  Proof.
-    split; intros.
-    - inversion H. trivial.
-    - destruct v. constructor. unfold value_is_bool in H. discriminate.
-  Qed.
-
-  Lemma value_is_array_equiv :
-    forall v, value_is_arrayP v <-> value_is_array v = true.
-  Proof.
-    split; intros.
-    - inversion H. trivial.
-    - destruct v; try constructor. unfold value_is_array in H.
-      unfold compose, value_is_bool, negb in H. discriminate.
-  Qed.
-
-  Lemma flat_value_equiv :
-    forall v, flat_valueP v <-> flat_value v = true.
-  Proof.
-    split; intros.
-    - unfold flat_value. inversion H. subst. trivial.
-      + rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst.
-        apply value_is_bool_equiv. apply H0. assumption.
-    - destruct v. constructor. constructor. unfold flat_value in H.
-      rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv.
-      apply H. assumption.
-  Qed.
-
-  Fixpoint value_to_nat' (i : nat) (v : value) : option nat :=
-    match i, v with
-    | _, VBool b => Some (Nat.b2n b)
-    | _, VArray [VBool b] => Some (Nat.b2n b)
-    | S i', VArray ((VBool b) :: l) =>
-      Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l))
-    | _, _ => None
-    end.
-
-  Definition value_length (v : value) : nat :=
-    match v with
-    | VBool _ => 1
-    | VArray l => Datatypes.length l
-    end.
-
-  Definition value_to_nat (v : value) : option nat :=
-    value_to_nat' (value_length v) v.
-
-  Lemma empty_is_flat : flat_valueP (VArray []).
-  Proof.
-    constructor. apply Forall_forall. intros. inversion H.
-  Qed.
-
-  Lemma check_5_is_101 :
-    value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
-  Proof. reflexivity. Qed.
-
-  Lemma cons_value_flat :
-    forall (b : bool) (v : value),
-      flat_valueP v -> flat_valueP (cons_value (VBool b) v).
-  Proof.
-    intros. unfold cons_value. destruct v.
-    - constructor. apply Forall_forall. intros.
-      inversion H0; subst. constructor.
-      inversion H1; subst. constructor.
-      inversion H2.
-    - intros. inversion H. inversion H1; subst; constructor.
-      + apply Forall_forall. intros.
-        inversion H0; subst. constructor.
-        inversion H2.
-      + repeat constructor. assumption. assumption.
-  Qed.
-
-  Lemma nat_to_value'_is_flat :
-    forall (sz n : nat),
-      flat_valueP (nat_to_value' sz n).
-  Proof.
-    induction sz; intros.
-    - subst. apply empty_is_flat.
-    - unfold_rec nat_to_value'.
-      destruct (Nat.even n); apply cons_value_flat; apply IHsz.
-  Qed.
-
-  Lemma nat_to_value_is_flat :
-    forall (sz n : nat),
-      flat_valueP (nat_to_value n).
-  Proof.
-    intros. unfold nat_to_value. apply nat_to_value'_is_flat.
-  Qed.
-
-  Lemma nat_to_value_idempotent :
-    forall (sz n : nat),
-      sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
-  Proof.
-    induction sz; intros.
-    - inversion H.
-    - unfold_rec value_to_nat'.
-      assert (flat_valueP (nat_to_value' (S sz) n)).
-      { apply nat_to_value'_is_flat. }
-      destruct (nat_to_value' (S sz) n) eqn:?.
-  Admitted.
-
-  Module VerilogEval.
-
-    Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value :=
-      Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)).
-
-    Definition state_find (k : string) (s : state) : option value :=
-      Map.find k (fst s).
-
-    Definition eval_binop (op : binop) (a1 a2 : value) : option value :=
-      match op with
-      | Plus => app Nat.add a1 a2
-      | Minus => app Nat.sub a1 a2
-      | Times => app Mult.tail_mult a1 a2
-      | Divide => app Nat.div a1 a2
-      | _ => Some a1
-      end.
-
-(*    Fixpoint eval_expr (s : state) (e : expr) : option value :=
-      match e with
-      | Lit n => Some n
-      | Var v => state_find v s
-      | Neg a => 0 - (eval_expr s a)
-      | BinOp op a1 a2 => eval_binop op a1 a2
-      | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f
-      end.
-*)
-  End VerilogEval.
-
-End Verilog.
-Export Verilog.