connection de call_prover dans le main

src/core/theory.ml

@@ -956,3 +956,10 @@ let print_ctxt fmt ctxt =
 
 let print_th fmt th = fprintf fmt "<theory (TODO>"
 
+(* Utils *)
+exception NotGoalContext
+
+let goal_of_ctxt ctxt =
+  match ctxt.ctxt_decl.d_node with
+    | Dprop (Pgoal,pr) -> pr
+    | _ -> raise NotGoalContext

src/core/theory.mli

@@ -216,3 +216,10 @@ val print_ident : Format.formatter -> ident -> unit
 val print_uc : Format.formatter -> theory_uc -> unit
 val print_ctxt : Format.formatter -> context -> unit
 val print_th : Format.formatter -> theory -> unit
+
+(* Utils *)
+
+exception NotGoalContext
+val goal_of_ctxt : context -> prop 
+(* goal_of_ctxt ctxt return the goal of a goal context
+   the ctxt must end with a goal.*)

src/main.ml

@@ -64,8 +64,13 @@ let () =
 let () = 
   match !output with
     | None when not !call -> type_only := true
+    | Some _ when !call -> 
+        eprintf "--output and --call can't be use at the same time.(Whynot?)@.";
+        exit 1
     | _ -> ()
 
+let timeout = if !timeout <= 0 then None else Some !timeout
+
 (*
 let transformation l = 
   let t1 = Simplify_recursive_definition.t in
@@ -176,14 +181,21 @@ let do_file env drv filename_printer file =
                                | Dprop (_,{pr_name = pr_name}) -> 
                                    Ident.derived_from pr_name pr.pr_name
                                | _ -> assert false) goals in
-      let file = 
-        let file = Filename.basename file in
-        let file = Filename.chop_extension file in
-        Ident.id_unique filename_printer 
-          (Ident.id_register (Ident.id_fresh file)) in
       match !output with
-        | None -> ()
+        | None (* we are in the call mode *) -> 
+            let call (th,ctxt) = 
+              let res = Driver.call_prover ~debug:!debug ?timeout drv ctxt in
+              printf "%s %s %s : %a@." 
+                file th.th_name.Ident.id_short 
+                (goal_of_ctxt ctxt).pr_name.Ident.id_long
+                Call_provers.print_prover_result res in
+            List.iter call goals
         | Some dir -> 
+            let file = 
+              let file = Filename.basename file in
+              let file = Filename.chop_extension file in
+              Ident.id_unique filename_printer 
+                (Ident.id_register (Ident.id_fresh file)) in
             let ident_printer = Ident.create_ident_printer 
               ~sanitizer:file_sanitizer [] in
             List.iter 

src/output/call_provers.ml

@@ -17,6 +17,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Format
+
 type prover_answer = 
   | Valid
   | Invalid
@@ -25,12 +27,23 @@ type prover_answer =
   | Timeout
   | HighFailure
 
+let print_prover_answer fmt = function
+  | Valid -> fprintf fmt "Valid"
+  | Invalid -> fprintf fmt "Invalid"
+  | Unknown s -> pp_print_string fmt s
+  | Failure s -> pp_print_string fmt s
+  | Timeout -> fprintf fmt "Timeout"
+  | HighFailure -> fprintf fmt "HighFailure"
+
 type prover_result =
     { pr_time   : float;
       pr_answer : prover_answer;
       pr_stderr : string;
       pr_stdout : string}
 
