1(*  Title:      Pure/ML/ml_pp.ML
2    Author:     Makarius
3
4ML toplevel pretty-printing for logical entities.
5*)
6
7structure ML_PP: sig end =
8struct
9
10val _ =
11  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
12
13val _ =
14  ML_system_pp (fn depth => fn _ =>
15    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure);
16
17val _ =
18  ML_system_pp (fn depth => fn _ =>
19    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure);
20
21val _ =
22  ML_system_pp (fn depth => fn _ =>
23    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure);
24
25val _ =
26  ML_system_pp (fn depth => fn _ =>
27    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);
28
29
30local
31
32fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
33fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
34
35fun prt_term parens (dp: FixedInt.int) t =
36  if dp <= 0 then Pretty.str "..."
37  else
38    (case t of
39      _ $ _ =>
40        op :: (strip_comb t)
41        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
42        |> Pretty.separate " $"
43        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
44    | Abs (a, T, b) =>
45        prt_apps "Abs"
46         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
47          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
48          prt_term false (dp - 3) b]
49    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
50    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
51    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
52    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
53
54in
55
56val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
57
58
59local
60
61fun prt_proof parens dp prf =
62  if dp <= 0 then Pretty.str "..."
63  else
64    (case prf of
65      _ % _ => prt_proofs parens dp prf
66    | _ %% _ => prt_proofs parens dp prf
67    | Abst (a, T, b) =>
68        prt_apps "Abst"
69         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
70          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
71          prt_proof false (dp - 3) b]
72    | AbsP (a, t, b) =>
73        prt_apps "AbsP"
74         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
75          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
76          prt_proof false (dp - 3) b]
77    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
78    | MinProof => Pretty.str "MinProof"
79    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
80    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
81    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
82    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
83    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
84    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
85
86and prt_proofs parens dp prf =
87  let
88    val (head, args) = strip_proof prf [];
89    val prts =
90      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
91  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
92
93and strip_proof (p % t) res =
94      strip_proof p
95        ((fn d =>
96          [Pretty.str " %", Pretty.brk 1,
97            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
98  | strip_proof (p %% q) res =
99      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
100  | strip_proof p res = (fn d => prt_proof true d p, res);
101
102in
103
104val _ =
105  ML_system_pp (fn depth => fn _ => fn prf =>
106    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
107
108end;
109
110end;
111
112end;
113