revert the last interface change, using a separate printer is enough

drivers/coq-realize.drv

+
+printer "coq-realize"
+filename "%f_%t_%g.v"
+
+valid 0
+unknown "Error: \\(.*\\)$" "\\1"
+fail "Syntax error: \\(.*\\)$" "\\1"
+time "why3cpulimit time : %s s"
+
+prelude "(* This file is generated by Why3's Coq driver *)"
+prelude "(* Beware! Only edit allowed sections below    *)"
+
+(* À discuter *)
+(*transformation "simplify_recursive_definition"*)
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_non_struct_recursion"
+
+transformation "eliminate_if"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification_in_goal"*)
+
+
+theory BuiltIn
+
+  prelude "Require Import ZArith."
+  prelude "Require Import Rbase."
+
+  syntax type   int   "Z"
+  syntax type   real  "R"
+  syntax predicate  (=)   "(%1 = %2)"
+end
+
+theory bool.Bool
+
+  syntax type bool   "bool"
+
+  syntax function True  "true"
+  syntax function False "false"
+
+  syntax function andb  "(andb %1 %2)"
+  syntax function orb   "(orb %1 %2)"
+  syntax function xorb  "(xorb %1 %2)"
+  syntax function notb  "(negb %1)"
+
+end
+
+
+theory int.Int
+
+  syntax function zero "0%Z"
+  syntax function one  "1%Z"
+
+  syntax function (+)  "(%1 + %2)%Z"
+  syntax function (-)  "(%1 - %2)%Z"
+  syntax function (*)  "(%1 * %2)%Z"
+  syntax function (-_) "(-%1)%Z"
+
+  syntax predicate (<=) "(%1 <= %2)%Z"
+  syntax predicate (<)  "(%1 <  %2)%Z"
+  syntax predicate (>=) "(%1 >= %2)%Z"
+  syntax predicate (>)  "(%1 >  %2)%Z"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+
+end
+
+theory int.Abs
+
+  syntax function abs "(Zabs %1)"
+
+  remove prop Abs_pos
+
+end
+
+theory int.MinMax
+
+  syntax function min "(Zmin %1 %2)"
+  syntax function max "(Zmax %1 %2)"
+
+end
+
+(* removed: Coq Zdiv is NOT true Euclidean division:
+   Zmod can be negative, in fact (Zmod x y) has the same sign as y,
+   which is not the usual convention of programming language either. 
+
+theory int.EuclideanDivision
+
+  prelude "Require Import Zdiv."
+
+  syntax function div "(Zdiv %1 %2)"
+  syntax function mod "(Zmod %1 %2)"
+
+  remove prop Div_mod
+  remove prop Div_bound
+  remove prop Mod_bound
+  remove prop Mod_1
+  remove prop Div_1
+
+end
+*)
+
+theory int.ComputerDivision
+
+  (* Coq Z0div provides the division and modulo operators
+     with the same convention as mainstream programming language
+     such C, Java, OCaml *)
+
+  prelude "Require Import ZOdiv."
+
+  syntax function div "(ZOdiv %1 %2)"
+  syntax function mod "(ZOmod %1 %2)"
+
+  remove prop Div_mod
+  remove prop Div_bound
+  remove prop Mod_bound
+  remove prop Div_sign_pos
+  remove prop Div_sign_neg
+  remove prop Mod_sign_pos
+  remove prop Mod_sign_neg
+  remove prop Rounds_toward_zero
+  remove prop Div_1
+  remove prop Mod_1
+  remove prop Div_inf
+  remove prop Mod_inf
+  remove prop Div_mult
+  remove prop Mod_mult
+
+end
+
+
+theory real.Real
+
+  syntax function zero "0%R"
+  syntax function one  "1%R"
+
+  syntax function (+)  "(%1 + %2)%R"
+  syntax function (-)  "(%1 - %2)%R"
+  syntax function (-_) "(-%1)%R"
+  syntax function (*)  "(%1 * %2)%R"
+  syntax function (/)  "(Rdiv %1 %2)%R"
+  syntax function inv  "(Rinv %1)"
+
+  syntax predicate (<=) "(%1 <= %2)%R"
+  syntax predicate (<)  "(%1 <  %2)%R"
+  syntax predicate (>=) "(%1 >= %2)%R"
+  syntax predicate (>)  "(%1 >  %2)%R"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop assoc_mul_div
+  remove prop assoc_div_mul
+  remove prop assoc_div_div
+
+end
+
+theory real.RealInfix
+
+  syntax function (+.)  "(%1 + %2)%R"
+  syntax function (-.)  "(%1 - %2)%R"
+  syntax function (-._) "(-%1)%R"
+  syntax function ( *.) "(%1 * %2)%R"
+  syntax function (/.)  "(%1 / %2)%R"
+
+  syntax predicate (<=.) "(%1 <= %2)%R"
+  syntax predicate (<.)  "(%1 <  %2)%R"
+  syntax predicate (>=.) "(%1 >= %2)%R"
+  syntax predicate (>.)  "(%1 >  %2)%R"
+
+end
+
+theory real.Abs
+
+  prelude "Require Import Rbasic_fun."
+
+  syntax function abs "(Rabs %1)"
+
+  remove prop Abs_le
+  remove prop Abs_pos
+
+end
+
+theory real.FromInt
+
+  syntax function from_int "(IZR %1)"
+
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+
+end
+
+theory real.Square
+
+  prelude "Require Import R_sqrt."
+
+  syntax function sqr  "(Rsqr %1)"
+  syntax function sqrt "(sqrt %1)"  (* and not Rsqrt *)
+
+  remove prop Sqrt_positive
+  remove prop Sqrt_square
+  remove prop Square_sqrt
+
+end
+
+
+theory real.ExpLog
+
+  prelude "Require Import Rtrigo_def."
+  prelude "Require Import Rpower."
+
+  syntax function exp "(exp %1)"
+  syntax function log "(ln %1)"
+
+  remove prop Exp_zero
+  remove prop Exp_sum
+  remove prop Log_one
+  remove prop Log_mul
+  remove prop Log_exp
+  remove prop Exp_log
+
+end
+
+
+theory real.Power
+
+  prelude "Require Import Rpower."
+
+  (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
+end
+
+theory real.Trigonometry
+
+  prelude "Require Import Rtrigo."
+  prelude "Require Import AltSeries. (* for def of pi *)"
+
+  syntax function cos "(Rtrigo_def.cos %1)"
+  syntax function sin "(Rtrigo_def.sin %1)"
+
+  syntax function pi "PI"
+
+  syntax function tan "(Rtrigo.tan %1)"
+  (* syntax function atan "atan not defined in Coq ?" *)
+
+  remove prop Pythagorean_identity
+  remove prop Cos_le_one
+  remove prop Sin_le_one
+  remove prop Cos_0
+  remove prop Sin_0
+  remove prop Cos_pi
+  remove prop Sin_pi
+  remove prop Cos_pi2
+  remove prop Sin_pi2
+
+end

src/core/printer.ml

@@ -33,7 +33,7 @@ type prelude_map = prelude Mid.t
 
 type 'a pp = formatter -> 'a -> unit
 
-type printer = Env.env -> prelude -> prelude_map -> ?realize:bool -> ?old:in_channel -> task pp
+type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
 
 let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
 
@@ -50,7 +50,7 @@ let lookup_printer s =
 
 let list_printers ()  = Hashtbl.fold (fun k _ acc -> k::acc) printers []
 
-let () = register_printer "(null)" (fun _ _ _ ?realize:_ ?old:_ _ _ -> ())
+let () = register_printer "(null)" (fun _ _ _ ?old:_ _ _ -> ())
 
 (** Syntax substitutions *)
 

src/core/printer.mli

@@ -31,7 +31,7 @@ type prelude_map = prelude Mid.t
 
 type 'a pp = Format.formatter -> 'a -> unit
 
-type printer = Env.env -> prelude -> prelude_map -> ?realize:bool -> ?old:in_channel -> task pp
+type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
 
 val register_printer : string -> printer -> unit
 

src/driver/driver.ml

@@ -280,7 +280,7 @@ let prepare_task drv task =
   let task = update_task drv task in
   List.fold_left apply task transl
 
-let print_task_prepared ?realize ?old drv fmt task =
+let print_task_prepared ?old drv fmt task =
   let p = match drv.drv_printer with
     | None -> raise NoPrinter
     | Some p -> p
@@ -288,15 +288,15 @@ let print_task_prepared ?realize ?old drv fmt task =
   let printer =
     lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
   in
-  fprintf fmt "@[%a@]@?" (printer ?realize ?old) task
+  fprintf fmt "@[%a@]@?" (printer ?old) task
 
-let print_task ?realize ?old drv fmt task =
+let print_task ?old drv fmt task =
   let task = prepare_task drv task in
-  print_task_prepared ?realize ?old drv fmt task
+  print_task_prepared ?old drv fmt task
 
 let print_theory ?old drv fmt th =
   let task = Task.use_export None th in
-  print_task ~realize:true ?old drv fmt task
+  print_task ?old drv fmt task
 
 let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
   let buf = Buffer.create 1024 in

src/driver/driver.mli

@@ -45,7 +45,6 @@ val call_on_buffer :
 
 
 val print_task :
-  ?realize   : bool ->
   ?old       : in_channel ->
   driver -> Format.formatter -> Task.task -> unit
 
@@ -65,7 +64,6 @@ val prove_task :
 val prepare_task : driver -> Task.task -> Task.task
 
 val print_task_prepared :
-  ?realize   : bool ->
   ?old       : in_channel ->
   driver -> Format.formatter -> Task.task -> unit
 

src/printer/alt_ergo.ml

@@ -248,7 +248,7 @@ let print_task_old pr thpr fmt task =
   fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
 
 let () = register_printer "alt-ergo-old"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task_old pr thpr fmt task)
 
