From a5f2cb785649e2bb73b450262e2e54703ef526c4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Feb 2018 04:09:23 +0100 Subject: [checker] Printer cleanup. Makes printing rules more explicit and should close #6799. --- checker/checker.ml | 44 +++++++-------- checker/print.ml | 156 ++++++++++++++++++----------------------------------- checker/print.mli | 2 +- 3 files changed, 75 insertions(+), 127 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index b2aeb1f14..fd2725c85 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -17,10 +17,10 @@ open Check let () = at_exit flush_all -let chk_pp = Pp.pp_with Format.std_formatter +let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a let fatal_error info anomaly = - flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -269,26 +269,26 @@ let explain_exn = function | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" | CantApplyBadType ((n,a,b),(hd,hdty),args) -> - Format.printf "====== ill-typed term ====@\n"; - Format.printf "@[application head=@ "; - Print.print_pure_constr hd; - Format.printf "@]@\n@[head type=@ "; - Print.print_pure_constr hdty; - Format.printf "@]@\narguments:@\n@["; - Array.iteri (fun i (t,ty) -> - Format.printf "@[arg %d=@ " (i+1); - Print.print_pure_constr t; - Format.printf "@ type=@ "; - Print.print_pure_constr ty) args; - Format.printf "@]@\n====== type error ====@\n"; - Print.print_pure_constr b; - Format.printf "@\nis not convertible with@\n"; - Print.print_pure_constr a; - Format.printf "@\n====== universes ====@\n"; - chk_pp - (Univ.pr_universes - (ctx.Environ.env_stratification.Environ.env_universes)); - str "\nCantApplyBadType at argument " ++ int n + (* This mix of printf / pp was here before... *) + let fmt = Format.std_formatter in + let open Format in + let open Print in + fprintf fmt "====== ill-typed term ====@\n"; + fprintf fmt "@[application head=@ %a@]@\n" print_pure_constr hd; + fprintf fmt "@[head type=@ %a@]@\n" print_pure_constr hdty; + let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1) + print_pure_constr t print_pure_constr ty + in + fprintf fmt "arguments:@\n@[%a@]@\n" (pp_arrayi pp_arg) args; + fprintf fmt "====== type error ====@\n"; + fprintf fmt "%a@\n" print_pure_constr b; + fprintf fmt "is not convertible with@\n"; + fprintf fmt "%a@\n" print_pure_constr a; + fprintf fmt "====== universes ====@\n"; + fprintf fmt "%a@\n%!" Pp.pp_with + (Univ.pr_universes + (ctx.Environ.env_stratification.Environ.env_universes)); + str "CantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" diff --git a/checker/print.ml b/checker/print.ml index c1fa8f94c..fc9cd687e 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -12,137 +12,85 @@ open Format open Cic open Names -let chk_pp = Pp.pp_with Format.std_formatter +let chk_pp fmt = Pp.pp_with fmt +let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a +let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i) +let pp_id fmt id = fprintf fmt "%s" (Id.to_string id) -let print_instance i = chk_pp (Univ.Instance.pr i) - -let print_pure_constr csr = - let rec term_display c = match c with - | Rel n -> print_string "#"; print_int n - | Meta n -> print_string "Meta("; print_int n; print_string ")" - | Var id -> print_string (Id.to_string id) - | Sort s -> sort_display s - | Cast (c,_, t) -> open_hovbox 1; - print_string "("; (term_display c); print_cut(); - print_string "::"; (term_display t); print_string ")"; close_box() +let print_pure_constr fmt csr = + let rec pp_term fmt c = match c with + | Rel n -> fprintf fmt "#%d" n + | Meta n -> fprintf fmt "Meta(%d)" n + | Var id -> pp_id fmt id + | Sort s -> pp_sort fmt s + | Cast (c,_, t) -> + fprintf fmt "@[(%a@;::%a)@]" pp_term c pp_term t | Prod (Name(id),t,c) -> - open_hovbox 1; - print_string"("; print_string (Id.to_string id); - print_string ":"; box_display t; - print_string ")"; print_cut(); - box_display c; close_box() + fprintf fmt "@[(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c | Prod (Anonymous,t,c) -> - print_string"("; box_display t; print_cut(); print_string "->"; - box_display c; print_string ")"; + fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c | Lambda (na,t,c) -> - print_string "["; name_display na; - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c | LetIn (na,b,t,c) -> - print_string "["; name_display na; print_string "="; - box_display b; print_cut(); - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c | App (c,l) -> - print_string "("; - box_display c; - Array.iter (fun x -> print_space (); box_display x) l; - print_string ")" - | Evar _ -> print_string "Evar#" - | Const (c,u) -> print_string "Cons("; - sp_con_display c; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "(@[%a@]@, @[%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l; + | Evar _ -> pp_print_string fmt "Evar#" + | Const (c,u) -> + fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u | Ind ((sp,i),u) -> - print_string "Ind("; - sp_display sp; - print_string ","; print_int i; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u | Construct (((sp,i),j),u) -> - print_string "Constr("; - sp_display sp; - print_string ","; - print_int i; print_string ","; print_int j; - print_string ","; print_instance u; print_string ")" + fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u | Case (ci,p,c,bl) -> - open_vbox 0; - print_string "<"; box_display p; print_string ">"; - print_cut(); print_string "Case"; - print_space(); box_display c; print_space (); print_string "of"; - open_vbox 0; - Array.iter (fun x -> print_cut(); box_display x) bl; - close_box(); - print_cut(); - print_string "end"; - close_box() + let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in + fprintf fmt "@[<@[%a@]>@,Case@ @[%a@]@ of@[%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 0; - name_display lna.(k); print_string "/"; - print_int t.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut() - done - in print_string"{"; print_fix(); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[ %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "Fix(%d)@,@[{%a}@]" i (pp_arrayi pp_fixc) tl | CoFix(i,(lna,tl,bl)) -> - print_string "CoFix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 1; - name_display lna.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut(); - done - in print_string"{"; print_fix (); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[ %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "CoFix(%d)@,@[{%a}@]" i (pp_arrayi pp_fixc) tl | Proj (p, c) -> - print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; - box_display c; print_string ")" + fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c - and box_display c = open_hovbox 1; term_display c; close_box() + and pp_sort fmt = function + | Prop(Pos) -> pp_print_string fmt "Set" + | Prop(Null) -> pp_print_string fmt "Prop" + | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) - and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" + and pp_name fmt = function + | Name id -> pp_id fmt id + | Anonymous -> pp_print_string fmt "_" - and name_display = function - | Name id -> print_string (Id.to_string id) - | Anonymous -> print_string "_" (* Remove the top names for library and Scratch to avoid long names *) - and sp_display sp = -(* let dir,l = decode_kn sp in + and sp_display fmt sp = +(* let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (MutInd.debug_to_string sp) - and sp_con_display sp = -(* let dir,l = decode_kn sp in + pp_print_string fmt (MutInd.debug_to_string sp) + + and sp_con_display fmt sp = + (* + let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (Constant.debug_to_string sp) + pp_print_string fmt (Constant.debug_to_string sp) in - try - box_display csr; print_flush() - with e -> - print_string (Printexc.to_string e);print_flush (); - raise e - - - + try + fprintf fmt "@[%a@]%!" pp_term csr + with e -> + pp_print_string fmt (Printexc.to_string e); + print_flush (); + raise e diff --git a/checker/print.mli b/checker/print.mli index 67562125f..da1362ca5 100644 --- a/checker/print.mli +++ b/checker/print.mli @@ -10,4 +10,4 @@ open Cic -val print_pure_constr : constr -> unit +val print_pure_constr : Format.formatter -> constr -> unit -- cgit v1.2.3