[models] Actually print values, not terms

This patch makes it so that the model values that we print are actually
values, not terms (i.e. they do not contain variables).  This is
achieved by aggressively substituting variable definitions when
printing.

The patch is a bit more involved than I'd have liked, because we can't
simply substitute semantic values into terms, so the guts of the model
printing had to be changed a little.

The code now works in two pass. In the first pass, we build a hash table
from symbols (constants and arrays) to their respective definitions
using the new `value_defn` mini-language, which we then use for
printing. The substitution is performed on-the-fly in the second pass,
which actually prints, using the hash table that was built in the first
pass.

src/lib/frontend/models.ml

@@ -41,13 +41,14 @@ module E = Expr
 module ME = Expr.Map
 module SE = Expr.Set
 module MS = Map.Make(String)
+module MX = Shostak.MXH
 
 let constraints = ref MS.empty
 
 module Pp_smtlib_term = struct
 
   let to_string_type t =
-    asprintf "%a" Ty.print t
+    asprintf "%a" Ty.pp_smtlib t
 
   let rec print fmt t =
     let {E.f;xs;ty; _} = E.term_view t in
@@ -229,26 +230,24 @@ module Pp_smtlib_term = struct
 end
 
 module SmtlibCounterExample = struct
-
-  let x_print fmt (_ , ppr) = fprintf fmt "%s" ppr
-
   let pp_term fmt t =
     if Options.get_output_format () == Why3 then
       Pp_smtlib_term.print fmt t
     else
       E.print fmt t
 
-  let dummy_value_of_type ty =
+  let rec pp_dummy_value_of_type ppf ty =
     match ty with
-      Ty.Tint -> "0"
-    | Ty.Treal -> "0.0"
-    | Ty.Tbool -> "false"
-    | _ -> asprintf "%a" pp_term (Expr.fresh_name ty)
+      Ty.Tint -> Fmt.pf ppf "0"
+    | Ty.Treal -> Fmt.pf ppf "0.0"
+    | Ty.Tbool -> Fmt.pf ppf "false"
+    | Ty.Tfarray (_, rty) ->
+      Fmt.pf ppf "((as const %a) %a)" Ty.pp_smtlib ty pp_dummy_value_of_type rty
+    | _ -> Fmt.pf ppf "@@%a" pp_term (Expr.fresh_name ty)
 
   let pp_dummy_value_of_type fmt ty =
     if not (Options.get_interpretation_use_underscore ()) then
-      let d = dummy_value_of_type ty in
-      fprintf fmt "%s " d
+      pp_dummy_value_of_type fmt ty
     else
       fprintf fmt "_ "
 
@@ -316,43 +315,39 @@ module SmtlibCounterExample = struct
 
   let print_fun_def fmt name args ty t =
     let print_args fmt (ty,name) =
-      Format.fprintf fmt "(%s %a)" name Ty.print ty in
+      Format.fprintf fmt "(%s %a)" name Ty.pp_smtlib ty in
     let defined_value =
       try
-        let res,_,_ = (MS.find (Sy.to_string name) !constraints) in res
+        let res,_,_ = (MS.find (Sy.to_string name) !constraints) in
+        dprintf "%s" res
       with _ -> t
     in
 
     Format.fprintf fmt
-      "@ (define-fun %a (%a) %a %s)"
+      "@ (@[define-fun %a (%a) %a@ %t)@]"
       Sy.print name
       (Printer.pp_list_space (print_args)) args
-      Ty.print ty
+      Ty.pp_smtlib ty
       defined_value
 
