6 |
6 |
7 structure ML_PP: sig end = |
7 structure ML_PP: sig end = |
8 struct |
8 struct |
9 |
9 |
10 val _ = |
10 val _ = |
11 PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
11 ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
12 |
12 |
13 val _ = |
13 val _ = |
14 PolyML.addPrettyPrinter (fn depth => fn _ => |
14 ML_system_pp (fn depth => fn _ => |
15 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory); |
15 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory); |
16 |
16 |
17 val _ = |
17 val _ = |
18 PolyML.addPrettyPrinter (fn depth => fn _ => |
18 ML_system_pp (fn depth => fn _ => |
19 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory); |
19 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory); |
20 |
20 |
21 val _ = |
21 val _ = |
22 PolyML.addPrettyPrinter (fn depth => fn _ => |
22 ML_system_pp (fn depth => fn _ => |
23 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory); |
23 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory); |
24 |
24 |
25 val _ = |
25 val _ = |
26 PolyML.addPrettyPrinter (fn depth => fn _ => |
26 ML_system_pp (fn depth => fn _ => |
27 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory); |
27 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory); |
28 |
28 |
29 |
29 |
30 local |
30 local |
31 |
31 |
41 |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u) |
41 |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u) |
42 |> Pretty.separate " $" |
42 |> Pretty.separate " $" |
43 |> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
43 |> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
44 | Abs (a, T, b) => |
44 | Abs (a, T, b) => |
45 prt_apps "Abs" |
45 prt_apps "Abs" |
46 [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)), |
46 [Pretty.from_polyml (ML_system_pretty (a, dp - 1)), |
47 Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)), |
47 Pretty.from_polyml (ML_system_pretty (T, dp - 2)), |
48 prt_term false (dp - 3) b] |
48 prt_term false (dp - 3) b] |
49 | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))) |
49 | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))) |
50 | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (a, dp - 1)))); |
52 | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))); |
53 |
53 |
54 in |
54 in |
55 |
55 |
56 val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth); |
56 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth); |
57 |
57 |
58 |
58 |
59 local |
59 local |
60 |
60 |
61 fun prt_proof parens dp prf = |
61 fun prt_proof parens dp prf = |
64 (case prf of |
64 (case prf of |
65 _ % _ => prt_proofs parens dp prf |
65 _ % _ => prt_proofs parens dp prf |
66 | _ %% _ => prt_proofs parens dp prf |
66 | _ %% _ => prt_proofs parens dp prf |
67 | Abst (a, T, b) => |
67 | Abst (a, T, b) => |
68 prt_apps "Abst" |
68 prt_apps "Abst" |
69 [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)), |
69 [Pretty.from_polyml (ML_system_pretty (a, dp - 1)), |
70 Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)), |
70 Pretty.from_polyml (ML_system_pretty (T, dp - 2)), |
71 prt_proof false (dp - 3) b] |
71 prt_proof false (dp - 3) b] |
72 | AbsP (a, t, b) => |
72 | AbsP (a, t, b) => |
73 prt_apps "AbsP" |
73 prt_apps "AbsP" |
74 [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)), |
74 [Pretty.from_polyml (ML_system_pretty (a, dp - 1)), |
75 Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)), |
75 Pretty.from_polyml (ML_system_pretty (t, dp - 2)), |
76 prt_proof false (dp - 3) b] |
76 prt_proof false (dp - 3) b] |
77 | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t) |
77 | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t) |
78 | MinProof => Pretty.str "MinProof" |
78 | MinProof => Pretty.str "MinProof" |
79 | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))) |
79 | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))) |
80 | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (a, dp - 1)))) |
84 | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))) |
85 |
85 |
86 and prt_proofs parens dp prf = |
86 and prt_proofs parens dp prf = |
87 let |
87 let |
88 val (head, args) = strip_proof prf []; |
88 val (head, args) = strip_proof prf []; |
89 val prts = |
89 val prts = |
92 |
92 |
93 and strip_proof (p % t) res = |
93 and strip_proof (p % t) res = |
94 strip_proof p |
94 strip_proof p |
95 ((fn d => |
95 ((fn d => |
96 [Pretty.str " %", Pretty.brk 1, |
96 [Pretty.str " %", Pretty.brk 1, |
97 Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res) |
97 Pretty.from_polyml (ML_system_pretty (t, d))]) :: res) |
98 | strip_proof (p %% q) res = |
98 | strip_proof (p %% q) res = |
99 strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d 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); |
100 | strip_proof p res = (fn d => prt_proof true d p, res); |
101 |
101 |
102 in |
102 in |
103 |
103 |
104 val _ = |
104 val _ = |
105 PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => |
105 ML_system_pp (fn depth => fn _ => fn prf => |
106 ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf))); |
106 ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf))); |
107 |
107 |
108 end; |
108 end; |
109 |
109 |
110 end; |
110 end; |