Commit dc0b56b0 authored by Andrei Paskevich's avatar Andrei Paskevich

print qualified names in types for type-mismatch errors

Not done for low-level TypeMismatch exception in Ity.
However, this should not be an issue, since the majority
of type errors happen in Dexpr and will be reported with
qualified names.
parent 0080ce31
......@@ -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
......
......@@ -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) ->
......
......@@ -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 *)
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment