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