src/Pure/Syntax/printer.ML
author nipkow
Tue, 02 Aug 1994 20:08:57 +0200
changeset 505 97eb677142d9
parent 504 a4f09493d929
child 506 e0ca460d6e51
permissions -rw-r--r--
minimized () in forced printing of barckets (show_brackets)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/printer.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     4
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
Pretty printing of asts, terms, types and print (ast) translation.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
signature PRINTER0 =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
sig
504
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    10
  val show_brackets: bool ref
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    11
  val show_sorts: bool ref
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val show_types: bool ref
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
signature PRINTER =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  include PRINTER0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  structure Symtab: SYMTAB
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    19
  structure SynExt: SYN_EXT
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
    20
  local open SynExt SynExt.Ast in
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    val term_to_ast: (string -> (term list -> term) option) -> term -> ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
    val typ_to_ast: (string -> (term list -> term) option) -> typ -> ast
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    23
    type prtab
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    24
    val empty_prtab: prtab
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    25
    val extend_prtab: prtab -> xprod list -> prtab
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    26
    val merge_prtabs: prtab -> prtab -> prtab
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    27
    val pretty_term_ast: prtab -> (string -> (ast list -> ast) option)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    28
      -> ast -> Pretty.T
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    29
    val pretty_typ_ast: prtab -> (string -> (ast list -> ast) option)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    30
      -> ast -> Pretty.T
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    34
functor PrinterFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    35
  and SExtension: SEXTENSION sharing TypeExt.SynExt = SExtension.Parser.SynExt)
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 237
diff changeset
    36
  : PRINTER =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
structure Symtab = Symtab;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    40
structure SynExt = TypeExt.SynExt;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
    41
