Display counterexample in a tab.

src/driver/call_provers.ml

@@ -163,15 +163,7 @@ let rec debug_print_model model =
     debug_print_model t;
   end
 
-let rec add_model str model =
-  match model with
-  | [] -> str
-  | (term, value)::t -> begin
-    let n_str = str ^ term ^ " = " ^ value ^ "\n" in
-    add_model n_str t
-  end
-
-let parse_prover_run res_parser time out ret on_timelimit timelimit =
+let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
   let ans = match ret with
     | Unix.WSTOPPED n ->
         Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
@@ -192,14 +184,13 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
       && time >= (0.9 *. float timelimit) -> Timeout
     | _ -> ans
   in
-  let model = res_parser.prp_model_parser out in
-  let out_with_model = add_model (out^"\nModel:\n") model
-  in
+  let model = res_parser.prp_model_parser out printer_mapping in
+  (* let out_with_model = add_model (out^"\nModel:\n") model in *)
   Debug.dprintf debug "Call_provers: model:@.";
   debug_print_model model;
   { pr_answer = ans;
     pr_status = ret;
-    pr_output = out_with_model;
+    pr_output = out;
     pr_time   = time;
     pr_steps  = steps;
     pr_model  = model;
@@ -230,8 +221,9 @@ let actualcommand command timelimit memlimit stepslimit file =
   List.map (Str.global_substitute cmd_regexp replace) arglist,
   !use_stdin, !on_timelimit
 
-let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
+let  call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
                  ~res_parser
+		 ~printer_mapping
                  ?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
 
   let command, use_stdin, on_timelimit =
@@ -277,12 +269,13 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
           if inplace then swallow (Sys.rename (save fin)) fin;
           if redirect then swallow Sys.remove fout
         end;
-        parse_prover_run res_parser time out ret on_timelimit timelimit
+        parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping
     in
     { call = call; pid = pid }
 
 let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
                    ~res_parser ~filename
+		   ~printer_mapping
                    ?(inplace=false) buffer =
 
   let fin,cin =
@@ -293,7 +286,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
       Filename.open_temp_file "why_" ("_" ^ filename) in
   Buffer.output_buffer cin buffer; close_out cin;
   call_on_file ~command ~timelimit ~memlimit ~stepslimit
-               ~res_parser ~cleanup:true ~inplace fin
+               ~res_parser ~printer_mapping ~cleanup:true ~inplace fin
 
 let query_call pc =
   let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in

src/ide/gmain.ml

@@ -347,6 +347,12 @@ let output_page,output_tab =
   3, GPack.vbox ~homogeneous:false ~packing:
     (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
 
+let counterexample_page,counterexample_tab =
+  let label = GMisc.label ~text:"Counter-example" () in
+  3, GPack.vbox ~homogeneous:false ~packing:
+    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
+
+
 let _ = GPack.hbox ~packing:(source_tab#pack ~expand:false) ()
 
 (******************)
@@ -389,6 +395,18 @@ let output_view =
     ~packing:scrolled_output_view#add
     ()
 
+let scrolled_counterexample_view =
+  GBin.scrolled_window
+    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
+    ~shadow_type:`ETCHED_OUT ~packing:counterexample_tab#add ()
+
+let counterexample_view =
+  GSourceView2.source_view
+    ~editable:false
+    ~show_line_numbers:true
+    ~packing:scrolled_counterexample_view#add
+    ()
+
 let modifiable_sans_font_views = ref [goals_view#misc]
 let modifiable_mono_font_views =
   ref [task_view#misc;edited_view#misc;output_view#misc]
@@ -539,6 +557,14 @@ let split_transformation = "split_goal_wp"
 let inline_transformation = "inline_goal"
 let intro_transformation = "introduce_premises"
 
+let rec add_model str model =
+  match model with
+  | [] -> str
+  | (term, value)::t -> begin
+    let n_str = str ^ term ^ " = " ^ value ^ "\n" in
+    add_model n_str t
+  end
+
 let goal_task_text g =
   if (Gconfig.config ()).intro_premises then
     let trans =
@@ -608,11 +634,23 @@ let update_tabs a =
       (Pp.string_of (Pp.hov 2 print) m.S.metas_added)
     | _ -> ""
  in
+  let counterexample_text = 
+    match a with
+    | S.Proof_attempt a ->
+      begin
+        match a.S.proof_state with
+	  | S.Done r ->
+            add_model "" r.Call_provers.pr_model
+	  | _ -> "" 
+      end
+    | _ -> ""
+  in
  task_view#source_buffer#set_text task_text;
  task_view#scroll_to_mark `INSERT;
  edited_view#source_buffer#set_text edited_text;
  edited_view#scroll_to_mark `INSERT;
- output_view#source_buffer#set_text output_text
+ output_view#source_buffer#set_text output_text;
+ counterexample_view#source_buffer#set_text counterexample_text