1 (* Title: Pure/ML/install_pp_polyml.ML |
|
2 Author: Makarius |
|
3 |
|
4 ML toplevel pretty-printing for Poly/ML. |
|
5 *) |
|
6 |
|
7 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T => |
|
8 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>"))); |
|
9 |
|
10 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon => |
|
11 ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon))); |
|
12 |
|
13 PolyML.addPrettyPrinter (fn _ => fn _ => fn task => |
|
14 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task)))); |
|
15 |
|
16 PolyML.addPrettyPrinter (fn _ => fn _ => fn group => |
|
17 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group)))); |
|
18 |
|
19 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos => |
|
20 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos))); |
|
21 |
|
22 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding => |
|
23 ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding))); |
|
24 |
|
25 PolyML.addPrettyPrinter (fn _ => fn _ => fn th => |
|
26 ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th))); |
|
27 |
|
28 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct => |
|
29 ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct))); |
|
30 |
|
31 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT => |
|
32 ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT))); |
|
33 |
|
34 PolyML.addPrettyPrinter (fn _ => fn _ => fn T => |
|
35 ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T))); |
|
36 |
|
37 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy => |
|
38 ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy))); |
|
39 |
|
40 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt => |
|
41 ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt))); |
|
42 |
|
43 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast => |
|
44 ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast))); |
|
45 |
|
46 PolyML.addPrettyPrinter (fn _ => fn _ => fn path => |
|
47 ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path))); |
|
48 |
|
49 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest => |
|
50 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest))))); |
|
51 |
|
52 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state => |
|
53 ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>"))); |
|
54 |
|
55 PolyML.addPrettyPrinter (fn _ => fn _ => fn st => |
|
56 ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st))); |
|
57 |
|
58 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism => |
|
59 ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism))); |
|
60 |
|
61 PolyML.addPrettyPrinter (fn depth => fn _ => fn str => |
|
62 ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str))); |
|
63 |
|
64 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => |
|
65 ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree))); |
|
66 |
|
67 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
|
68 pretty (Synchronized.value var, depth)); |
|
69 |
|
70 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
71 (case Future.peek x of |
|
72 NONE => PolyML.PrettyString "<future>" |
|
73 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
74 | SOME (Exn.Res y) => pretty (y, depth))); |
|
75 |
|
76 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
77 (case Lazy.peek x of |
|
78 NONE => PolyML.PrettyString "<lazy>" |
|
79 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
80 | SOME (Exn.Res y) => pretty (y, depth))); |
|
81 |
|
82 |
|
83 local |
|
84 |
|
85 open PolyML; |
|
86 val from_ML = Pretty.from_ML o ML_Pretty.from_polyml; |
|
87 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
|
88 fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; |
|
89 |
|
90 fun prt_term parens (dp: FixedInt.int) t = |
|
91 if dp <= 0 then Pretty.str "..." |
|
92 else |
|
93 (case t of |
|
94 _ $ _ => |
|
95 op :: (strip_comb t) |
|
96 |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u) |
|
97 |> Pretty.separate " $" |
|
98 |> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
|
99 | Abs (a, T, b) => |
|
100 prt_apps "Abs" |
|
101 [from_ML (prettyRepresentation (a, dp - 1)), |
|
102 from_ML (prettyRepresentation (T, dp - 2)), |
|
103 prt_term false (dp - 3) b] |
|
104 | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1))) |
|
105 | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1))) |
|
106 | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1))) |
|
107 | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1)))); |
|
108 |
|
109 in |
|
110 |
|
111 val _ = |
|
112 PolyML.addPrettyPrinter (fn depth => fn _ => fn t => |
|
113 ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t))); |
|
114 |
|
115 local |
|
116 |
|
117 fun prt_proof parens dp prf = |
|
118 if dp <= 0 then Pretty.str "..." |
|
119 else |
|
120 (case prf of |
|
121 _ % _ => prt_proofs parens dp prf |
|
122 | _ %% _ => prt_proofs parens dp prf |
|
123 | Abst (a, T, b) => |
|
124 prt_apps "Abst" |
|
125 [from_ML (prettyRepresentation (a, dp - 1)), |
|
126 from_ML (prettyRepresentation (T, dp - 2)), |
|
127 prt_proof false (dp - 3) b] |
|
128 | AbsP (a, t, b) => |
|
129 prt_apps "AbsP" |
|
130 [from_ML (prettyRepresentation (a, dp - 1)), |
|
131 from_ML (prettyRepresentation (t, dp - 2)), |
|
132 prt_proof false (dp - 3) b] |
|
133 | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t) |
|
134 | MinProof => Pretty.str "MinProof" |
|
135 | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1))) |
|
136 | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1))) |
|
137 | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1))) |
|
138 | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1))) |
|
139 | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1))) |
|
140 | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1)))) |
|
141 |
|
142 and prt_proofs parens dp prf = |
|
143 let |
|
144 val (head, args) = strip_proof prf []; |
|
145 val prts = |
|
146 head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args); |
|
147 in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end |
|
148 |
|
149 and strip_proof (p % t) res = |
|
150 strip_proof p |
|
151 ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res) |
|
152 | strip_proof (p %% q) res = |
|
153 strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res) |
|
154 | strip_proof p res = (fn d => prt_proof true d p, res); |
|
155 |
|
156 in |
|
157 |
|
158 val _ = |
|
159 PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => |
|
160 ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf))); |
|
161 |
|
162 end; |
|
163 |
|
164 end; |
|