@@ -261,7 +261,7 @@ let print_decls =
   Trans.on_tagged_ls meta_ac (fun ac ->
     Printer.sprint_decls (print ac))
 
-let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
+let print_task _env pr thpr ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is a no-no *)
   (* forget_all ident_printer; *)
   print_prelude fmt pr;

src/printer/coq.ml

@@ -376,11 +376,11 @@ let context_end = "(* DO NOT EDIT BELOW *)"
 (* current kind of script in an old file *)
 type old_file_state = InContext | InProof | NoWhere
 
-let copy_proof s ch fmt = 
+let copy_proof s ch fmt =
   copy_user_script proof_begin proof_end ch fmt;
   s := NoWhere
 
-let copy_context s ch fmt = 
+let copy_context s ch fmt =
   copy_user_script context_begin context_end ch fmt;
   s := NoWhere
 
@@ -665,19 +665,19 @@ let init_printer th =
   Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
   pr
 
-let print_task _env pr thpr ?realize ?old fmt task =
+let print_task _env pr thpr realize ?old fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
-  let realization,decls = 
-    if realize = Some true then
+  let realization,decls =
+    if realize then
       let used = Task.used_theories task in
       (* 2 cases: goal is clone T with [] or goal is a real goal *)
       let used = match task with
         | None -> assert false
         | Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
             Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
