Interleaving counter-example model with source code.

src/core/model_parser.ml

@@ -98,11 +98,12 @@ let create_model_element ~name ~value ?location ?term () =
     me_term = term;
   }
 
+(*
 let print_location fmt m_element =
     match m_element.me_location with
     | None -> fprintf fmt "\"no location\""
     | Some loc -> Loc.report_position fmt loc
-
+*)
 
 (*
 *************************************************************** 
@@ -129,16 +130,24 @@ type raw_model_parser =  string -> model_element list
 *)
 
 let print_model_element fmt m_element =
-  fprintf fmt  "    %s = %a\n" 
+  fprintf fmt  "%s = %a" 
       m_element.me_name print_model_value m_element.me_value
 
-let print_model_elements fmt line m_elements =
-  fprintf fmt "  Line %d:\n" line;
-  List.iter (print_model_element fmt) m_elements
+let print_model_elements ?(delimiter = "\n") fmt m_elements =
+  List.iter 
+    (fun m_element ->
+      print_model_element fmt m_element;
+      fprintf fmt "%s" delimiter
+    ) 
+    m_elements
 
 let print_model_file fmt filename model_file =
   fprintf fmt "File %s:\n" filename;
-  IntMap.iter (print_model_elements fmt) model_file
+  IntMap.iter 
+    (fun line m_elements ->
+      fprintf fmt "Line %d:\n" line;
+      print_model_elements fmt m_elements) 
+    model_file
 
 let print_model fmt model =
   StringMap.iter (print_model_file fmt) model
@@ -159,6 +168,51 @@ let get_elements model_file line_number =
   with Not_found ->
     []
 
+let make_int_to_line_map lines =
+  let (map, _) = List.fold_left
+    (fun (map, num_line) line -> (IntMap.add num_line line map, num_line+1))
+    (IntMap.empty, 1) 
+    lines in
+  map
+
+let get_padding line =
+  try 
+    let r = Str.regexp " *" in
+    ignore (Str.search_forward r line 0);
+    Str.matched_string line
+  with Not_found -> ""
+
+let interleave_line model_file (source_code, line_number) line =
+  try
+    let model_elements = IntMap.find line_number model_file in
+
+    print_model_elements str_formatter model_elements ~delimiter:"; ";
+    let line_model = 
+      (get_padding line) ^
+	"(* " ^ 
+	(flush_str_formatter ()) ^ 
+	"*)" in
+
+    (source_code ^ line_model ^ "\n" ^ line, line_number + 1)
+  with Not_found ->
+    (source_code ^ line, line_number + 1)
+  
+
+let interleave_with_source model filename source_code =
+  try
+    let model_file = StringMap.find  filename model in
+    (*let (_, model_file) = StringMap.choose model in*)
+    let lines = Str.split (Str.regexp "^") source_code in
+    (*let int_to_line_map = make_int_to_line_map lines in*)
+    let (source_code, _) = List.fold_left
+    (interleave_line model_file)
+    ("", 1)
+    lines in
+    source_code
+  with Not_found ->
+    source_code
+  
+
 (*
 *************************************************************** 
 **  Building the model from raw model

src/core/model_parser.mli

@@ -102,6 +102,7 @@ val print_model : Format.formatter -> model -> unit
 
 val model_to_string : model -> string
 
+val interleave_with_source : model -> string -> string -> string
 
 (*
 *************************************************************** 

src/ide/gmain.ml

@@ -366,6 +366,8 @@ let () =
 (* views          *)
 (******************)
 
+let current_file = ref ""
+
 let scrolled_task_view =
   GBin.scrolled_window
     ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
@@ -643,18 +645,28 @@ let update_tabs a =
       begin
         match a.S.proof_state with
 	  | S.Done r ->
-	    Model_parser.model_to_string r.Call_provers.pr_model
+	    Model_parser.model_to_string r.Call_provers.pr_model ^ "\n" ^
+	    (Model_parser.interleave_with_source 
+	      r.Call_provers.pr_model
+	      !current_file
+	      (Sysutil.file_contents !current_file))
 	  | _ -> ""
       end
     | _ -> ""
   in
+  (*
+  let counterexample_text =
+    try 
+      Sysutil.file_contents !current_file
+    with _  -> "" 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;
- counterexample_view#source_buffer#set_text counterexample_text;
+  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;
+  counterexample_view#source_buffer#set_text counterexample_text;
 
 
 
@@ -1899,8 +1911,6 @@ let () = source_view#set_highlight_current_line true
 let () = source_view#source_buffer#set_text (source_text fname)
 *)
 
-let current_file = ref ""
-
 let set_current_file f =
   current_file := f;
   file_info#set_text ("file: " ^ !current_file)

src/session/session.ml

@@ -1194,7 +1194,7 @@ let load_result r =
           Call_provers.pr_output = "";
           Call_provers.pr_status = Unix.WEXITED 0;
 	  Call_provers.pr_steps = steps;
-	  Call_provers.pr_model = []
+	  Call_provers.pr_model = Model_parser.empty_model
         }
     | "undone" -> Interrupted
     | "unedited" -> Unedited

src/session/session_scheduler.ml

@@ -294,7 +294,7 @@ let schedule_edition t command filename callback =
       Call_provers.prp_regexps = [];
       Call_provers.prp_timeregexps = [];
       Call_provers.prp_stepregexps = [];
-      Call_provers.prp_model_parser = fun _ _ -> [] 
+      Call_provers.prp_model_parser = fun _ _ -> Model_parser.empty_model 
     } in
   let precall =
     Call_provers.call_on_file ~command ~res_parser ~redirect:false filename ~printer_mapping:Printer.get_default_printer_mapping in