Model parser returning locations of terms.

src/core/model_parser.ml

@@ -11,8 +11,13 @@
 
 open Stdlib
 
+type model_element = { 
+  me_name     : string;
+  me_value    : string;
+  me_location : Loc.position option; 
+}
 
-type model_parser =  string -> Printer.printer_mapping -> (string * string) list
+type model_parser =  string -> Printer.printer_mapping -> model_element list
 
 type reg_model_parser = Pp.formatted * model_parser
 

src/core/model_parser.mli

@@ -9,7 +9,13 @@
 (*                                                                  *)
 (********************************************************************)
 
-type model_parser = string ->  Printer.printer_mapping -> (string * string) list
+type model_element = { 
+  me_name     : string;
+  me_value    : string;
+  me_location : Loc.position option; 
+}
+
+type model_parser = string ->  Printer.printer_mapping -> model_element list
 
 val register_model_parser : desc:Pp.formatted -> string -> model_parser -> unit
 

src/driver/call_provers.ml

@@ -10,6 +10,7 @@
 (********************************************************************)
 
 open Format
+open Model_parser
 
 let debug = Debug.register_info_flag "call_prover"
   ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
@@ -97,7 +98,7 @@ type prover_result = {
   pr_output : string;
   pr_time   : float;
   pr_steps  : int;		(* -1 if unknown *)
-  pr_model  : (string * string) list;
+  pr_model  : model_element list;
 }
 
 type prover_result_parser = {
@@ -158,8 +159,8 @@ let save f = f ^ ".save"
 let rec debug_print_model model =
   match model with
   | [] -> ()
-  | (term, value)::t -> begin
-    Debug.dprintf debug "Call_provers: model %s = %s@." term value;
+  | el::t -> begin
+    Debug.dprintf debug "Call_provers: model %s = %s@." el.me_name el.me_value;
     debug_print_model t;
   end
 

src/driver/call_provers.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Model_parser
+
 (** Call provers and parse their outputs *)
 
 type prover_answer =
@@ -39,8 +41,8 @@ type prover_result = {
   (** The time taken by the prover *)
   pr_steps  : int;
   (** The number of steps taken by the prover (-1 if not available) *)
-  (** The model produced by a the solver (pairs of term value) *)
-  pr_model  : (string * string) list;
+  (** The model produced by a the solver *)
+  pr_model  : model_element list;
 }
 
 val print_prover_answer : Format.formatter -> prover_answer -> unit

src/driver/parse_cvc4_z3_model.ml

@@ -14,6 +14,7 @@
 open Printer
 open Ident
 open Term
+open Model_parser
 
 exception EndOfStringExc;;
 
@@ -131,10 +132,15 @@ let rec get_terms_values_strings raw_strings terms collected_strings =
   match raw_strings with
   | [] -> collected_strings
   | (raw_term_string, value)::raw_strings_tail ->
-    let (term_string, terms_tail) = match terms with
-      | [] -> (raw_term_string, [])
-      | term::t_tail -> ((get_term_string term raw_term_string), t_tail) in
-    get_terms_values_strings raw_strings_tail terms_tail (collected_strings @ [(term_string, value)])
+    let (term_string, term_location, terms_tail) = match terms with
+      | [] -> (raw_term_string, None, [])
+      | term::t_tail -> ((get_term_string term raw_term_string), term.t_loc, t_tail) in
+    let new_model_element = { 
+      me_name = term_string; 
+      me_value = value; 
+      me_location = term_location} in
+    let collected_strings = collected_strings @ [new_model_element] in
+    get_terms_values_strings raw_strings_tail terms_tail collected_strings
 
 (* Parses the model returned by CVC4 or Z3.
 Assumes that the model has the following form "model: (pairs)"
@@ -150,5 +156,5 @@ let parse model printer_mapping =
 
 let _ = parse "dasfdfd dafsd ( dasfdf ) dfa unknown ((x 1))" Printer.get_default_printer_mapping
 
-let () = Model_parser.register_model_parser "cvc4_z3" parse
+let () = register_model_parser "cvc4_z3" parse
   ~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."

src/ide/gmain.ml

@@ -17,6 +17,7 @@ open Whyconf
 open Gconfig
 open Stdlib
 open Debug
+open Model_parser
 
 module C = Whyconf
 
@@ -560,8 +561,14 @@ 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
+  | m_element::t -> begin
+    let loc_string = match m_element.me_location with
+      | None -> "\"no location\""
+      | Some loc -> begin
+	Loc.report_position str_formatter loc;
+	flush_str_formatter ()
+      end in
+    let n_str = str ^ m_element.me_name ^ " at " ^ loc_string ^ " = " ^ m_element.me_value ^ "\n" in
     add_model n_str t
   end