diff --git a/src/core/dterm.ml b/src/core/dterm.ml
index 6f31768fe8226322a2a022b5aaa56e072a2d77a2..e8b156c3899c788f990df5ebb4bd4f1eafe08c43 100644
--- a/src/core/dterm.ml
+++ b/src/core/dterm.ml
@@ -124,16 +124,17 @@ let rec print_dty ht pri fmt = function
Format.fprintf fmt "(%a)"
(Pp.print_list Pp.comma (print_dty ht 0)) dl
| Dapp (ts,[]) ->
- Pretty.print_ts fmt ts
+ Pretty.print_ts_qualified fmt ts
| Dapp (ts,dl) ->
Format.fprintf fmt (protect_on (pri > 1) "%a@ %a")
- Pretty.print_ts ts (Pp.print_list Pp.space (print_dty ht 2)) dl
+ Pretty.print_ts_qualified ts
+ (Pp.print_list Pp.space (print_dty ht 2)) dl
| Duty ({ty_node = Tyapp (ts,(_::_))} as ty)
when (pri > 1 && not (is_ts_tuple ts))
|| (pri = 1 && ts_equal ts Ty.ts_func) ->
- Format.fprintf fmt "(%a)" Pretty.print_ty ty
+ Format.fprintf fmt "(%a)" Pretty.print_ty_qualified ty
| Duty ty ->
- Pretty.print_ty fmt ty
+ Pretty.print_ty_qualified fmt ty
let print_dty = let ht = Hint.create 3 in fun fmt dty ->
print_dty ht 0 fmt dty
diff --git a/src/core/pretty.ml b/src/core/pretty.ml
index a1371ce3e286b5e6bafd86fa729f73086becec9c..e71ead90f2e1430beae2056d7462a3168043a531 100644
--- a/src/core/pretty.ml
+++ b/src/core/pretty.ml
@@ -53,6 +53,13 @@ module type Printer = sig
val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
+ val print_ts_qualified : formatter -> tysymbol -> unit
+ val print_ls_qualified : formatter -> lsymbol -> unit
+ val print_cs_qualified : formatter -> lsymbol -> unit
+ val print_pr_qualified : formatter -> prsymbol -> unit
+ val print_th_qualified : formatter -> theory -> unit
+ val print_ty_qualified : formatter -> ty -> unit
+
val print_quant : formatter -> quant -> unit (* quantifier *)
val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
val print_pat : formatter -> pattern -> unit (* pattern *)
@@ -86,9 +93,7 @@ module type Printer = sig
end
-let debug_print_attrs =
- Debug.register_info_flag
- "print_attributes"
+let debug_print_attrs = Debug.register_info_flag "print_attributes"
~desc:"Print@ attributes@ of@ identifiers@ and@ expressions."
let debug_print_locs = Debug.register_info_flag "print_locs"
@@ -97,6 +102,10 @@ let debug_print_locs = Debug.register_info_flag "print_locs"
let debug_print_coercions = Debug.register_info_flag "print_coercions"
~desc:"Print@ coercions@ in@ logical@ formulas."
+(* always print qualified?
+let debug_print_qualifs = Debug.register_info_flag "print_qualifs"
+ ~desc:"Print@ qualifiers@ of@ identifiers@ in@ error@ messages."*)
+
let create sprinter aprinter tprinter pprinter do_forget_all =
(module (struct
@@ -154,31 +163,102 @@ let print_ls fmt ls =
let print_pr fmt pr =
Ident.print_decoded fmt (id_unique pprinter pr.pr_name)
+let print_library_path fmt lp =
+ let str fmt s =
+ if String.contains s ' ' || String.contains s '.' then begin
+ pp_print_char fmt '"'; pp_print_string fmt s; pp_print_char fmt '"'
+ end else pp_print_string fmt s in
+ let dot fmt () =
+ pp_print_char fmt '.'; pp_print_cut fmt () in
+ if lp <> [] then begin
+ print_list dot str fmt lp; dot fmt ()
+ end
+
+let print_qualified_name fmt qn =
+ let dot fmt () =
+ pp_print_char fmt '.'; pp_print_cut fmt () in
+ if qn <> [] then begin
+ dot fmt (); print_list dot pp_print_string fmt qn
+ end
+
+let print_decoded_name fmt qn =
+ match List.rev qn with
+ | sn::qn ->
+ print_qualified_name fmt (List.rev qn);
+ pp_print_char fmt '.'; pp_print_cut fmt ();
+ Ident.print_decoded fmt sn
+ | [] -> ()
+
+let print_th_qualified fmt th =
+(* if Debug.test_flag debug_print_qualifs then begin *)
+ try
+ let lp,tn,_ = Theory.restore_path th.th_name in
+ fprintf fmt "%a%s" print_library_path lp tn
+ with Not_found -> print_th fmt th
+(* end else print_th fmt th *)
+
+let print_ts_qualified fmt ts =
+ if ts_equal ts ts_func then pp_print_string fmt "(->)" else
+(* if Debug.test_flag debug_print_qualifs then begin *)
+ try
+ let lp,tn,qn = Theory.restore_path ts.ts_name in
+ fprintf fmt "%a%s%a" print_library_path lp tn print_qualified_name qn
+ with Not_found -> print_ts fmt ts
+(* end else print_ts fmt ts *)
+
+let print_cs_qualified fmt ls =
+(* if Debug.test_flag debug_print_qualifs then begin *)
+ try
+ let lp,tn,qn = Theory.restore_path ls.ls_name in
+ fprintf fmt "%a%s%a" print_library_path lp tn print_qualified_name qn
+ with Not_found -> print_cs fmt ls
+(* end else print_cs fmt ls *)
+
+let print_ls_qualified fmt ls =
+(* if Debug.test_flag debug_print_qualifs then begin *)
+ try
+ let lp,tn,qn = Theory.restore_path ls.ls_name in
+ fprintf fmt "%a%s%a" print_library_path lp tn print_decoded_name qn
+ with Not_found -> print_ls fmt ls
+(* end else print_ls fmt ls *)
+
+let print_pr_qualified fmt pr =
+(* if Debug.test_flag debug_print_qualifs then begin *)
+ try
+ let lp,tn,qn = Theory.restore_path pr.pr_name in
+ fprintf fmt "%a%s%a" print_library_path lp tn print_decoded_name qn
+ with Not_found -> print_pr fmt pr
+(* end else print_pr fmt pr *)
+
(** Types *)
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
-let rec print_ty_node pri fmt ty = match ty.ty_node with
+let rec print_ty_node q pri fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, [t1;t2]) when ts_equal ts Ty.ts_func ->
fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
- (print_ty_node 1) t1 (print_ty_node 0) t2
+ (print_ty_node q 1) t1 (print_ty_node q 0) t2
| Tyapp (ts, []) when is_ts_tuple ts ->
fprintf fmt "unit"
| Tyapp (ts, tl) when is_ts_tuple ts ->
- fprintf fmt "(%a)" (print_list comma (print_ty_node 0)) tl
- | Tyapp (ts, []) -> print_ts fmt ts
+ fprintf fmt "(%a)" (print_list comma (print_ty_node q 0)) tl
+ | Tyapp (ts, []) ->
+ if q then print_ts_qualified fmt ts else print_ts fmt ts
| Tyapp (ts, tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
- print_ts ts (print_list space (print_ty_node 2)) tl
+ (if q then print_ts_qualified else print_ts) ts
+ (print_list space (print_ty_node q 2)) tl
+
+let print_ty fmt ty = print_ty_node false 0 fmt ty
-let print_ty fmt ty = print_ty_node 0 fmt ty
+let print_ty_qualified fmt ty = print_ty_node true 0 fmt ty
let print_vsty fmt v =
fprintf fmt "%a%a:@,%a" print_vs v
print_id_attrs v.vs_name print_ty v.vs_ty
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
-let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node 2) ty
+let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node false 2) ty
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs
(* can the type of a value be derived from the type of the arguments? *)
@@ -654,7 +734,7 @@ let () = Exn_printer.register
begin fun fmt exn -> match exn with
| Ty.TypeMismatch (t1,t2) ->
fprintf fmt "Type mismatch between %a and %a"
- print_ty t1 print_ty t2
+ print_ty_qualified t1 print_ty_qualified t2
| Ty.BadTypeArity ({ts_args = []} as ts, _) ->
fprintf fmt "Type symbol %a expects no arguments" print_ts ts
| Ty.BadTypeArity (ts, app_arg) ->
diff --git a/src/core/pretty.mli b/src/core/pretty.mli
index ab4622ce6cffc750a6704744b88bac9519b001d6..870dc5d29f17e7234daeed28304fa697c204029d 100644
--- a/src/core/pretty.mli
+++ b/src/core/pretty.mli
@@ -48,6 +48,13 @@ module type Printer = sig
val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
+ val print_ts_qualified : formatter -> tysymbol -> unit
+ val print_ls_qualified : formatter -> lsymbol -> unit
+ val print_cs_qualified : formatter -> lsymbol -> unit
+ val print_pr_qualified : formatter -> prsymbol -> unit
+ val print_th_qualified : formatter -> theory -> unit
+ val print_ty_qualified : formatter -> ty -> unit
+
val print_quant : formatter -> quant -> unit (* quantifier *)
val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
val print_pat : formatter -> pattern -> unit (* pattern *)
diff --git a/src/mlw/dexpr.ml b/src/mlw/dexpr.ml
index bfc7822d278d8f3a394332548860d91428a208b8..26e4f20caf53d4249230354449d6faa3959ddaec 100644
--- a/src/mlw/dexpr.ml
+++ b/src/mlw/dexpr.ml
@@ -263,7 +263,7 @@ let rec print_dity pur pri fmt = function
| Durg (Dapp (s,tl,rl),{reg_name = id}) ->
Format.fprintf fmt
(protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a@ @@%s")
- Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
+ Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
(print_regs (print_dity pur 0)) rl (Ident.id_unique rprinter id)
| Dvar {contents = Dreg _} | Durg _ -> assert false
| Dapp (s,[t1;t2],[]) when its_equal s its_func ->
@@ -273,16 +273,16 @@ let rec print_dity pur pri fmt = function
Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity pur 0)) tl
| Dapp (s,tl,_) when pur ->
Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "%a%a")
- Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
+ Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
| Dapp (s,tl,rl) when not s.its_mutable ->
Format.fprintf fmt
(protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a")
- Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
+ Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
(print_regs (print_dity pur 0)) rl
| Dapp (s,tl,rl) ->
Format.fprintf fmt
(protect_on (pri > 1 && (tl <> [] || rl <> [])) "{%a}%a%a")
- Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
+ Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
(print_regs (print_dity pur 0)) rl
let print_dity fmt d = print_dity false 0 fmt d