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