open SExtension.Parser.Lexicon SynExt.Ast SynExt TypeExt SExtension;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(** options for printing **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val show_types = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val show_sorts = ref false;
504
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    48
val show_brackets = ref false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    51
(** convert term or typ to ast **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    53
fun apply_trans name a f args =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    54
  (f args handle
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    Match => raise Match
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    56
  | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
fun ast_of_term trf show_types show_sorts tm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    fun prune_typs (t_seen as (Const _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
      | prune_typs (t as Free (x, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
          if ty = dummyT then (t, seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
          else if t mem seen then (Free (x, dummyT), seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
      | prune_typs (t as Var (xi, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
          if ty = dummyT then (t, seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
          else if t mem seen then (Var (xi, dummyT), seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
      | prune_typs (t_seen as (Bound _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
      | prune_typs (Abs (x, ty, t), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
          let val (t', seen') = prune_typs (t, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
          in (Abs (x, ty, t'), seen') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
      | prune_typs (t1 $ t2, seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
            val (t1', seen') = prune_typs (t1, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
            val (t2', seen'') = prune_typs (t2, seen');
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
          in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
            (t1' $ t2', seen'')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
          end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
    fun ast_of (Const (a, _)) = trans a []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
      | ast_of (Free (x, ty)) = constrain x (Free (x, dummyT)) ty
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
      | ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (Var (xi, dummyT)) ty
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
      | ast_of (Bound i) = Variable ("B." ^ string_of_int i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
      | ast_of (t as Abs _) = ast_of (abs_tr' t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
      | ast_of (t as _ $ _) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
          (case strip_comb t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
            (Const (a, _), args) => trans a args
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
          | (f, args) => Appl (map ast_of (f :: args)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
    and trans a args =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
      (case trf a of
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    95
        Some f => ast_of (apply_trans "print translation" a f args)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
      | None => raise Match)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
          handle Match => mk_appl (Constant a) (map ast_of args)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    and constrain x t ty =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
      if show_types andalso ty <> dummyT then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
        ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
      else Variable x;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  in
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   104
    if show_types then
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   105
      ast_of (#1 (prune_typs (prop_tr' show_sorts tm, [])))
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   106
    else ast_of (prop_tr' show_sorts tm)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(* term_to_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
fun term_to_ast trf tm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  ast_of_term trf (! show_types) (! show_sorts) tm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(* typ_to_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun typ_to_ast trf ty =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
  ast_of_term trf false false (term_of_typ (! show_sorts) ty);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   123
(** type prtab **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
datatype symb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
  Arg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
  TypArg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
  String of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
  Break of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
  Block of int * symb list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   132
type prtab = (symb list * int * int) Symtab.table;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   133
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   134
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   135
(* xprods_to_fmts *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   136
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   137
fun xprod_to_fmt (XProd (_, _, "", _)) = None
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   138
  | xprod_to_fmt (XProd (_, xsymbs, const, pri)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   139
      let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   140
        fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   141
          | cons_str s syms = String s :: syms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   142
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   143
        fun arg (s, p) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   144
          (if s = "type" then TypArg else Arg)
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   145
          (if is_terminal s then 1000 else p);
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   146
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   147
        fun xsyms_to_syms (Delim s :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   148
              apfst (cons_str s) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   149
          | xsyms_to_syms (Argument s_p :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   150
              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   151
          | xsyms_to_syms (Space s :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   152
              apfst (cons_str s) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   153
          | xsyms_to_syms (Bg i :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   154
              let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   155
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   156
                val (syms, xsyms'') = xsyms_to_syms xsyms';
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   157
              in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   158
                (Block (i, bsyms) :: syms, xsyms'')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   159
              end
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   160
          | xsyms_to_syms (Brk i :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   161
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   162
          | xsyms_to_syms (En :: xsyms) = ([], xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   163
          | xsyms_to_syms [] = ([], []);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   164
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   165
        fun nargs (Arg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   166
          | nargs (TypArg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   167
          | nargs (String _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   168
          | nargs (Break _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   169
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   170
          | nargs [] = 0;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   171
      in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   172
        (case xsyms_to_syms xsymbs of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   173
          (symbs, []) => Some (const, (symbs, nargs symbs, pri))
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   174
        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   175
      end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   176
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   177
fun xprods_to_fmts xprods =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   178
  gen_distinct eq_fst (mapfilter xprod_to_fmt xprods);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   179
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   180
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   181
(* empty, extend, merge prtabs *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   182
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   183
fun err_dup_fmts cs =
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   184
  error ("Duplicate formats in printer table for " ^ commas_quote cs);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   185
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   186
val empty_prtab = Symtab.null;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   188
fun extend_prtab tab xprods =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   189
  Symtab.extend (op =) (tab, xprods_to_fmts xprods)
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   190
    handle Symtab.DUPS cs => err_dup_fmts cs;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   191
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   192
fun merge_prtabs tab1 tab2 =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   193
  Symtab.merge (op =) (tab1, tab2)
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   194
    handle Symtab.DUPS cs => err_dup_fmts cs;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   195
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   198
(** pretty term or typ asts **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   200
fun pretty prtab trf type_mode ast0 p0 =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   202
    val trans = apply_trans "print ast translation";
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   203
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   204
    val appT = if type_mode then tappl_ast_tr' else appl_ast_tr';
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   205
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
    fun synT ([], args) = ([], args)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
      | synT (Arg p :: symbs, t :: args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   208
          let val (Ts, args') = synT (symbs, args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
          in (astT (t, p) @ Ts, args') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
      | synT (TypArg p :: symbs, t :: args) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   211
          let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   212
            val (Ts, args') = synT (symbs, args);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   213
          in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   214
            if type_mode then (astT (t, p) @ Ts, args')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   215
            else (pretty prtab trf true t p @ Ts, args')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   216
          end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
      | synT (String s :: symbs, args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   218
          let val (Ts, args') = synT (symbs, args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
          in (Pretty.str s :: Ts, args') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
      | synT (Block (i, bsymbs) :: symbs, args) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
            val (bTs, args') = synT (bsymbs, args);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
            val (Ts, args'') = synT (symbs, args');
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
          in (Pretty.blk (i, bTs) :: Ts, args'') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
      | synT (Break i :: symbs, args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   226
          let val (Ts, args') = synT (symbs, args);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   227
          in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   228
      | synT (_ :: _, []) = sys_error "synT"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
    and parT (pr, args, p, p': int) =
505
97eb677142d9 minimized () in forced printing of barckets (show_brackets)
nipkow
parents: 504
diff changeset
   231
      if p > p' orelse (!show_brackets andalso p' <> max_pri) then
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   232
        #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   233
      else #1 (synT (pr, args))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
    and prefixT (_, a, [], _) = [Pretty.str a]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
      | prefixT (c, _, args, p) = astT (appT (c, args), p)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   238
    and splitT 0 ([x], ys) = (x, ys)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   239
      | splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   240
      | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   241
      | splitT _ _ = sys_error "splitT"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   242
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
    and combT (tup as (c, a, args, p)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
        val nargs = length args;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   246
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
        fun prnt (pr, n, p') =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   248
          if nargs = n then parT (pr, args, p, p')
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   249
          else if nargs < n orelse type_mode then prefixT tup
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   250
          else astT (appT (splitT n ([c], args)), p);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
      in
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   252
        (case (trf a, Symtab.lookup (prtab, a)) of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   253
          (None, None) => prefixT tup
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   254
        | (None, Some prnp) => prnt prnp
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   255
        | (Some f, None) =>
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   256
            (astT (trans a f args, p) handle Match => prefixT tup)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   257
        | (Some f, Some prnp) =>
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   258
            (astT (trans a f args, p) handle Match => prnt prnp))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
      end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
    and astT (c as Constant a, p) = combT (c, a, [], p)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
      | astT (Variable x, _) = [Pretty.str x]
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   263
      | astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
          combT (c, a, args, p)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
      | astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
      | astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
    astT (ast0, p0)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
(* pretty_term_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   274
fun pretty_term_ast prtab trf ast =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   275
  Pretty.blk (0, pretty prtab trf false ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
(* pretty_typ_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   280
fun pretty_typ_ast prtab trf ast =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   281
  Pretty.blk (0, pretty prtab trf true ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285