From f53038c5a4fd3fdab8233e57c84f1dc43dcf9425 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 13 Feb 2020 12:03:45 +0000 Subject: Improve the Coq sources and add extraction --- Makefile | 23 ++++++++++++++------ extraction/main.ml | 2 +- src/CoqUp/Helper.v | 10 +++++++-- src/CoqUp/Show.v | 1 + src/CoqUp/Verilog.v | 62 ++++++++++++++++------------------------------------- 5 files changed, 45 insertions(+), 53 deletions(-) diff --git a/Makefile b/Makefile index 1302e6e..9ef58ed 100644 --- a/Makefile +++ b/Makefile @@ -9,7 +9,7 @@ VS=$(wildcard src/CoqUp/*.v) all: $(MAKE) coq - $(MAKE) extraction + $(MAKE) compile install: $(MAKE) -f Makefile.coq install @@ -19,15 +19,24 @@ coq: Makefile.coq extraction: extraction/STAMP +compile: extraction/STAMP + @echo "OCaml bin/coqup" + @mkdir -p bin + @dune build extraction/main.exe + @cp _build/default/extraction/main.exe bin/coqup + extraction/STAMP: - rm -f extraction/*.ml extraction/*.mli - $(COQEXEC) ./extraction/Extraction.v - touch $@ + @echo "COQEXEC ./extraction/Extraction.v" + @$(COQEXEC) ./extraction/Extraction.v + @touch $@ -Makefile.coq: Makefile - $(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq +Makefile.coq: + @echo "COQMAKE Makefile.coq" + @$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq clean:: Makefile.coq $(MAKE) -f Makefile.coq clean - rm -f */*.v.d */*.glob */*.vo */*~ *~ rm -f Makefile.coq + +clean:: + rm -f */*.v.d */*.glob */*.vo */*~ *~ diff --git a/extraction/main.ml b/extraction/main.ml index 235a155..870a0bc 100644 --- a/extraction/main.ml +++ b/extraction/main.ml @@ -6,4 +6,4 @@ let rec nat_to_int = function | S n -> 1 + nat_to_int n let () = - print_endline ("Result: " ^ (Verilog.value_to_nat (Verilog.VBool Coq_true) |> nat_to_int)) + print_endline ("Result: ") diff --git a/src/CoqUp/Helper.v b/src/CoqUp/Helper.v index f57a16f..292d011 100644 --- a/src/CoqUp/Helper.v +++ b/src/CoqUp/Helper.v @@ -3,13 +3,19 @@ Module Option. Definition default {T : Type} (x : T) (u : option T) : T := match u with | Some y => y - | None => x + | _ => 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 => None + | _ => 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 index 953a5ec..83ec5bc 100644 --- a/src/CoqUp/Show.v +++ b/src/CoqUp/Show.v @@ -40,3 +40,4 @@ Module Show. }. End Show. +Export Show. diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v index de1910c..314c95e 100644 --- a/src/CoqUp/Verilog.v +++ b/src/CoqUp/Verilog.v @@ -1,10 +1,10 @@ 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. +Structures.OrderedTypeEx +FSets.FMapList +Program.Basics +PeanoNat. +From CoqUp Require Import Helper Tactics Show. Import ListNotations. @@ -202,56 +202,32 @@ Module Verilog. destruct (nat_to_value' (S sz) n) eqn:?. Admitted. - Module VerilogNotation. - - Declare Scope verilog_scope. - Bind Scope verilog_scope with expr. - Bind Scope verilog_scope with stmnt. - Bind Scope verilog_scope with verilog. - Delimit Scope verilog_scope with verilog. - - Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope. - Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope. - Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope. - Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope. - Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope. - Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope. - Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope. - Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope. - Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope. - Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope. - Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope. - Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope. - Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope. - Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope. - - Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope. - Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope. - Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope. - - End VerilogNotation. - Module VerilogEval. - Definition state_find (k : string) (s : state) : value := - Option.default (VBool false) (Map.find k (fst s)). + 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) : value := + Definition eval_binop (op : binop) (a1 a2 : value) : option value := match op with - | Plus => a1 + a2 - | Minus => a1 - a2 - | Times => a1 * a2 + | 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) : nat := +(* Fixpoint eval_expr (s : state) (e : expr) : option value := match e with - | Lit n => n + | 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. -- cgit