src/Pure/ML/install_pp_polyml.ML
author wenzelm
Fri, 18 Mar 2016 16:26:35 +0100
changeset 62663 bea354f6ff21
parent 62503 19afb533028e
permissions -rw-r--r--
clarified modules; tuned signature;
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
62356
wenzelm
parents: 52426
diff changeset
     4
ML 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
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
     7
PolyML.addPrettyPrinter
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
     8
  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
62356
wenzelm
parents: 52426
diff changeset
     9
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    10
PolyML.addPrettyPrinter
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    11
  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
62356
wenzelm
parents: 52426
diff changeset
    12
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    13
PolyML.addPrettyPrinter
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    14
  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
62356
wenzelm
parents: 52426
diff changeset
    15
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    16
PolyML.addPrettyPrinter
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    17
  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
33767
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    18
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    19
PolyML.addPrettyPrinter
bea354f6ff21 clarified modules;
wenzelm
parents: 62503
diff changeset
    20
  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    21
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    22
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    23
local
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    24
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    25
open PolyML;
62503
19afb533028e clarified modules;
wenzelm
parents: 62387
diff changeset
    26
val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    27
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
    28
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
    29
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    30
fun prt_term parens (dp: FixedInt.int) t =
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    31
  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
    32
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    33
    (case t of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    34
      _ $ _ =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    35
        op :: (strip_comb t)
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    36
        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    37
        |> Pretty.separate " $"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    38
        |> (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
    39
    | 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
    40
        prt_apps "Abs"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    41
         [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
    42
          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
    43
          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
    44
    | 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
    45
    | 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
    46
    | 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
    47
    | 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
    48
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    49
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    50
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    51
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    52
  PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
62503
19afb533028e clarified modules;
wenzelm
parents: 62387
diff changeset
    53
    ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
52426
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
local
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
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
    58
  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
    59
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    60
    (case prf of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    61
      _ % _ => 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
    62
    | _ %% _ => 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
    63
    | 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
    64
        prt_apps "Abst"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    65
         [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
    66
          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
    67
          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
    68
    | 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
    69
        prt_apps "AbsP"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    70
         [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
    71
          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
    72
          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
    73
    | 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
    74
    | 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
    75
    | 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
    76
    | 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
    77
    | 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
    78
    | 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
    79
    | 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
    80
    | 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
    81
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    82
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
    83
  let
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    84
    val (head, args) = strip_proof prf [];
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    85
    val prts =
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    86
      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    87
  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
    88
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    89
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
    90
      strip_proof p
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    91
        ((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
    92
  | 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
    93
      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
    94
  | 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
    95
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    96
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    97
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    98
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    99
  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
62503
19afb533028e clarified modules;
wenzelm
parents: 62387
diff changeset
   100
    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   101
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   102
end;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   103
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   104
end;