coq driver

Makefile.in

@@ -172,7 +172,11 @@ test: bin/why.byte  $(TOOLS)
 		--call --goal Test.G src/test.why --timeout 3
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
 		--output-file tmp.v --goal Test.G src/test.why 
-	coqc -require ZArith tmp.v
+	bin/why.byte --call --driver drivers/alt_ergo.drv -I theories/ \
+		--goal ExpLog.Log_e theories/real.why 
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-file tmp.v --goal ExpLog.Log_e theories/real.why 
+	coqc tmp.v
 
 testl: bin/whyl.byte
 	ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw

drivers/coq.drv

@@ -3,7 +3,13 @@ printer "coq"
 filename "%f_%t_%s.v"
 call_on_file "coqc %s"
 
+
+
 theory BuiltIn
+
+  prelude "Require Import ZArith."
+  prelude "Require Import Rbase."
+
   syntax type   int     "Z"
   syntax type   real    "R"
   syntax logic  (_=_)   "(%1 = %2)"
@@ -13,7 +19,7 @@ end
 
 theory int.Int
 
-  prelude "Require ZArith."
+  prelude "Require Import ZArith."
 
   syntax logic zero "0%Z"
   syntax logic one "1%Z"

src/driver/driver.ml

@@ -101,7 +101,7 @@ type prover_answer =
   | HighFailure
 
 type theory_driver = {
-  thd_prelude : string option;
+  thd_prelude : string list;
   thd_tsymbol : unit ;
 }
 
@@ -128,7 +128,7 @@ type printer = driver -> formatter -> task -> unit
 and raw_driver = {
   drv_printer     : printer option;
   drv_prover      : Call_provers.prover;
-  drv_prelude     : string option;
+  drv_prelude     : string list;
   drv_filename    : string option;
   drv_transforms  : task tlist_reg;
   drv_rules       : theory_rules list;
@@ -138,7 +138,7 @@ and driver = {
   drv_raw : raw_driver;
   drv_clone : clone;
   drv_env : env;
-  drv_thprelude   : string Hid.t;
+  drv_thprelude   : string list Hid.t;
   (* the first is the translation only for this ident, the second is
      also for representant *)
   drv_theory      : (translation * translation) Hid.t;
@@ -289,14 +289,18 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
           with Not_found -> errorm ~loc "Unknown proposition %s" 
             (string_of_qualid qualid q)
         end
-    | Rprelude (loc,s) -> if Hid.mem driver.drv_thprelude th.th_name
-      then errorm ~loc "duplicate prelude"
-      else Hid.add driver.drv_thprelude th.th_name s in
+    | Rprelude (loc,s) -> 
+        let l = 
+          try Hid.find driver.drv_thprelude th.th_name 
+          with Not_found -> []
+        in
+        Hid.replace driver.drv_thprelude th.th_name (s::l) 
+  in
   List.iter add trl
 
 let load_driver file env =
   let f = load_file file in
-  let prelude     = ref None in
+  let prelude     = ref [] in
   let printer     = ref None in
   let call_stdin  = ref None in
   let call_file   = ref None in
@@ -313,7 +317,7 @@ let load_driver file env =
 	printer := Some (Hashtbl.find printers s)
     | Printer s -> 
 	errorm ~loc "unknown printer %s" s 
-    | Prelude s -> set_or_raise loc prelude s "prelude"
+    | Prelude s -> prelude := s :: !prelude
     | CallStdin s -> set_or_raise loc call_stdin s "callstdin"
     | CallFile s -> set_or_raise loc call_file s "callfile"
     | RegexpValid s -> regexps:=(s,Valid)::!regexps

src/printer/coq.ml

@@ -165,8 +165,10 @@ and print_tnode opl opr drv fmt t = match t.t_node with
       assert false
   | Tvar v ->
       print_vs fmt v
-  | Tconst c ->
-      Pretty.print_const fmt c
+  | Tconst (ConstInt n) -> fprintf fmt "%s%%Z" n
+  | Tconst (ConstReal c) -> 
+      Print_real.print_with_integers
+	"(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c
   | Tlet (t1,tb) ->
       let v,t2 = t_open_bound tb in
       fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
@@ -333,6 +335,7 @@ let print_decls drv fmt dl =
 let print_context drv fmt task =
   forget_all (); 
   fprintf fmt "(* beginning of generated file *)@\n@\n";
+  fprintf fmt "Require Import ZArith.@\n@\n";
   print_decls drv fmt (Task.task_decls task);
   fprintf fmt "(* end of generated file *)@."
 

src/printer/print_real.mli

@@ -20,3 +20,9 @@
 open Format
 
 val print : formatter -> Term.real_constant -> unit
+
+val print_with_integers : 
+  (string -> 'a, Format.formatter, unit) format ->
+  (string -> string -> 'a, Format.formatter, unit) format ->
+  (string -> string -> 'a, Format.formatter, unit) format ->
+  Format.formatter -> Term.real_constant -> 'a