diff options
-rw-r--r-- | Makefile | 16 | ||||
-rw-r--r-- | _CoqProject | 16 | ||||
-rw-r--r-- | extraction/Extraction.v | 4 | ||||
-rw-r--r-- | extraction/driver.ml | 73 | ||||
-rw-r--r-- | extraction/dune | 8 | ||||
-rw-r--r-- | src/Common/Helper.v (renamed from src/CoqUp/Helper.v) | 0 | ||||
-rw-r--r-- | src/Common/Show.v (renamed from src/CoqUp/Show.v) | 0 | ||||
-rw-r--r-- | src/Common/Tactics.v (renamed from src/CoqUp/Tactics.v) | 0 | ||||
-rw-r--r-- | src/Common/dune | 3 | ||||
-rw-r--r-- | src/CoqUp/CoqUp.v | 4 | ||||
-rw-r--r-- | src/CoqUp/Verilog.v | 234 | ||||
-rw-r--r-- | src/Driver/CompCert.v (renamed from src/CoqUp/CompCert.v) | 0 | ||||
-rw-r--r-- | src/Driver/Driver.ml | 4 | ||||
-rw-r--r-- | src/Driver/dune | 7 | ||||
-rw-r--r-- | src/Extraction/Extraction.v | 8 | ||||
-rw-r--r-- | src/Extraction/dune | 4 | ||||
-rw-r--r-- | src/Verilog/PrettyPrint.ml | 48 | ||||
-rw-r--r-- | src/Verilog/PrettyPrint.mli | 1 | ||||
-rw-r--r-- | src/Verilog/VerilogAST.v | 231 | ||||
-rw-r--r-- | src/Verilog/dune | 4 | ||||
-rw-r--r-- | src/dune | 3 |
21 files changed, 336 insertions, 332 deletions
@@ -3,7 +3,7 @@ COMPCERTRECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclig COMPCERTCOQINCLUDES=$(foreach d, $(RECDIRS), -R lib/CompCert/$(d) compcert.$(d)) -COQINCLUDES=-R src/CoqUp CoqUp $(COMPCERTCOQINCLUDES) +COQINCLUDES=-R src/Common CoqUp.Common -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction $(COMPCERTCOQINCLUDES) COQEXEC=$(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE="$(COQBIN)coq_makefile" @@ -24,17 +24,17 @@ install: coq: Makefile.coq $(MAKE) -f Makefile.coq -extraction: extraction/STAMP +extraction: src/Extraction/STAMP -compile: extraction/STAMP +compile: src/Extraction/STAMP @echo "OCaml bin/coqup" @mkdir -p bin - @dune build extraction/main.exe - @cp _build/default/extraction/main.exe bin/coqup + @dune build src/Extraction/Driver.exe + @cp _build/default/src/Extraction/Driver.exe bin/coqup -extraction/STAMP: - @echo "COQEXEC ./extraction/Extraction.v" - @$(COQEXEC) ./extraction/Extraction.v +src/Extraction/STAMP: + @echo "COQEXEC ./src/Extraction/Extraction.v" + @$(COQEXEC) ./src/Extraction/Extraction.v @touch $@ Makefile.coq: diff --git a/_CoqProject b/_CoqProject index 3d5dae3..54ff493 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,2 +1,16 @@ --R src/CoqUp CoqUp -R lib/CompCert/lib compcert.lib -R lib/CompCert/common compcert.common -R lib/CompCert/x86 compcert.x86 -R lib/CompCert/backend compcert.backend -R lib/CompCert/cfrontend compcert.cfrontend -R lib/CompCert/driver compcert.driver -R lib/CompCert/flocq compcert.flocq -R lib/CompCert/exportclight compcert.exportclight -R lib/CompCert/cparser compcert.cparser -R lib/CompCert/MenhirLib compcert.MenhirLib +-R src/Common CoqUp.Common +-R src/Verilog CoqUp.Verilog +-R src/Driver CoqUp.Driver +-R src/Extraction CoqUp.Extraction + +-R lib/CompCert/lib compcert.lib +-R lib/CompCert/common compcert.common +-R lib/CompCert/x86 compcert.x86 +-R lib/CompCert/backend compcert.backend +-R lib/CompCert/cfrontend compcert.cfrontend +-R lib/CompCert/driver compcert.driver +-R lib/CompCert/flocq compcert.flocq +-R lib/CompCert/exportclight compcert.exportclight +-R lib/CompCert/cparser compcert.cparser +-R lib/CompCert/MenhirLib compcert.MenhirLib -R lib/CompCert/x86_64 compcert.x86_64 diff --git a/extraction/Extraction.v b/extraction/Extraction.v deleted file mode 100644 index 4c5f034..0000000 --- a/extraction/Extraction.v +++ /dev/null @@ -1,4 +0,0 @@ -From CoqUp Require Import Verilog. - -Cd "extraction". -Separate Extraction Verilog.nat_to_value Verilog.value_to_nat. diff --git a/extraction/driver.ml b/extraction/driver.ml deleted file mode 100644 index eb14d45..0000000 --- a/extraction/driver.ml +++ /dev/null @@ -1,73 +0,0 @@ -open Compcert - -let parse_c_file sourcename ifile = - (* Simplification options *) - let simplifs = - "b" (* blocks: mandatory *) - ^ (if false then "s" else "") - ^ (if false then "f" else "") - ^ (if false then "p" else "") - in - (* Parsing and production of a simplified C AST *) - let ast = Parse.preprocessed_file simplifs sourcename ifile in - (* Conversion to Csyntax *) - let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in - (* Save CompCert C AST if requested *) - PrintCsyntax.print_if csyntax; - csyntax - -let compile_c_file sourcename ifile ofile = - (* Parse the ast *) - let csyntax = parse_c_file sourcename ifile in - (* Convert to Asm *) - let rtl = - match Compiler.apply_partial - (CoqUp.transf_frontend csyntax) with - | Errors.OK rtl -> - rtl - | Errors.Error msg -> - let loc = file_loc sourcename in - fatal_error loc "%a" print_error msg in - (* Print Asm in text form *) - let oc = open_out ofile in - PrintAsm.print_program oc asm; - close_out oc - -let compile_i_file sourcename preproname = - if !option_interp then begin - Machine.config := Machine.compcert_interpreter !Machine.config; - let csyntax = parse_c_file sourcename preproname in - Interp.execute csyntax; - "" - end else if !option_S then begin - compile_c_file sourcename preproname - (output_filename ~final:true sourcename ".c" ".s"); - "" - end else begin - let asmname = - if !option_dasm - then output_filename sourcename ".c" ".s" - else tmp_file ".s" in - compile_c_file sourcename preproname asmname; - let objname = object_filename sourcename ".c" in - assemble asmname objname; - objname - end - -(* Processing of a .c file *) - -let process_c_file sourcename = - ensure_inputfile_exists sourcename; - if !option_E then begin - preprocess sourcename (output_filename_default "-"); - "" - end else begin - let preproname = if !option_dprepro then - output_filename sourcename ".c" ".i" - else - tmp_file ".i" in - preprocess sourcename preproname; - compile_i_file sourcename preproname - end - -let _ = print_endline "Hello world" diff --git a/extraction/dune b/extraction/dune deleted file mode 100644 index 12a6b8d..0000000 --- a/extraction/dune +++ /dev/null @@ -1,8 +0,0 @@ -(executables - (flags (:standard -warn-error -A)) - (names driver) - (libraries compcert)) - -(install - (section bin) - (files (driver.exe as coqup))) diff --git a/src/CoqUp/Helper.v b/src/Common/Helper.v index 292d011..292d011 100644 --- a/src/CoqUp/Helper.v +++ b/src/Common/Helper.v diff --git a/src/CoqUp/Show.v b/src/Common/Show.v index 83ec5bc..83ec5bc 100644 --- a/src/CoqUp/Show.v +++ b/src/Common/Show.v diff --git a/src/CoqUp/Tactics.v b/src/Common/Tactics.v index 5978d49..5978d49 100644 --- a/src/CoqUp/Tactics.v +++ b/src/Common/Tactics.v 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)) 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/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. diff --git a/src/CoqUp/CompCert.v b/src/Driver/CompCert.v index c984690..c984690 100644 --- a/src/CoqUp/CompCert.v +++ b/src/Driver/CompCert.v diff --git a/src/Driver/Driver.ml b/src/Driver/Driver.ml new file mode 100644 index 0000000..47125fa --- /dev/null +++ b/src/Driver/Driver.ml @@ -0,0 +1,4 @@ +open Verilog +open Extraction + +let _ = print_string (PrettyPrint.prettyprint VerilogAST.verilog_example) diff --git a/src/Driver/dune b/src/Driver/dune new file mode 100644 index 0000000..e295a76 --- /dev/null +++ b/src/Driver/dune @@ -0,0 +1,7 @@ +(executables + (names Driver) + (libraries compcert coqup.verilog coqup.extraction)) + +(install + (section bin) + (files (Driver.exe as coqup))) diff --git a/src/Extraction/Extraction.v b/src/Extraction/Extraction.v new file mode 100644 index 0000000..c4248cb --- /dev/null +++ b/src/Extraction/Extraction.v @@ -0,0 +1,8 @@ +Require CoqUp.Verilog.VerilogAST. + +Require Import ExtrOcamlBasic. +Require Import ExtrOcamlString. + +Cd "src/Extraction". +Separate Extraction + VerilogAST.nat_to_value VerilogAST.value_to_nat VerilogAST.verilog VerilogAST.verilog_example. diff --git a/src/Extraction/dune b/src/Extraction/dune new file mode 100644 index 0000000..731701a --- /dev/null +++ b/src/Extraction/dune @@ -0,0 +1,4 @@ +(library + (name Extraction) + (public_name coqup.extraction) + (flags (:standard -warn-error -A))) diff --git a/src/Verilog/PrettyPrint.ml b/src/Verilog/PrettyPrint.ml new file mode 100644 index 0000000..786d962 --- /dev/null +++ b/src/Verilog/PrettyPrint.ml @@ -0,0 +1,48 @@ +open Extraction.VerilogAST + +let concat = String.concat "" + +let indent i = String.make (2 * i) ' ' + +let fold_map f s = List.map f s |> concat + +let rec pprint_value = function + | VBool l -> if l then "1" else "0" + (* Assume that array is flat if it's a literal, should probably be changed to a nat or int *) + | VArray a -> concat [List.length a |> string_of_int; "'b"; fold_map pprint_value a] + +let pprint_binop = function + | Plus -> " + " + | Minus -> " - " + | Times -> " * " + | Divide -> " / " + | LT -> " < " + | GT -> " > " + | LE -> " <= " + | GE -> " >= " + | Eq -> " == " + | And -> " & " + | Or -> " | " + | Xor -> "^" + +let rec pprint_expr = function + | Lit l -> pprint_value l + | Var s -> List.to_seq s |> String.of_seq + | Neg e -> concat ["(-"; pprint_expr e; ")"] + | BinOp (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] + | Ternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] + +let rec pprint_stmnt i = + let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i+2) s] + in function + | Skip -> concat [indent i; ";\n"] + | Block s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"] + | Cond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n"; + pprint_stmnt (i + 1) st; indent i; "else\n"; + pprint_stmnt (i + 1) sf] + | Case (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n"; + fold_map pprint_case es; indent i; "endcase"] + | Blocking (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] + | Nonblocking (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] + +let prettyprint = fold_map (pprint_stmnt 0) diff --git a/src/Verilog/PrettyPrint.mli b/src/Verilog/PrettyPrint.mli new file mode 100644 index 0000000..843feec --- /dev/null +++ b/src/Verilog/PrettyPrint.mli @@ -0,0 +1 @@ +val prettyprint : Extraction.VerilogAST.verilog -> string diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v new file mode 100644 index 0000000..0c2b38b --- /dev/null +++ b/src/Verilog/VerilogAST.v @@ -0,0 +1,231 @@ +From Coq Require Import Lists.List Strings.String. +From Coq Require Import +Structures.OrderedTypeEx +FSets.FMapList +Program.Basics +PeanoNat. +From CoqUp.Common Require Import Helper Tactics Show. + +Import ListNotations. + +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). + +Definition verilog_example := Verilog [Block [Nonblocking (Var "hello") (BinOp Plus (Lit (nat_to_value 40)) (Lit (nat_to_value 20))); Cond (BinOp LE (Lit (nat_to_value 2)) (Lit (nat_to_value 3))) (Blocking (Var "Another") (BinOp Times (Lit (nat_to_value 20)) (Lit (nat_to_value 500)))) Skip]; Block []]. + +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. diff --git a/src/Verilog/dune b/src/Verilog/dune new file mode 100644 index 0000000..227d4a5 --- /dev/null +++ b/src/Verilog/dune @@ -0,0 +1,4 @@ +(library + (name Verilog) + (public_name coqup.verilog) + (libraries coqup.extraction)) diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..1c9fdde --- /dev/null +++ b/src/dune @@ -0,0 +1,3 @@ +(library + (name CoqUp) + (public_name coqup)) |