src/Pure/ML/ml_pp.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62819 d3ff367a16a0
child 67380 8bef51521f21
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62665
     1
(*  Title:      Pure/ML/ml_pp.ML
wenzelm@38327
     2
    Author:     Makarius
wenzelm@30633
     3
wenzelm@62665
     4
ML toplevel pretty-printing for logical entities.
wenzelm@30633
     5
*)
wenzelm@30633
     6
wenzelm@62665
     7
structure ML_PP: sig end =
wenzelm@62665
     8
struct
wenzelm@62356
     9
wenzelm@62665
    10
val _ =
wenzelm@62819
    11
  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
wenzelm@62665
    12
wenzelm@62665
    13
val _ =
wenzelm@62819
    14
  ML_system_pp (fn depth => fn _ =>
wenzelm@62673
    15
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
wenzelm@62356
    16
wenzelm@62665
    17
val _ =
wenzelm@62819
    18
  ML_system_pp (fn depth => fn _ =>
wenzelm@62673
    19
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
wenzelm@62356
    20
wenzelm@62665
    21
val _ =
wenzelm@62819
    22
  ML_system_pp (fn depth => fn _ =>
wenzelm@62673
    23
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
wenzelm@33767
    24
wenzelm@62665
    25
val _ =
wenzelm@62819
    26
  ML_system_pp (fn depth => fn _ =>
wenzelm@62673
    27
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
wenzelm@30633
    28
wenzelm@52426
    29
wenzelm@52426
    30
local
wenzelm@52426
    31
wenzelm@52426
    32
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
wenzelm@52426
    33
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
wenzelm@52426
    34
wenzelm@62387
    35
fun prt_term parens (dp: FixedInt.int) t =
wenzelm@52426
    36
  if dp <= 0 then Pretty.str "..."
wenzelm@52426
    37
  else
wenzelm@52426
    38
    (case t of
wenzelm@52426
    39
      _ $ _ =>
wenzelm@52426
    40
        op :: (strip_comb t)
wenzelm@62387
    41
        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
wenzelm@52426
    42
        |> Pretty.separate " $"
wenzelm@52426
    43
        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
wenzelm@52426
    44
    | Abs (a, T, b) =>
wenzelm@52426
    45
        prt_apps "Abs"
wenzelm@62819
    46
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
wenzelm@62819
    47
          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
wenzelm@52426
    48
          prt_term false (dp - 3) b]
wenzelm@62819
    49
    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    50
    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    51
    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    52
    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
wenzelm@52426
    53
wenzelm@52426
    54
in
wenzelm@52426
    55
wenzelm@62819
    56
val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
wenzelm@62665
    57
wenzelm@52426
    58
wenzelm@52426
    59
local
wenzelm@52426
    60
wenzelm@52426
    61
fun prt_proof parens dp prf =
wenzelm@52426
    62
  if dp <= 0 then Pretty.str "..."
wenzelm@52426
    63
  else
wenzelm@52426
    64
    (case prf of
wenzelm@52426
    65
      _ % _ => prt_proofs parens dp prf
wenzelm@52426
    66
    | _ %% _ => prt_proofs parens dp prf
wenzelm@52426
    67
    | Abst (a, T, b) =>
wenzelm@52426
    68
        prt_apps "Abst"
wenzelm@62819
    69
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
wenzelm@62819
    70
          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
wenzelm@52426
    71
          prt_proof false (dp - 3) b]
wenzelm@52426
    72
    | AbsP (a, t, b) =>
wenzelm@52426
    73
        prt_apps "AbsP"
wenzelm@62819
    74
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
wenzelm@62819
    75
          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
wenzelm@52426
    76
          prt_proof false (dp - 3) b]
wenzelm@52426
    77
    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
wenzelm@52426
    78
    | MinProof => Pretty.str "MinProof"
wenzelm@62819
    79
    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    80
    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    81
    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    82
    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    83
    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
wenzelm@62819
    84
    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
wenzelm@52426
    85
wenzelm@52426
    86
and prt_proofs parens dp prf =
wenzelm@33545
    87
  let
wenzelm@52426
    88
    val (head, args) = strip_proof prf [];
wenzelm@62387
    89
    val prts =
wenzelm@62387
    90
      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
wenzelm@52426
    91
  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
wenzelm@52426
    92
wenzelm@52426
    93
and strip_proof (p % t) res =
wenzelm@52426
    94
      strip_proof p
wenzelm@62665
    95
        ((fn d =>
wenzelm@62665
    96
          [Pretty.str " %", Pretty.brk 1,
wenzelm@62819
    97
            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
wenzelm@52426
    98
  | strip_proof (p %% q) res =
wenzelm@52426
    99
      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
wenzelm@52426
   100
  | strip_proof p res = (fn d => prt_proof true d p, res);
wenzelm@33545
   101
wenzelm@52426
   102
in
wenzelm@52426
   103
wenzelm@52426
   104
val _ =
wenzelm@62819
   105
  ML_system_pp (fn depth => fn _ => fn prf =>
wenzelm@62667
   106
    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
wenzelm@52426
   107
wenzelm@52426
   108
end;
wenzelm@52426
   109
wenzelm@52426
   110
end;
wenzelm@62665
   111
wenzelm@62665
   112
end;