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