Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: printer.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Syntax/printer.ML
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

Pretty printing of asts, terms, types and print (ast) translation.
*)

signature BASIC_PRINTER =
sig
  val show_brackets: bool Config.T
  val show_types: bool Config.T
  val show_sorts: bool Config.T
  val show_markup: bool Config.T
  val show_structs: bool Config.T
  val show_question_marks: bool Config.T
  val pretty_priority: int Config.T
end;

signature PRINTER =
sig
  include BASIC_PRINTER
  val show_markup_default: bool Unsynchronized.ref
  val show_type_emphasis: bool Config.T
  val type_emphasis: Proof.context -> typ -> bool
  type prtabs
  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
  val get_prefix: prtabs -> Symtab.key -> string option
  val get_binder: prtabs -> Symtab.key -> string option
  val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
  val empty_prtabs: prtabs
  val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
  val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
  val merge_prtabs: prtabs -> prtabs -> prtabs
  val pretty_term_ast: bool -> Proof.context -> prtabs ->
    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
    (string -> Ast.ast list -> Pretty.T option) ->
    (string -> Markup.T list * string) ->
    Ast.ast -> Pretty.T list
  val pretty_typ_ast: Proof.context -> prtabs ->
    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
    (string -> Ast.ast list -> Pretty.T option) ->
    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
end;

structure Printer: PRINTER =
struct

(** options for printing **)

val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
val show_types = Config.declare_option_bool ("show_types", \<^here>);
val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
val show_markup_default = Unsynchronized.ref false;
val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false);
val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>);
val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true);

fun type_emphasis ctxt T =
  T <> dummyT andalso
    (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
      Config.get ctxt show_type_emphasis andalso not (is_Type T));

(** type prtabs **)

datatype symb =
  Arg of int |
  TypArg of int |
  String of bool * string |
  Break of int |
  Block of Syntax_Ext.block_info * symb list;

type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;

fun mode_tab (prtabs: prtabs) mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);

fun lookup_default prtabs = Symtab.lookup_list (mode_tab prtabs "");

(* approximative syntax *)

datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;

local

fun is_arg (Arg _) = true
  | is_arg (TypArg _) = true
  | is_arg _ = false;

fun is_space str = forall_string (fn s => s = " ") str;

fun clean symbs = symbs |> maps
  (fn Block (_, body) => clean body
    | symb as String (_, s) => if is_space s then [] else [symb]
    | symb => if is_arg symb then [symb] else []);

in

fun get_prefix prtabs c =
  lookup_default prtabs c
  |> get_first (fn (symbs, _, _) =>
      (case clean symbs of
        String (_, d) :: rest => if forall is_arg rest then SOME d else NONE
      | _ => NONE));

fun get_binder prtabs c =
  lookup_default prtabs (Mixfix.binder_name c)
  |> get_first (fn (symbs, _, _) =>
      (case clean symbs of
        String (_, d) :: _ => SOME d
      | _ => NONE));

fun get_infix prtabs c =
  lookup_default prtabs c
  |> map_filter (fn (symbs, _, p) =>
      (case clean symbs of
        [Arg p1, String (_, d), Arg p2] => SOME (p1, p2, d, p)
      | [TypArg p1, String (_, d), TypArg p2] => SOME (p1, p2, d, p)
      | _ => NONE))
  |> get_first (fn (p1, p2, d, p) =>
      if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
      else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = d, pri = p}
      else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
      else NONE);

end;

(* xprod_to_fmt *)

fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
  | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
      let
        fun arg (s, p) =
          (if s = "type" then TypArg else Arg)
          (if Lexicon.is_terminal s then 1000 else p);

        fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
              apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
                (xsyms_to_syms xsyms)
          | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
          | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
              apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
          | xsyms_to_syms (Syntax_Ext.Bg info :: xsyms) =
              let
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
                val (syms, xsyms'') = xsyms_to_syms xsyms';
              in
                (Block (info, bsyms) :: syms, xsyms'')
              end
          | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
          | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
          | xsyms_to_syms [] = ([], []);

        fun nargs (Arg _ :: syms) = nargs syms + 1
          | nargs (TypArg _ :: syms) = nargs syms + 1
          | nargs (String _ :: syms) = nargs syms
          | nargs (Break _ :: syms) = nargs syms
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
          | nargs [] = 0;
      in
        (case xsyms_to_syms xsymbs of
          (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
        | _ => raise Fail "Unbalanced pretty-printing blocks")
      end;

(* empty, extend, merge prtabs *)

val empty_prtabs = [];

fun update_prtabs mode xprods prtabs =
  let
    val fmts = map_filter xprod_to_fmt xprods;
    val tab' = fold (Symtab.update_list (op =)) fmts (mode_tab prtabs mode);
  in AList.update (op =) (mode, tab') prtabs end;

fun remove_prtabs mode xprods prtabs =
  let
    val tab = mode_tab prtabs mode;
    val fmts = map_filter (fn xprod as Syntax_Ext.XProd (_, _, c, _) =>
      if null (Symtab.lookup_list tab c) then NONE
      else xprod_to_fmt xprod) xprods;
    val tab' = fold (Symtab.remove_list (op =)) fmts tab;
  in AList.update (op =) (mode, tab') prtabs end;

fun merge_prtabs prtabs1 prtabs2 =
  let
    val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
    fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
  in map merge modes end;

(** pretty term or typ asts **)

fun is_chain [Block (_, pr)] = is_chain pr
  | is_chain [Arg _] = true
  | is_chain _  = false;

val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);

fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
  let
    val show_brackets = Config.get ctxt show_brackets;

    (*default applications: prefix / postfix*)
    val appT =
      if type_mode then Syntax_Trans.tappl_ast_tr'
      else if curried then Syntax_Trans.applC_ast_tr'
      else Syntax_Trans.appl_ast_tr';

    fun synT _ ([], args) = ([], args)
      | synT m (Arg p :: symbs, t :: args) =
          let val (Ts, args') = synT m (symbs, args);
          in (astT (t, p) @ Ts, args') end
      | synT m (TypArg p :: symbs, t :: args) =
          let
            val (Ts, args') = synT m (symbs, args);
          in
            if type_mode then (astT (t, p) @ Ts, args')
            else
              (pretty true curried (Config.put pretty_priority p ctxt)
                tabs trf markup_trans markup_extern t @ Ts, args')
          end
      | synT m (String (do_mark, s) :: symbs, args) =
          let
            val (Ts, args') = synT m (symbs, args);
            val T =
              if do_mark
              then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
              else Pretty.str s;
          in (T :: Ts, args') end
      | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
          let
            val (bTs, args') = synT m (bsymbs, args);
            val (Ts, args'') = synT m (symbs, args');
            val T =
              Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs
              |> unbreakable ? Pretty.unbreakable;
          in (T :: Ts, args'') end
      | synT m (Break i :: symbs, args) =
          let
            val (Ts, args') = synT m (symbs, args);
            val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
          in (T :: Ts, args') end

    and parT m (pr, args, p, p': int) = #1 (synT m
          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
            [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
           else pr, args))

    and atomT a = Pretty.marks_str (markup_extern a)

    and prefixT (_, a, [], _) = [atomT a]
      | prefixT (c, _, args, p) = astT (appT (c, args), p)

    and splitT 0 ([x], ys) = (x, ys)
      | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
      | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)

    and combT (tup as (c, a, args, p)) =
      let
        val nargs = length args;

        (*find matching table entry, or print as prefix / postfix*)
        fun prnt ([], []) = prefixT tup
          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
          | prnt ((pr, n, p') :: prnps, tbs) =
              if nargs = n then parT (#1 (markup_extern a)) (pr, args, p, p')
              else if nargs > n andalso not type_mode then
                astT (appT (splitT n ([c], args)), p)
              else prnt (prnps, tbs);
      in
        (case markup_trans a args of
          SOME prt => [prt]
        | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
      end

    and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
      | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast]
      | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
      | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
      | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
  in astT (ast0, Config.get ctxt pretty_priority) end;

(* pretty_term_ast *)

fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast =
  pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;

(* pretty_typ_ast *)

fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast =
  pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;

end;

structure Basic_Printer: BASIC_PRINTER = Printer;
open Basic_Printer;

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.