isabelle: src/Pure/ML/ml_pp.ML@254582abf067

     1 (*  Title:      Pure/ML/ml_pp.ML

     2     Author:     Makarius

     4 ML toplevel pretty-printing for logical entities.

     5 *)

     7 structure ML_PP: sig end =

     8 struct

    10 val _ =

    11   PolyML.addPrettyPrinter

    12     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);

    14 val _ =

    15   PolyML.addPrettyPrinter

    16     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);

    18 val _ =

    19   PolyML.addPrettyPrinter

    20     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);

    22 val _ =

    23   PolyML.addPrettyPrinter

    24     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);

    26 val _ =

    27   PolyML.addPrettyPrinter

    28     (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);

    31 local

    33 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];

    34 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";

    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))));

    55 in

    57 val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);

    60 local

    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))))

    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

    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);

   103 in

   105 val _ =

   106   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>

   107     ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));

   109 end;

   111 end;

   113 end;

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--