Added a complete extraction example

Author: monadius

cw_example_extraction/Makefile

@@ -0,0 +1,7 @@
+all:
+	coqc Preloaded.v
+	coqc Solution.v
+	coqc -I ../src -Q ../theories CW SolutionTest.v
+
+clean:
+	rm -f *.o *.cmx *.cmi *.vo *.glob a.out *.ml *.mli

cw_example_extraction/Preloaded.v

@@ -0,0 +1,5 @@
+Fixpoint factorial n :=
+  match n with
+  | O => 1
+  | S n => S n * factorial n
+  end.

cw_example_extraction/Solution.v

@@ -0,0 +1,40 @@
+Require Solution.
+Require Import Preloaded.
+Require Coq.extraction.Extraction.
+From CW Require Import Loader.
+
+Extract Inductive nat => "int"
+  ["0" "(fun x -> x + 1)"]
+  "(fun zero succ n -> if n = 0 then zero () else succ (n - 1))".
+
+Extract Constant plus => "( + )".
+Extract Constant mult => "( * )".
+
+CWTest "Successful Extraction Test".
+
+Extraction "factorial.ml" Solution.factorial.
+
+CWCompileAndRun "factorial.mli" "factorial.ml" Options Driver "
+open Factorial
+let () = 
+  assert (factorial 3 = 6);
+  assert (factorial 0 = 1);
+  assert (factorial 5 = 120)
+".
+
+CWTest "Extraction Test With Errors".
+
+Extract Constant mult => "*".
+
+Extraction "factorial.ml" Solution.factorial.
+
+CWCompileAndRun "factorial.mli" "factorial.ml" Options Driver "
+open Factorial
+let () = 
+  assert (factorial 3 = 6);
+  assert (factorial 0 = 1);
+  assert (factorial 5 = 120)
+".
+
+CWEndTest.
+

cw_example_extraction/SolutionTest.v

@@ -137,20 +137,25 @@ let test_file_regex ?(fname = solution_file) match_flag regex =
     CErrors.user_err (str "Bad match")
   end
 
-let run_system_command args =
+let run_system_command ?err_msg args =
   let cmd = String.concat " " args in
   Printf.printf "Running: %s" cmd;
   match Unix.system cmd with
-  | Unix.WEXITED 0 -> passed "OK"
-  | _ -> failed "Failed"
+  | Unix.WEXITED 0 -> ()
+  | _ ->
+    let msg = match err_msg with None -> "Failed" | Some msg -> msg in
+    failed msg;
+    CErrors.user_err (str msg)
 
 let write_file fname str =
   let oc = open_out fname in
   Printf.fprintf oc "%s" str;
   close_out oc
 
+(** Compiles and runs the given OCaml source files *)
 let compile_and_run files ?(options = "") driver_code =
   write_file driver_file driver_code;
-  run_system_command ([ocaml_compiler; options] @ files @ [driver_file]);
+  run_system_command ~err_msg:"Compilation failed" ([ocaml_compiler; options] @ files @ [driver_file]);
+  passed "OK";
   run_system_command ["./a.out"];
   passed "OK"