Improve the Coq sources and add extraction

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.