Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: unityl.c Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/ML/ml_pp.ML
    Author:     Makarius

ML toplevel pretty-printing for logical entities.
*)

structure ML_PP: sig end =
struct

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

val _ =
  ML_system_pp (fn depth => fn _ =>
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure);

val _ =
  ML_system_pp (fn depth => fn _ =>
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure);

val _ =
  ML_system_pp (fn depth => fn _ =>
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure);

val _ =
  ML_system_pp (fn depth => fn _ =>
    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);

local

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

fun prt_term parens (dp: FixedInt.int) t =
  if dp <= 0 then Pretty.str "..."
  else
    (case t of
      _ $ _ =>
        op :: (strip_comb t)
        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
        |> Pretty.separate " $"
        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    | Abs (a, T, b) =>
        prt_apps "Abs"
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
          prt_term false (dp - 3) b]
    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));

in

val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);

local

fun prt_proof parens dp prf =
  if dp <= 0 then Pretty.str "..."
  else
    (case prf of
      _ % _ => prt_proofs parens dp prf
    | _ %% _ => prt_proofs parens dp prf
    | Abst (a, T, b) =>
        prt_apps "Abst"
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
          prt_proof false (dp - 3) b]
    | AbsP (a, t, b) =>
        prt_apps "AbsP"
         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
          prt_proof false (dp - 3) b]
    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
    | MinProof => Pretty.str "MinProof"
    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | PClass a => prt_app "PClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))

and prt_proofs parens dp prf =
  let
    val (head, args) = strip_proof prf [];
    val prts =
      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end

and strip_proof (p % t) res =
      strip_proof p
        ((fn d =>
          [Pretty.str " %", Pretty.brk 1,
            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
  | strip_proof (p %% q) res =
      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
  | strip_proof p res = (fn d => prt_proof true d p, res);

in

val _ =
  ML_system_pp (fn depth => fn _ => fn prf =>
    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));

end;

end;

end;

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.