-  let output_constants_counterexample ?(ignored = Sy.Set.empty) fmt records =
+  let output_constants_counterexample pp fmt records =
     ModelMap.iter
       (fun (f, xs_ty, ty) st ->
          assert (xs_ty == []);
-         begin match ty with
-           | Ty.Tfarray _ when Sy.Set.mem f ignored -> ()
-           | _ ->
-             match ModelMap.V.elements st with
-             | [[], rep] ->
-               let rep = Format.asprintf "%a" x_print rep in
-               let rep =
-                 match ty with
-                 | Ty.Trecord r ->
-                   let constr = mk_records_constr records f r in
-                   sprintf "(%s)" constr
-                 | _ -> rep
-               in
-
-               print_fun_def fmt f [] ty rep
-             | _ -> assert false
-         end)
-
-  let output_functions_counterexample fmt records fprofs =
+         match ModelMap.V.elements st with
+         | [[], rep] ->
+           let rep =
+             match ty with
+             | Ty.Trecord r ->
+               let constr = mk_records_constr records f r in
+               dprintf "(%s)" constr
+             | _ -> dprintf "%a" pp rep
+           in
+
+           print_fun_def fmt f [] ty rep
+         | _ -> assert false)
+
+  let output_functions_counterexample pp fmt records fprofs =
     let  records = ref records in
     ModelMap.iter
       (fun (f, xs_ty, ty) st ->
@@ -362,92 +357,68 @@ module SmtlibCounterExample = struct
 
          let rep =
            let representants =
-             ModelMap.V.fold (fun (xs_values,(_rep,srep)) acc ->
+             ModelMap.V.fold (fun (xs_values,(rep,srep)) acc ->
                  assert ((List.length xs_ty_named) = (List.length xs_values));
                  records :=
                    check_records !records xs_ty_named xs_values f ty srep;
-                 let reps = try MS.find srep acc with Not_found -> [] in
-                 MS.add srep (xs_values :: reps) acc
-               ) st MS.empty in
+                 let reps = try MX.find rep acc |> snd with Not_found -> [] in
+                 MX.add rep (srep, xs_values :: reps) acc
+               ) st MX.empty in
 
-           let representants = MS.fold (fun srep xs_values_list acc ->
-               (srep,xs_values_list) :: acc) representants [] in
+           let representants = MX.fold (fun rep (srep, xs_values_list) acc ->
+               ((rep, srep),xs_values_list) :: acc) representants [] in
 
            let rec mk_ite_and xs tys =
              match xs, tys with
              | [],[] -> assert false
-             | [xs,_],[_ty,name] ->
-               asprintf "(= %s %a)" name pp_term xs
-             | (xs,_) :: l1, (_ty,name) :: l2 ->
-               asprintf "(and (= %s %a) %s)"
+             | [_,rs],[_ty,name] ->
+               dprintf "(= %s %a)" name pp rs
+             | (_,rs) :: l1, (_ty,name) :: l2 ->
+               dprintf "(and (= %s %a) %t)"
                  name
-                 pp_term xs
+                 pp rs
                  (mk_ite_and l1 l2)
              | _, _ -> assert false
            in
 
            let mk_ite_or l =
              let pp_or_list fmt xs_values =
-               fprintf fmt "%s" (mk_ite_and xs_values xs_ty_named)
+               fprintf fmt "%t" (mk_ite_and xs_values xs_ty_named)
              in
              match l with
              | [] -> assert false
              | [xs_values] -> mk_ite_and xs_values xs_ty_named
              | xs_values :: l ->
-               asprintf "(or %s %a)"
+               dprintf "(or %t %a)"
                  (mk_ite_and xs_values xs_ty_named)
                  (Printer.pp_list_space pp_or_list) l
            in
 
            let rec reps_aux reps =
              match reps with
-             | [] -> asprintf "%a" pp_dummy_value_of_type ty
+             | [] -> dprintf "%a" pp_dummy_value_of_type ty
              | [srep,xs_values_list] ->
                if Options.get_interpretation_use_underscore () then
-                 asprintf "(ite %s %s %s)"
+                 dprintf "(@[<hv>ite %t@ %a@ %t)@]"
                    (mk_ite_or xs_values_list)
-                   srep
+                   pp srep
                    (reps_aux [])
                else
-                 srep
+                 dprintf "%a" pp srep
              | (srep,xs_values_list) :: l ->
-               asprintf "(ite %s %s %s)"
+               dprintf "(@[<hv>ite %t@ %a@ %t)@]"
                  (mk_ite_or xs_values_list)
-                 srep
+                 pp srep
                  (reps_aux l)
            in
            if List.length representants = 1 then
-             sprintf "%s" (fst (List.hd representants))
+             dprintf "%a" pp (fst (List.hd representants))
            else
              reps_aux representants
          in
          print_fun_def fmt f xs_ty_named ty rep;
       ) fprofs;
     !records
