src/Pure/Syntax/printer.ML
author berghofe
Fri, 15 Mar 1996 12:01:19 +0100
changeset 1580 e3fd931e6095
parent 1509 7f693bb0d7dd
child 2200 2538977e94fa
permissions -rw-r--r--
Added some functions which allow redirection of Isabelle's output
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 =
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
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
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    13
  val show_no_free_types: bool ref
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    14
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
signature PRINTER =
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    17
  sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  include PRINTER0
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    19
  val term_to_ast: (string -> (term list -> term) option) -> term -> Ast.ast
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    20
  val typ_to_ast: (string -> (term list -> term) option) -> typ -> Ast.ast
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    21
  type prtab
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    22
  val empty_prtab: prtab
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    23
  val extend_prtab: prtab -> SynExt.xprod list -> prtab
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    24
  val merge_prtabs: prtab -> prtab -> prtab
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    25
  val pretty_term_ast: bool -> prtab -> (string -> (Ast.ast list -> Ast.ast) option)
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    26
    -> Ast.ast -> Pretty.T
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    27
  val pretty_typ_ast: bool -> prtab -> (string -> (Ast.ast list -> Ast.ast) option)
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    28
    -> Ast.ast -> Pretty.T
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    29
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    31
structure Printer : PRINTER =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
struct
1509
7f693bb0d7dd Elimination of fully-functorial style.
paulson
parents: 1089
diff changeset
    33
