src/Pure/Syntax/printer.ML
author oheimb
Fri Jan 29 17:10:26 1999 +0100 (1999-01-29)
changeset 6164 a0e9501d56f8
parent 5691 3a6de95c09d0
child 6273 94ce639eb7e5
permissions -rw-r--r--
moved print_mode to ROOT.ML
wenzelm@18
     1
(*  Title:      Pure/Syntax/printer.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@18
     4
wenzelm@18
     5
Pretty printing of asts, terms, types and print (ast) translation.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature PRINTER0 =
wenzelm@2384
     9
sig
nipkow@504
    10
  val show_brackets: bool ref
nipkow@504
    11
  val show_sorts: bool ref
clasohm@0
    12
  val show_types: bool ref
wenzelm@617
    13
  val show_no_free_types: bool ref
wenzelm@2384
    14
end;
clasohm@0
    15
clasohm@0
    16
signature PRINTER =
wenzelm@2384
    17
sig
clasohm@0
    18
  include PRINTER0
wenzelm@5691
    19
  val term_to_ast: (string -> (bool -> typ -> term list -> term) list) -> term -> Ast.ast
wenzelm@5691
    20
  val typ_to_ast: (string -> (bool -> typ -> term list -> term) list) -> typ -> Ast.ast
wenzelm@5691
    21
  val sort_to_ast: (string -> (bool -> typ -> term list -> term) list) -> sort -> Ast.ast
wenzelm@2200
    22
  type prtabs
wenzelm@2200
    23
  val empty_prtabs: prtabs
wenzelm@2200
    24
  val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
wenzelm@2200
    25
  val merge_prtabs: prtabs -> prtabs -> prtabs
wenzelm@2200
    26
  val pretty_term_ast: bool -> prtabs
wenzelm@5691
    27
    -> (string -> (Ast.ast list -> Ast.ast) list)
wenzelm@2701
    28
    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
wenzelm@2200
    29
  val pretty_typ_ast: bool -> prtabs
wenzelm@5691
    30
    -> (string -> (Ast.ast list -> Ast.ast) list)
wenzelm@2701
    31
    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
wenzelm@2384
    32
end;
clasohm@0
    33
wenzelm@2365
    34
structure Printer: PRINTER =
clasohm@0
    35
struct
wenzelm@2200
    36
wenzelm@2200
    37
clasohm@0
    38
(** options for printing **)
clasohm@0
    39
clasohm@0
    40
val show_types = ref false;
clasohm@0
    41
val show_sorts = ref false;
nipkow@504
    42
val show_brackets = ref false;
wenzelm@617
    43
val show_no_free_types = ref false;
wenzelm@617
    44
clasohm@0
    45
clasohm@0
    46
wenzelm@2701
    47
(** misc utils **)
wenzelm@2701
    48
wenzelm@2701
    49
(* apply print (ast) translation function *)
clasohm@0
    50
wenzelm@5691
    51
fun apply_first [] x = raise Match
wenzelm@5691
    52
  | apply_first (f :: fs) x = f x handle Match => apply_first fs x;
wenzelm@5691
    53
wenzelm@5691
    54
fun apply_trans name a fs args =
wenzelm@5691
    55
  (apply_first fs args handle
clasohm@0
    56
    Match => raise Match
wenzelm@18
    57
  | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
clasohm@0
    58
wenzelm@5691
    59
fun apply_typed x y fs = map (fn f => f x y) fs;
wenzelm@4147
    60
clasohm@0
    61
wenzelm@2701
    62
(* simple_ast_of *)
wenzelm@2701
    63
wenzelm@5691
    64
fun simple_ast_of (Const (c, _)) = Ast.Constant c
wenzelm@5691
    65
  | simple_ast_of (Free (x, _)) = Ast.Variable x
wenzelm@5691
    66
  | simple_ast_of (Var (xi, _)) = Ast.Variable (Lexicon.string_of_vname xi)
wenzelm@2701
    67
  | simple_ast_of (t as _ $ _) =
wenzelm@2701
    68
      let val (f, args) = strip_comb t in
wenzelm@5691
    69
        Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
wenzelm@2701
    70
      end
wenzelm@5691
    71
  | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
wenzelm@2701
    72
  | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
wenzelm@2701
    73
wenzelm@2701
    74
wenzelm@2701
    75
wenzelm@3776
    76
(** sort_to_ast, typ_to_ast **)
wenzelm@2701
    77
wenzelm@2701
    78
fun ast_of_termT trf tm =
clasohm@0
    79
  let
wenzelm@5691
    80
    (* FIXME improve: lookup token classes *)
wenzelm@2701
    81
    fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
wenzelm@2701
    82
      | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
wenzelm@2701
    83
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
wenzelm@2701
    84
      | ast_of (Const (a, _)) = trans a []
wenzelm@2701
    85
      | ast_of (t as _ $ _) =
wenzelm@2701
    86
          (case strip_comb t of
wenzelm@2701
    87
            (Const (a, _), args) => trans a args
wenzelm@5691
    88
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
wenzelm@5691
    89
      | ast_of t = simple_ast_of t
wenzelm@2701
    90
    and trans a args =
wenzelm@5691
    91
      ast_of (apply_trans "print translation" a (apply_typed false dummyT (trf a)) args)
wenzelm@5691
    92
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
wenzelm@5691
    93
  in ast_of tm end;
wenzelm@617
    94
wenzelm@5691
    95
fun sort_to_ast trf S = ast_of_termT trf (TypeExt.term_of_sort S);
wenzelm@5691
    96
fun typ_to_ast trf T = ast_of_termT trf (TypeExt.term_of_typ (! show_sorts) T);
wenzelm@2701
    97
wenzelm@2701
    98
wenzelm@2701
    99
wenzelm@2701
   100
(** term_to_ast **)
wenzelm@2701
   101
wenzelm@2701
   102
fun mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
wenzelm@2701
   103
  | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
wenzelm@5691
   104
  | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
wenzelm@5691
   105
  | mark_freevars (t as Var _) =  Lexicon.const "_var" $ t
wenzelm@2701
   106
  | mark_freevars a = a;
wenzelm@2701
   107
wenzelm@2701
   108
fun ast_of_term trf no_freeTs show_types show_sorts tm =
wenzelm@2701
   109
  let
clasohm@0
   110
    fun prune_typs (t_seen as (Const _, _)) = t_seen
clasohm@0
   111
      | prune_typs (t as Free (x, ty), seen) =
clasohm@0
   112
          if ty = dummyT then (t, seen)
wenzelm@5691
   113
          else if no_freeTs orelse t mem seen then (Lexicon.free x, seen)
clasohm@0
   114
          else (t, t :: seen)
clasohm@0
   115
      | prune_typs (t as Var (xi, ty), seen) =
clasohm@0
   116
          if ty = dummyT then (t, seen)
wenzelm@5691
   117
          else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen)
clasohm@0
   118
          else (t, t :: seen)
clasohm@0
   119
      | prune_typs (t_seen as (Bound _, _)) = t_seen
clasohm@0
   120
      | prune_typs (Abs (x, ty, t), seen) =
clasohm@0
   121
          let val (t', seen') = prune_typs (t, seen);
clasohm@0
   122
          in (Abs (x, ty, t'), seen') end
clasohm@0
   123
      | prune_typs (t1 $ t2, seen) =
clasohm@0
   124
          let
clasohm@0
   125
            val (t1', seen') = prune_typs (t1, seen);
clasohm@0
   126
            val (t2', seen'') = prune_typs (t2, seen');
clasohm@0
   127
          in
clasohm@0
   128
            (t1' $ t2', seen'')
clasohm@0
   129
          end;
clasohm@0
   130
wenzelm@2701
   131
    fun ast_of tm =
wenzelm@2701
   132
      (case strip_comb tm of
wenzelm@5691
   133
        (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
wenzelm@2701
   134
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
wenzelm@5691
   135
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
wenzelm@2701
   136
      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
wenzelm@5691
   137
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
wenzelm@2701
   138
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
wenzelm@5691
   139
          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
wenzelm@2701
   140
      | (Const (c, T), ts) => trans c T ts
wenzelm@5691
   141
      | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
clasohm@0
   142
wenzelm@2384
   143
    and trans a T args =
wenzelm@5691
   144
      ast_of (apply_trans "print translation" a (apply_typed show_sorts T (trf a)) args)
wenzelm@5691
   145
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
clasohm@0
   146
wenzelm@2701
   147
    and constrain t T =
wenzelm@2701
   148
      if show_types andalso T <> dummyT then
wenzelm@5691
   149
        Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
wenzelm@5691
   150
          ast_of_termT trf (TypeExt.term_of_typ show_sorts T)]
wenzelm@2701
   151
      else simple_ast_of t
clasohm@0
   152
  in
wenzelm@2701
   153
    tm
wenzelm@5691
   154
    |> SynTrans.prop_tr'
wenzelm@2701
   155
    |> (if show_types then #1 o prune_typs o rpair [] else I)
wenzelm@2701
   156
    |> mark_freevars
wenzelm@2701
   157
    |> ast_of
clasohm@0
   158
  end;
clasohm@0
   159
clasohm@0
   160
fun term_to_ast trf tm =
wenzelm@2701
   161
  ast_of_term trf (! show_no_free_types) (! show_types orelse ! show_sorts)
wenzelm@2701
   162
    (! show_sorts) tm;
clasohm@0
   163
clasohm@0
   164
clasohm@0
   165
wenzelm@2200
   166
(** type prtabs **)
clasohm@0
   167
clasohm@0
   168
datatype symb =
clasohm@0
   169
  Arg of int |
clasohm@0
   170
  TypArg of int |
clasohm@0
   171
  String of string |
clasohm@0
   172
  Break of int |
clasohm@0
   173
  Block of int * symb list;
clasohm@0
   174
wenzelm@2200
   175
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
wenzelm@2200
   176
wenzelm@3816
   177
wenzelm@2200
   178
(*find tab for mode*)
wenzelm@2200
   179
fun get_tab prtabs mode =
wenzelm@4487
   180
  if_none (assoc (prtabs, mode)) Symtab.empty;
wenzelm@2200
   181
wenzelm@2200
   182
(*collect tabs for mode hierarchy (default "")*)
wenzelm@2200
   183
fun tabs_of prtabs modes =
wenzelm@2200
   184
  mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]);
wenzelm@2200
   185
wenzelm@2200
   186
(*find formats in tab hierarchy*)
wenzelm@2200
   187
fun get_fmts [] _ = []
wenzelm@2200
   188
  | get_fmts (tab :: tabs) a = Symtab.lookup_multi (tab, a) @ get_fmts tabs a;
wenzelm@18
   189
wenzelm@18
   190
wenzelm@3816
   191
(* xprod_to_fmt *)
wenzelm@237
   192
wenzelm@5691
   193
fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = None
wenzelm@5691
   194
  | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
wenzelm@237
   195
      let
wenzelm@2384
   196
        fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
wenzelm@2384
   197
          | cons_str s syms = String s :: syms;
wenzelm@2384
   198
wenzelm@237
   199
        fun arg (s, p) =
wenzelm@237
   200
          (if s = "type" then TypArg else Arg)
wenzelm@5691
   201
          (if Lexicon.is_terminal s then SynExt.max_pri else p);
wenzelm@237
   202
wenzelm@5691
   203
        fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
wenzelm@4699
   204
              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
wenzelm@5691
   205
          | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
wenzelm@237
   206
              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
wenzelm@5691
   207
          | xsyms_to_syms (SynExt.Space s :: xsyms) =
wenzelm@4699
   208
              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
wenzelm@5691
   209
          | xsyms_to_syms (SynExt.Bg i :: xsyms) =
wenzelm@237
   210
              let
wenzelm@237
   211
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
wenzelm@237
   212
                val (syms, xsyms'') = xsyms_to_syms xsyms';
wenzelm@237
   213
              in
wenzelm@237
   214
                (Block (i, bsyms) :: syms, xsyms'')
wenzelm@237
   215
              end
wenzelm@5691
   216
          | xsyms_to_syms (SynExt.Brk i :: xsyms) =
wenzelm@237
   217
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
wenzelm@5691
   218
          | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
wenzelm@237
   219
          | xsyms_to_syms [] = ([], []);
wenzelm@237
   220
wenzelm@237
   221
        fun nargs (Arg _ :: syms) = nargs syms + 1
wenzelm@237
   222
          | nargs (TypArg _ :: syms) = nargs syms + 1
wenzelm@237
   223
          | nargs (String _ :: syms) = nargs syms
wenzelm@237
   224
          | nargs (Break _ :: syms) = nargs syms
wenzelm@237
   225
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
wenzelm@237
   226
          | nargs [] = 0;
wenzelm@237
   227
      in
wenzelm@237
   228
        (case xsyms_to_syms xsymbs of
wenzelm@237
   229
          (symbs, []) => Some (const, (symbs, nargs symbs, pri))
wenzelm@237
   230
        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
wenzelm@237
   231
      end;
wenzelm@237
   232
wenzelm@237
   233
wenzelm@237
   234
(* empty, extend, merge prtabs *)
wenzelm@237
   235
wenzelm@2200
   236
val empty_prtabs = [];
wenzelm@18
   237
wenzelm@2200
   238
fun extend_prtabs prtabs mode xprods =
wenzelm@2200
   239
  let
wenzelm@3816
   240
    val fmts = rev (mapfilter xprod_to_fmt xprods);
wenzelm@2200
   241
    val tab = get_tab prtabs mode;
wenzelm@3816
   242
    val new_tab =
wenzelm@3816
   243
      if null fmts then tab
wenzelm@3816
   244
      else Symtab.make_multi (fmts @ Symtab.dest_multi tab)     (*prefer new entries*)
wenzelm@2200
   245
  in overwrite (prtabs, (mode, new_tab)) end;
clasohm@0
   246
wenzelm@2200
   247
fun merge_prtabs prtabs1 prtabs2 =
wenzelm@2200
   248
  let
wenzelm@2200
   249
    val modes = distinct (map fst (prtabs1 @ prtabs2));
wenzelm@2200
   250
    fun merge mode =
wenzelm@2200
   251
      (mode,
wenzelm@2200
   252
        generic_merge (op =) Symtab.dest_multi Symtab.make_multi
wenzelm@3816
   253
          (get_tab prtabs2 mode) (get_tab prtabs1 mode));       (*prefer 2nd over 1st*)
wenzelm@2200
   254
  in
wenzelm@2200
   255
    map merge modes
wenzelm@2200
   256
  end;
wenzelm@237
   257
clasohm@0
   258
clasohm@0
   259
wenzelm@237
   260
(** pretty term or typ asts **)
clasohm@0
   261
wenzelm@2200
   262
fun is_chain [Block (_, pr)] = is_chain pr
wenzelm@2200
   263
  | is_chain [Arg _] = true
wenzelm@2200
   264
  | is_chain _  = false;
nipkow@506
   265
wenzelm@2701
   266
fun pretty tabs trf tokentrf type_mode curried ast0 p0 =
clasohm@0
   267
  let
wenzelm@18
   268
    val trans = apply_trans "print ast translation";
wenzelm@18
   269
wenzelm@5691
   270
    fun token_trans c [Ast.Variable x] =
wenzelm@2701
   271
          (case tokentrf c of
wenzelm@2701
   272
            None => None
wenzelm@2701
   273
          | Some f => Some (f x))
wenzelm@2701
   274
      | token_trans _ _ = None;
wenzelm@2701
   275
wenzelm@2200
   276
    (*default applications: prefix / postfix*)
wenzelm@2200
   277
    val appT =
wenzelm@5691
   278
      if type_mode then TypeExt.tappl_ast_tr'
wenzelm@5691
   279
      else if curried then SynTrans.applC_ast_tr'
wenzelm@5691
   280
      else SynTrans.appl_ast_tr';
wenzelm@18
   281
clasohm@0
   282
    fun synT ([], args) = ([], args)
clasohm@0
   283
      | synT (Arg p :: symbs, t :: args) =
wenzelm@18
   284
          let val (Ts, args') = synT (symbs, args);
clasohm@0
   285
          in (astT (t, p) @ Ts, args') end
clasohm@0
   286
      | synT (TypArg p :: symbs, t :: args) =
wenzelm@237
   287
          let
wenzelm@237
   288
            val (Ts, args') = synT (symbs, args);
wenzelm@237
   289
          in
wenzelm@237
   290
            if type_mode then (astT (t, p) @ Ts, args')
wenzelm@2701
   291
            else (pretty tabs trf tokentrf true curried t p @ Ts, args')
wenzelm@237
   292
          end
clasohm@0
   293
      | synT (String s :: symbs, args) =
wenzelm@18
   294
          let val (Ts, args') = synT (symbs, args);
clasohm@0
   295
          in (Pretty.str s :: Ts, args') end
clasohm@0
   296
      | synT (Block (i, bsymbs) :: symbs, args) =
clasohm@0
   297
          let
clasohm@0
   298
            val (bTs, args') = synT (bsymbs, args);
clasohm@0
   299
            val (Ts, args'') = synT (symbs, args');
clasohm@0
   300
          in (Pretty.blk (i, bTs) :: Ts, args'') end
clasohm@0
   301
      | synT (Break i :: symbs, args) =
wenzelm@18
   302
          let val (Ts, args') = synT (symbs, args);
wenzelm@18
   303
          in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
wenzelm@237
   304
      | synT (_ :: _, []) = sys_error "synT"
clasohm@0
   305
wenzelm@554
   306
    and parT (pr, args, p, p': int) = #1 (synT
wenzelm@554
   307
          (if p > p' orelse
wenzelm@5691
   308
            (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
wenzelm@554
   309
            then [Block (1, String "(" :: pr @ [String ")"])]
wenzelm@554
   310
            else pr, args))
clasohm@0
   311
clasohm@0
   312
    and prefixT (_, a, [], _) = [Pretty.str a]
wenzelm@2384
   313
      | prefixT (c, _, args, p) =
wenzelm@5691
   314
          if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then
wenzelm@2507
   315
            error "Syntax insufficient for printing prefix applications!"
wenzelm@2384
   316
          else astT (appT (c, args), p)
clasohm@0
   317
wenzelm@18
   318
    and splitT 0 ([x], ys) = (x, ys)
wenzelm@5691
   319
      | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
wenzelm@18
   320
      | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
wenzelm@237
   321
      | splitT _ _ = sys_error "splitT"
wenzelm@18
   322
clasohm@0
   323
    and combT (tup as (c, a, args, p)) =
clasohm@0
   324
      let
clasohm@0
   325
        val nargs = length args;
wenzelm@18
   326
wenzelm@2701
   327
        (*find matching table entry, or print as prefix / postfix*)
wenzelm@2200
   328
        fun prnt [] = prefixT tup
wenzelm@2200
   329
          | prnt ((pr, n, p') :: prnps) =
wenzelm@2200
   330
              if nargs = n then parT (pr, args, p, p')
wenzelm@2200
   331
              else if nargs > n andalso not type_mode then
wenzelm@2200
   332
                astT (appT (splitT n ([c], args)), p)
wenzelm@2200
   333
              else prnt prnps;
wenzelm@2200
   334
      in
wenzelm@2701
   335
        (case token_trans a args of     (*try token translation function*)
wenzelm@2701
   336
          Some (s, len) => [Pretty.strlen s len]
wenzelm@5691
   337
        | None =>			(*try print translation functions*)
wenzelm@5691
   338
            astT (trans a (trf a) args, p) handle Match => prnt (get_fmts tabs a))
wenzelm@2200
   339
      end
wenzelm@2200
   340
wenzelm@5691
   341
    and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
wenzelm@5691
   342
      | astT (Ast.Variable x, _) = [Pretty.str x]
wenzelm@5691
   343
      | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) =
wenzelm@18
   344
          combT (c, a, args, p)
wenzelm@5691
   345
      | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
wenzelm@5691
   346
      | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
clasohm@0
   347
  in
clasohm@0
   348
    astT (ast0, p0)
clasohm@0
   349
  end;
clasohm@0
   350
clasohm@0
   351
clasohm@0
   352
(* pretty_term_ast *)
clasohm@0
   353
wenzelm@2701
   354
fun pretty_term_ast curried prtabs trf tokentrf ast =
wenzelm@2701
   355
  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
wenzelm@2701
   356
    trf tokentrf false curried ast 0);
clasohm@0
   357
clasohm@0
   358
clasohm@0
   359
(* pretty_typ_ast *)
clasohm@0
   360
wenzelm@2701
   361
fun pretty_typ_ast _ prtabs trf tokentrf ast =
wenzelm@2701
   362
  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
wenzelm@2701
   363
    trf tokentrf true false ast 0);
clasohm@0
   364
clasohm@0
   365
end;