src/Pure/ML/install_pp_polyml.ML
author wenzelm
Sun, 23 Jun 2013 18:11:38 +0200
changeset 52426 81e27230a8b7
parent 52425 de8a85aad216
child 62356 e307a410f46c
permissions -rw-r--r--
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47980
c81801f881b3 simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents: 43791
diff changeset
     1
(*  Title:      Pure/ML/install_pp_polyml.ML
38327
d6afb77b0f6d more precise and more maintainable dependencies;
wenzelm
parents: 33767
diff changeset
     2
    Author:     Makarius
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     3
50910
54f06ba192ef tuned comments;
wenzelm
parents: 47986
diff changeset
     4
Extra toplevel pretty-printing for Poly/ML.
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     5
*)
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     6
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     7
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     8
  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     9
43791
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    10
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    11
  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    12
33767
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    13
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    14
  pretty (Synchronized.value var, depth));
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    15
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    16
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    17
  (case Future.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    18
    NONE => PolyML.PrettyString "<future>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    19
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    20
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    21
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    22
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    23
  (case Lazy.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    24
    NONE => PolyML.PrettyString "<lazy>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    25
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    26
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    27
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    28
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    29
local
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    30
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    31
open PolyML;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    32
val from_ML = Pretty.from_ML o pretty_ml;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    33
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    34
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    35
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    36
fun prt_term parens dp t =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    37
  if dp <= 0 then Pretty.str "..."
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    38
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    39
    (case t of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    40
      _ $ _ =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    41
        op :: (strip_comb t)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    42
        |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    43
        |> Pretty.separate " $"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    44
        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    45
    | Abs (a, T, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    46
        prt_apps "Abs"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    47
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    48
          from_ML (prettyRepresentation (T, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    49
          prt_term false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    50
    | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    51
    | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    52
    | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    53
    | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1))));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    54
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    55
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    56
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    57
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    58
  PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    59
    ml_pretty (Pretty.to_ML (prt_term false depth t)));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    60
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    61
local
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    62
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    63
fun prt_proof parens dp prf =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    64
  if dp <= 0 then Pretty.str "..."
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    65
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    66
    (case prf of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    67
      _ % _ => prt_proofs parens dp prf
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    68
    | _ %% _ => prt_proofs parens dp prf
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    69
    | Abst (a, T, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    70
        prt_apps "Abst"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    71
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    72
          from_ML (prettyRepresentation (T, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    73
          prt_proof false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    74
    | AbsP (a, t, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    75
        prt_apps "AbsP"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    76
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    77
          from_ML (prettyRepresentation (t, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    78
          prt_proof false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    79
    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    80
    | MinProof => Pretty.str "MinProof"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    81
    | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    82
    | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    83
    | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    84
    | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    85
    | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    86
    | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1))))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    87
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    88
and prt_proofs parens dp prf =
33545
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    89
  let
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    90
    val (head, args) = strip_proof prf [];
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    91
    val prts = head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - i - 2)) args);
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    92
  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    93
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    94
and strip_proof (p % t) res =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    95
      strip_proof p
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    96
        ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    97
  | strip_proof (p %% q) res =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    98
      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    99
  | strip_proof p res = (fn d => prt_proof true d p, res);
33545
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
   100
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   101
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   102
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   103
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   104
  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   105
    ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   106
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   107
end;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   108
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   109
end;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   110