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