-
-  let output_arrays_counterexample fmt arrays =
-    let pp_array ppf (symbol, dty, st) =
-      let abstract =
-        Format.dprintf "(as @@%a %t)" Sy.print symbol dty
-      in
-      ModelMap.V.fold (fun (keys, (_value_r, value_s)) rst ->
-          Format.dprintf "(@[<hv>store@ %t@ %a %s)@]"
-            rst
-            Fmt.(list ~sep:sp (using (fun (_, (_, s)) -> s) string)) keys
-            value_s
-        ) st abstract ppf
-    in
-    let pp_array_ty ppf (args_ty, ret_ty) =
-      Format.fprintf ppf "(@[Array@ %a@ %a)@]"
-        Fmt.(list ~sep:sp Ty.print) args_ty
-        Ty.print ret_ty
-    in
-    ModelMap.iter
-      (fun (f, xs_ty, ty) st ->
-         let dty = Format.dprintf "%a" pp_array_ty (xs_ty, ty) in
-         Format.fprintf fmt "@ (@[define-fun %a () %t@ %a)@]"
-           Sy.print f dty pp_array (f, dty, st)) arrays
-
 end
 (* of module SmtlibCounterExample *)
 
@@ -475,6 +446,40 @@ module Why3CounterExample = struct
 end
 (* of module Why3CounterExample *)
 
+(* The [value_defn] type is a mini-language of the expressions that can occur in
+   constant values. *)
+type value_defn =
+  | Store of value_defn * value_defn * value_defn
+  (* An array store: [(store array key value)] *)
+  | Constant of Symbols.t * Ty.t
+  (* A constant of a given type. If the constant is defined in a model, it
+     must be resolved before being printed. *)
+  | Value of X.r * string
+  (* A leaf semantic value. This must be an actual value, i.e. it must not
+     contain any uninterpreted terms. *)
+
+let value (r, s) =
+  match X.term_extract r with
+  | Some t, _ ->
+    begin match E.term_view t with
+      | { f = Name _ as sy; _ } -> Constant (sy, X.type_info r)
+      | _ -> Value (r, s)
+    end
+  | _ ->
+    Value (r, s)
+
+let rec pp_value ppk ppf = function
+  | Store (a, k, v) ->
+    Format.fprintf ppf "(@[<hv>store@ %a@ %a %a)@]"
+      (pp_value ppk) a
+      (pp_value ppk) k
+      (pp_value ppk) v
+  | Constant (sy, t) -> ppk ppf (sy, t)
+  | Value (_, s) -> Format.pp_print_string ppf s
+
+let pp_constant ppf (_, t) =
+  Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
+
 let output_concrete_model fmt props ~functions ~constants ~arrays =
   Format.fprintf fmt "@[<v 2>(";
   if Options.get_model_type_constraints () then
@@ -483,20 +488,42 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
       Format.fprintf fmt "@ ; values"
     end;
 
+  let values = Hashtbl.create 17 in
+  (* Add the constants *)
+  ModelMap.iter (fun (f, xs_ty, _) st ->
+      assert (Lists.is_empty xs_ty);
+
+      ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
+          assert (Lists.is_empty keys);
+          Hashtbl.add values f (value (value_r, value_s)))
+        st) constants;
+
+  (* Add the arrays values, when applicable *)
+  ModelMap.iter (fun (f, xs_ty, ty) st ->
+      let root =
+        try Hashtbl.find values f
+        with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty))
+      in
+      Hashtbl.replace values f @@
+      ModelMap.V.fold (fun (keys, rs) acc ->
+          Store (acc, value (snd (List.hd keys)), value rs))
+        st root)
+    arrays;
+
+  let pp_value =
+    pp_value (fun ppf (sy, _) ->
+        pp_value pp_constant ppf (Hashtbl.find values sy))
+  in
+
+  let pp_x ppf xs = pp_value ppf (value xs) in
+
   (* Functions *)
   let records = SmtlibCounterExample.output_functions_counterexample
-      fmt  MS.empty functions in
-
-  let array_symbols =
-    ModelMap.fold (fun (f, _, _) _ -> Sy.Set.add f) arrays Sy.Set.empty
+      pp_x fmt  MS.empty functions
   in
 
   (* Constants *)
-  (* If the constant is present in the arrays map, it will be printed there. *)
   SmtlibCounterExample.output_constants_counterexample
-    ~ignored:array_symbols fmt records constants;
-
-  (* Arrays *)
-  SmtlibCounterExample.output_arrays_counterexample fmt arrays;
+    pp_x fmt records constants;
 
   Printer.print_fmt fmt "@]@,)";