open Lexicon Ast SynExt TypeExt SynTrans;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(** options for printing **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val show_types = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val show_sorts = ref false;
504
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    39
val show_brackets = ref false;
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    40
val show_no_free_types = ref false;
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    41
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    44
(** convert term or typ to ast **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    46
fun apply_trans name a f args =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    47
  (f args handle
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    Match => raise Match
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
  | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun ast_of_term trf show_types show_sorts tm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  let
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    54
    val no_freeTs = ! show_no_free_types;
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    55
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    fun prune_typs (t_seen as (Const _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
      | prune_typs (t as Free (x, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
          if ty = dummyT then (t, seen)
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    59
          else if no_freeTs orelse t mem seen then (free x, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
      | prune_typs (t as Var (xi, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
          if ty = dummyT then (t, seen)
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    63
          else if no_freeTs orelse t mem seen then (var xi, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
      | prune_typs (t_seen as (Bound _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
      | prune_typs (Abs (x, ty, t), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
          let val (t', seen') = prune_typs (t, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
          in (Abs (x, ty, t'), seen') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
      | prune_typs (t1 $ t2, seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
            val (t1', seen') = prune_typs (t1, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
            val (t2', seen'') = prune_typs (t2, seen');
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
          in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
            (t1' $ t2', seen'')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
          end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
    fun ast_of (Const (a, _)) = trans a []
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
    79
      | ast_of (Free (x, ty)) = constrain x (free x) ty
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
    80
      | ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (var xi) ty
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
      | ast_of (Bound i) = Variable ("B." ^ string_of_int i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
      | ast_of (t as Abs _) = ast_of (abs_tr' t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
      | ast_of (t as _ $ _) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
          (case strip_comb t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
            (Const (a, _), args) => trans a args
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
          | (f, args) => Appl (map ast_of (f :: args)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    and trans a args =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
      (case trf a of
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    90
        Some f => ast_of (apply_trans "print translation" a f args)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
      | None => raise Match)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
          handle Match => mk_appl (Constant a) (map ast_of args)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
    and constrain x t ty =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
      if show_types andalso ty <> dummyT then
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
    96
        ast_of (const constrainC $ t $ term_of_typ show_sorts ty)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
      else Variable x;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  in
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
    99
    if show_types then
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   100
      ast_of (#1 (prune_typs (prop_tr' show_sorts tm, [])))
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   101
    else ast_of (prop_tr' show_sorts tm)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
(* term_to_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
fun term_to_ast trf tm =
1089
e679617661bc Now show_sorts:=true causes printing of types
lcp
parents: 922
diff changeset
   108
  ast_of_term trf (!show_types orelse !show_sorts) (!show_sorts) tm;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
(* typ_to_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
fun typ_to_ast trf ty =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  ast_of_term trf false false (term_of_typ (! show_sorts) ty);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   118
(** type prtab **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
datatype symb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
  Arg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
  TypArg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
  String of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  Break of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
  Block of int * symb list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   127
type prtab = (symb list * int * int) Symtab.table;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   128
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   129
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   130
(* xprods_to_fmts *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   131
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   132
fun xprod_to_fmt (XProd (_, _, "", _)) = None
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   133
  | xprod_to_fmt (XProd (_, xsymbs, const, pri)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   134
      let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   135
        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
   136
          | cons_str s syms = String s :: syms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   137
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   138
        fun arg (s, p) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   139
          (if s = "type" then TypArg else Arg)
506
e0ca460d6e51 improved show_brackets again - Trueprop does not create () any more.
nipkow
parents: 505
diff changeset
   140
          (if is_terminal s then max_pri else p);
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   141
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   142
        fun xsyms_to_syms (Delim s :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   143
              apfst (cons_str s) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   144
          | xsyms_to_syms (Argument s_p :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   145
              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
   146
          | xsyms_to_syms (Space s :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   147
              apfst (cons_str s) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   148
          | xsyms_to_syms (Bg i :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   149
              let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   150
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   151
                val (syms, xsyms'') = xsyms_to_syms xsyms';
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   152
              in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   153
                (Block (i, bsyms) :: syms, xsyms'')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   154
              end
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   155
          | xsyms_to_syms (Brk i :: xsyms) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   156
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   157
          | xsyms_to_syms (En :: xsyms) = ([], xsyms)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   158
          | xsyms_to_syms [] = ([], []);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   159
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   160
        fun nargs (Arg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   161
          | nargs (TypArg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   162
          | nargs (String _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   163
          | nargs (Break _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   164
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   165
          | nargs [] = 0;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   166
      in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   167
        (case xsyms_to_syms xsymbs of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   168
          (symbs, []) => Some (const, (symbs, nargs symbs, pri))
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   169
        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   170
      end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   171
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   172
fun xprods_to_fmts xprods =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   173
  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
   174
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   175
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   176
(* empty, extend, merge prtabs *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   177
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   178
fun err_dup_fmts cs =
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   179
  error ("Duplicate formats in printer table for " ^ commas_quote cs);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   180
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   181
val empty_prtab = Symtab.null;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   183
fun extend_prtab tab xprods =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   184
  Symtab.extend (op =) (tab, xprods_to_fmts xprods)
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   185
    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
   186
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   187
fun merge_prtabs tab1 tab2 =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   188
  Symtab.merge (op =) (tab1, tab2)
381
8af09380c517 replaced fix_aprop by prop_tr';
wenzelm
parents: 258
diff changeset
   189
    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
   190
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   193
(** pretty term or typ asts **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   195
fun chain [Block (_, pr)] = chain pr
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   196
  | chain [Arg _] = true
506
e0ca460d6e51 improved show_brackets again - Trueprop does not create () any more.
nipkow
parents: 505
diff changeset
   197
  | chain _  = false;
e0ca460d6e51 improved show_brackets again - Trueprop does not create () any more.
nipkow
parents: 505
diff changeset
   198
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   199
fun pretty prtab trf type_mode curried ast0 p0 =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   201
    val trans = apply_trans "print ast translation";
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   202
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   203
    val appT = if type_mode then tappl_ast_tr' else
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   204
               if curried then applC_ast_tr' else appl_ast_tr';
18
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')
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   215
            else (pretty prtab trf true curried t p @ Ts, args')
237
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
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   230
    and parT (pr, args, p, p': int) = #1 (synT
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   231
          (if p > p' orelse
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   232
            (! show_brackets andalso p' <> max_pri andalso not (chain pr))
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   233
            then [Block (1, String "(" :: pr @ [String ")"])]
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   234
            else pr, args))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    and prefixT (_, a, [], _) = [Pretty.str a]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
      | prefixT (c, _, args, p) = astT (appT (c, args), p)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   239
    and splitT 0 ([x], ys) = (x, ys)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   240
      | splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   241
      | 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
   242
      | splitT _ _ = sys_error "splitT"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   243
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
    and combT (tup as (c, a, args, p)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
        val nargs = length args;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   247
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
        fun prnt (pr, n, p') =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   249
          if nargs = n then parT (pr, args, p, p')
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   250
          else if nargs < n orelse type_mode then prefixT tup
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   251
          else astT (appT (splitT n ([c], args)), p);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
      in
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   253
        (case (trf a, Symtab.lookup (prtab, a)) of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   254
          (None, None) => prefixT tup
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   255
        | (None, Some prnp) => prnt prnp
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   256
        | (Some f, None) =>
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   257
            (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
   258
        | (Some f, Some prnp) =>
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   259
            (astT (trans a f args, p) handle Match => prnt prnp))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
      end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
    and astT (c as Constant a, p) = combT (c, a, [], p)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
      | astT (Variable x, _) = [Pretty.str x]
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
      | astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   265
          combT (c, a, args, p)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
      | astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   267
      | astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
    astT (ast0, p0)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
(* pretty_term_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   275
fun pretty_term_ast curried prtab trf ast =
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   276
  Pretty.blk (0, pretty prtab trf false curried ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
(* pretty_typ_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   281
fun pretty_typ_ast _ prtab trf ast =
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 617
diff changeset
   282
  Pretty.blk (0, pretty prtab trf true false ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286