diff options
Diffstat (limited to 'src/CoqUp')
-rw-r--r-- | src/CoqUp/CompCert.v | 79 | ||||
-rw-r--r-- | src/CoqUp/CoqUp.v | 4 | ||||
-rw-r--r-- | src/CoqUp/Helper.v | 21 | ||||
-rw-r--r-- | src/CoqUp/Show.v | 43 | ||||
-rw-r--r-- | src/CoqUp/Tactics.v | 16 | ||||
-rw-r--r-- | src/CoqUp/Verilog.v | 234 |
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. |