src/Pure/ML/ml_pp.ML
author wenzelm
Fri Mar 18 21:29:10 2016 +0100 (2016-03-18)
changeset 62673 b5c57430b9dd
parent 62667 254582abf067
child 62819 d3ff367a16a0
permissions -rw-r--r--
observe ML print depth;
     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 (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    12 
    13 val _ =
    14   PolyML.addPrettyPrinter (fn depth => fn _ =>
    15     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
    16 
    17 val _ =
    18   PolyML.addPrettyPrinter (fn depth => fn _ =>
    19     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
    20 
    21 val _ =
    22   PolyML.addPrettyPrinter (fn depth => fn _ =>
    23     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    24 
    25 val _ =
    26   PolyML.addPrettyPrinter (fn depth => fn _ =>
    27     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
    28 
    29 
    30 local
    31 
    32 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    33 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    34 
    35 fun 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 (PolyML.prettyRepresentation (a, dp - 1)),
    47           Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    48           prt_term false (dp - 3) b]
    49     | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    50     | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    51     | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    52     | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
    53 
    54 in
    55 
    56 val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
    57 
    58 
    59 local
    60 
    61 fun 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 (PolyML.prettyRepresentation (a, dp - 1)),
    70           Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    71           prt_proof false (dp - 3) b]
    72     | AbsP (a, t, b) =>
    73         prt_apps "AbsP"
    74          [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    75           Pretty.from_polyml (PolyML.prettyRepresentation (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 (PolyML.prettyRepresentation (a, dp - 1)))
    80     | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    81     | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    82     | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    83     | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    84     | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
    85 
    86 and 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 
    93 and strip_proof (p % t) res =
    94       strip_proof p
    95         ((fn d =>
    96           [Pretty.str " %", Pretty.brk 1,
    97             Pretty.from_polyml (PolyML.prettyRepresentation (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 
   102 in
   103 
   104 val _ =
   105   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
   106     ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
   107 
   108 end;
   109 
   110 end;
   111 
   112 end;