23 (case Lazy.peek x of |
23 (case Lazy.peek x of |
24 NONE => PolyML.PrettyString "<lazy>" |
24 NONE => PolyML.PrettyString "<lazy>" |
25 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
25 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
26 | SOME (Exn.Res y) => pretty (y, depth))); |
26 | SOME (Exn.Res y) => pretty (y, depth))); |
27 |
27 |
28 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => |
28 |
|
29 local |
|
30 |
|
31 open PolyML; |
|
32 val from_ML = Pretty.from_ML o pretty_ml; |
|
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 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 - 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 [from_ML (prettyRepresentation (a, dp - 1)), |
|
48 from_ML (prettyRepresentation (T, dp - 2)), |
|
49 prt_term false (dp - 3) b] |
|
50 | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1))) |
|
51 | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1))) |
|
52 | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1))) |
|
53 | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1)))); |
|
54 |
|
55 in |
|
56 |
|
57 val _ = |
|
58 PolyML.addPrettyPrinter (fn depth => fn _ => fn t => |
|
59 ml_pretty (Pretty.to_ML (prt_term false depth t))); |
|
60 |
|
61 local |
|
62 |
|
63 fun prt_proof parens dp prf = |
|
64 if dp <= 0 then Pretty.str "..." |
|
65 else |
|
66 (case prf of |
|
67 _ % _ => prt_proofs parens dp prf |
|
68 | _ %% _ => prt_proofs parens dp prf |
|
69 | Abst (a, T, b) => |
|
70 prt_apps "Abst" |
|
71 [from_ML (prettyRepresentation (a, dp - 1)), |
|
72 from_ML (prettyRepresentation (T, dp - 2)), |
|
73 prt_proof false (dp - 3) b] |
|
74 | AbsP (a, t, b) => |
|
75 prt_apps "AbsP" |
|
76 [from_ML (prettyRepresentation (a, dp - 1)), |
|
77 from_ML (prettyRepresentation (t, dp - 2)), |
|
78 prt_proof false (dp - 3) b] |
|
79 | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t) |
|
80 | MinProof => Pretty.str "MinProof" |
|
81 | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1))) |
|
82 | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1))) |
|
83 | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1))) |
|
84 | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1))) |
|
85 | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1))) |
|
86 | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1)))) |
|
87 |
|
88 and prt_proofs parens dp prf = |
29 let |
89 let |
30 open PolyML; |
90 val (head, args) = strip_proof prf []; |
31 val from_ML = Pretty.from_ML o pretty_ml; |
91 val prts = head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - i - 2)) args); |
32 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
92 in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end |
33 fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; |
|
34 fun prt_term parens dp t = |
|
35 if dp <= 0 then Pretty.str "..." |
|
36 else |
|
37 (case t of |
|
38 _ $ _ => |
|
39 op :: (strip_comb t) |
|
40 |> map_index (fn (i, u) => prt_term true (dp - i - 1) u) |
|
41 |> Pretty.separate " $" |
|
42 |> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
|
43 | Abs (a, T, b) => |
|
44 prt_apps "Abs" |
|
45 [from_ML (prettyRepresentation (a, dp - 1)), |
|
46 from_ML (prettyRepresentation (T, dp - 2)), |
|
47 prt_term false (dp - 3) b] |
|
48 | Const const => prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1))) |
|
49 | Free free => prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1))) |
|
50 | Var var => prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1))) |
|
51 | Bound i => prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)))); |
|
52 in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); |
|
53 |
93 |
|
94 and strip_proof (p % t) res = |
|
95 strip_proof p |
|
96 ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res) |
|
97 | strip_proof (p %% q) res = |
|
98 strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res) |
|
99 | strip_proof p res = (fn d => prt_proof true d p, res); |
|
100 |
|
101 in |
|
102 |
|
103 val _ = |
|
104 PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => |
|
105 ml_pretty (Pretty.to_ML (prt_proof false depth prf))); |
|
106 |
|
107 end; |
|
108 |
|
109 end; |
|
110 |