-            Mid.remove th.Theory.th_name used 
+            Mid.remove th.Theory.th_name used
         | _ -> used
       in
       let symbols = Task.used_symbols used in
@@ -703,9 +703,14 @@ let print_task _env pr thpr ?realize ?old fmt task =
   in
   print_decls ~old info fmt decls
 
-let () = register_printer "coq" print_task
+let print_task_full env pr thpr ?old fmt task =
+  print_task env pr thpr false ?old fmt task
 
+let print_task_real env pr thpr ?old fmt task =
+  print_task env pr thpr true  ?old fmt task
 
+let () = register_printer "coq" print_task_full
+let () = register_printer "coq-realize" print_task_real
 
 (* specific printer for realization of theories *)
 (* OBSOLETE

src/printer/cvc3.ml

@@ -331,6 +331,6 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "cvc3"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr fmt task)

src/printer/gappa.ml

@@ -407,7 +407,7 @@ let print_goal info fmt g =
         fprintf fmt "# (no goal at all ??)@\n";
         fprintf fmt "1 in [0,0]@\n"
 
-let print_task env pr thpr ?realize:_ ?old:_ fmt task =
+let print_task env pr thpr ?old:_ fmt task =
   forget_all ident_printer;
   let info = get_info env task in
   print_prelude fmt pr;

src/printer/simplify.ml

@@ -179,7 +179,7 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "simplify"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr fmt task)
 

src/printer/smtv1.ml

@@ -242,6 +242,6 @@ let print_task pr thpr fmt task =
   fprintf fmt "@\n)@."
 
 let () = register_printer "smtv1"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr fmt task)

src/printer/smtv2.ml

@@ -338,7 +338,7 @@ let print_task_old pr thpr fmt task =
   fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
 
 let () = register_printer "smtv2"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task_old pr thpr fmt task)
 
@@ -357,7 +357,7 @@ let print_decls =
   Trans.on_meta Discriminate.meta_lsinst (fun dls ->
     Printer.sprint_decls (print dls))
 
-let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
+let print_task _env pr thpr ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is taboo *)
   (* forget_all ident_printer; *)
   print_prelude fmt pr;

src/printer/tptp.ml

@@ -147,7 +147,7 @@ let print_task pr thpr fmt task =
     (print_decl info) fmt (Task.task_decls task))
 
 let () = register_printer "tptp"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr fmt task)
 

src/printer/why3printer.ml

@@ -372,7 +372,7 @@ let print_tdecl fmt td = match td.td_node with
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
         m.meta_name (print_list comma print_meta_arg) al
 
-let print_task_old _env pr thpr ?realize:_ ?old:_ fmt task =
+let print_task_old _env pr thpr ?old:_ fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
@@ -386,7 +386,7 @@ let print_tdecls =
     print_tdecl fmt td in
   Printer.sprint_tdecls print
 
-let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
+let print_task _env pr thpr ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
   (* forget_all (); *)
   print_prelude fmt pr;

src/printer/yices.ml

@@ -331,6 +331,6 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "yices"
-  (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
+  (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr fmt task)