+let print_prover_result fmt pr = 
+  fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time
+
 type prover =
     { pr_call_stdin : string option; (* %f pour le nom du fichier *)
       pr_call_file  : string option;
@@ -67,7 +80,7 @@ let timed_sys_command ?stdin ?(debug=false) ?timeout cmd =
   let ret = Unix.close_process p in
   let t1 = Unix.times () in
   let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
-  if debug then Format.eprintf "Calldp : Command output : %s@." out;
+  if debug then Format.eprintf "Call_provers : Command output : %s@." out;
   (cpu_time,ret,out)
 
 let grep re str =

src/output/call_provers.mli

@@ -16,6 +16,7 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
+open Format
 
 type prover_answer = 
   | Valid
@@ -25,12 +26,16 @@ type prover_answer =
   | Timeout
   | HighFailure
 
+val print_prover_answer : formatter -> prover_answer -> unit
+
 type prover_result =
     { pr_time   : float;
       pr_answer : prover_answer;
       pr_stderr : string;
       pr_stdout : string}
 
+val print_prover_result : formatter -> prover_result -> unit
+
 type prover =
     { pr_call_stdin : string option; (* %f pour le nom du fichier *)
       pr_call_file  : string option;

src/output/driver.ml

@@ -123,9 +123,7 @@ type printer = driver -> formatter -> context -> unit
 and driver = {
   drv_printer    : printer option;
   drv_context    : context;
-  drv_call_stdin : string option;
-  drv_call_file  : string option;
-  drv_regexps    : (string * prover_answer) list;
+  drv_prover     : Call_provers.prover;
   drv_prelude    : string option;
   drv_filename   : string option;
   drv_rules      : theory_rules list;
@@ -287,12 +285,13 @@ let load_driver file env =
     | RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
     | Filename s -> set_or_raise loc filename s "filename"
   in
+  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
   List.iter add f.f_global;
   { drv_printer    = !printer;
     drv_context    = Context.init_context env;
-    drv_call_stdin = !call_stdin;
-    drv_call_file  = !call_file;
-    drv_regexps    = !regexps;
+    drv_prover     = {Call_provers.pr_call_stdin = !call_stdin;
+                      pr_call_file               = !call_file;
+                      pr_regexps                 = regexps};
     drv_prelude    = !prelude;
     drv_filename   = !filename;
     drv_rules      = f.f_rules;
@@ -343,9 +342,7 @@ let filename_of_goal drv ident_printer filename theory_name ctxt =
   match drv.drv_filename with
     | None -> errorm "no filename syntax given"
     | Some f -> 
-        let pr_name = match ctxt.ctxt_decl.d_node with
-          | Dprop (Pgoal,{pr_name=pr_name}) -> pr_name
-          | _ -> errorm "the bottom of this context is not a goal" in
+        let pr_name = (goal_of_ctxt ctxt).pr_name in
         let repl_fun s = 
           let i = matched_group 1 s in
           match i with
@@ -355,10 +352,24 @@ let filename_of_goal drv ident_printer filename theory_name ctxt =
             | _ -> errorm "substitution variable are only %%f %%t and %%s" in
         global_substitute regexp_filename repl_fun f
 
+let file_printer = 
+  create_ident_printer ~sanitizer:(sanitizer char_to_alnumus char_to_alnumus)
+    []
 
-let call_prover drv ctx = assert false (*TODO*)
-let call_prover_on_file drv filename = assert false (*TODO*)
-let call_prover_on_channel drv filename ic = assert false (*TODO*)
+let call_prover_on_file ?debug ?timeout drv filename =
+  Call_provers.on_file drv.drv_prover filename 
+let call_prover_on_buffer ?debug ?timeout ?filename drv ib = 
+  Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib 
+
+
+let call_prover ?debug ?timeout drv ctx =
+  let filename = 
+    match drv.drv_filename with
+      | None -> None
+      | Some _ -> Some (filename_of_goal drv file_printer "" "" ctx) in
+  let buffer = Buffer.create 128 in
+  bprintf buffer "%a@?" (print_context drv) ctx;
+  call_prover_on_buffer ?debug ?timeout ?filename drv buffer
 
 
 

src/output/driver.mli

@@ -61,9 +61,29 @@ type prover_answer =
   | Timeout
   | HighFailure
 
-val call_prover : driver -> context -> prover_answer
-val call_prover_on_file : driver -> string -> prover_answer
-val call_prover_on_channel : driver -> string -> in_channel -> prover_answer
+val call_prover : 
+  ?debug:bool -> (* if on print on stderr the commandline 
+                    and the output of the prover *)
+  ?timeout:int -> (* specify the time limit given to the prover,
+                     if not set unlimited time *)
+  driver ->       (* the driver to use *)
+  context ->      (* the context to prove with a goal as the last declaration *)
+  Call_provers.prover_result
+
+val call_prover_on_file : 
+  ?debug:bool -> 
+  ?timeout:int -> 
+  driver -> 
+  string -> 
+    Call_provers.prover_result
+
+val call_prover_on_buffer : 
+  ?debug:bool -> 
+  ?timeout:int -> 
+  ?filename:string -> 
+  driver -> 
+  Buffer.t -> 
+  Call_provers.prover_result
 
 (* error reporting *)