src/Pure/ML/ml_pp.ML
author wenzelm
Fri Mar 18 17:51:57 2016 +0100 (2016-03-18)
changeset 62667 254582abf067
parent 62665 a78ce0c6e191
child 62673 b5c57430b9dd
permissions -rw-r--r--
clarified Pretty.T toplevel pp;
     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
    12     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    13 
    14 val _ =
    15   PolyML.addPrettyPrinter
    16     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
    17 
    18 val _ =
    19   PolyML.addPrettyPrinter
    20     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
    21 
    22 val _ =
    23   PolyML.addPrettyPrinter
    24     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    25 
    26 val _ =
    27   PolyML.addPrettyPrinter
    28     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
    29 
    30 
    31 local
    32 
    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: FixedInt.int) 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 - FixedInt.fromInt 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          [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    48           Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    49           prt_term false (dp - 3) b]
    50     | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    51     | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    52     | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    53     | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
    54 
    55 in
    56 
    57 val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
    58 
    59 
    60 local
    61 
    62 fun prt_proof parens dp prf =
    63   if dp <= 0 then Pretty.str "..."
    64   else
    65     (case prf of
    66       _ % _ => prt_proofs parens dp prf
    67     | _ %% _ => prt_proofs parens dp prf
    68     | Abst (a, T, b) =>
    69         prt_apps "Abst"
    70          [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    71           Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    72           prt_proof false (dp - 3) b]
    73     | AbsP (a, t, b) =>
    74         prt_apps "AbsP"
    75          [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    76           Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
    77           prt_proof false (dp - 3) b]
    78     | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
    79     | MinProof => Pretty.str "MinProof"
    80     | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    81     | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    82     | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    83     | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    84     | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    85     | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
    86 
    87 and prt_proofs parens dp prf =
    88   let
    89     val (head, args) = strip_proof prf [];
    90     val prts =
    91       head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
    92   in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
    93 
    94 and strip_proof (p % t) res =
    95       strip_proof p
    96         ((fn d =>
    97           [Pretty.str " %", Pretty.brk 1,
    98             Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
    99   | strip_proof (p %% q) res =
   100       strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
   101   | strip_proof p res = (fn d => prt_proof true d p, res);
   102 
   103 in
   104 
   105 val _ =
   106   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
   107     ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
   108 
   109 end;
   110 
   111 end;
   112 
   113 end;