src/Pure/Syntax/printer.ML
author wenzelm
Thu, 27 Mar 2008 17:35:56 +0100
changeset 26439 e38f7e1c07ce
parent 25393 0856e0141062
child 26707 ddf6bab64b96
permissions -rw-r--r--
tuned comments;
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
14176
716fec31f9ea Added show_all_types flag, such that all type information in the term
skalberg
parents: 12785
diff changeset
    14
  val show_all_types: bool ref
14837
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
    15
  val pp_show_brackets: Pretty.pp -> Pretty.pp
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    16
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
signature PRINTER =
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    19
sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  include PRINTER0
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    21
  val term_to_ast: Proof.context ->
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    22
    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    23
  val typ_to_ast: Proof.context ->
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    24
    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    25
  val sort_to_ast: Proof.context ->
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    26
    (string -> (Proof.context -> 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
    27
  type prtabs
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    28
  val empty_prtabs: prtabs
25393
0856e0141062 replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm
parents: 25386
diff changeset
    29
  val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
15753
eb014dfc57ee tuned extend_prtabs;
wenzelm
parents: 15574
diff changeset
    30
  val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    31
  val merge_prtabs: prtabs -> prtabs -> prtabs
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    32
  val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    33
    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23630
diff changeset
    34
    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    35
  val pretty_typ_ast: Proof.context -> bool -> prtabs
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    36
    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23630
diff changeset
    37
    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    38
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
2365
38295260a740 added chartrans_of;
wenzelm
parents: 2229
diff changeset
    40
structure Printer: PRINTER =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
struct
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    42
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    43
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(** options for printing **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val show_types = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val show_sorts = ref false;
504
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    48
val show_brackets = ref false;
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    49
val show_no_free_types = ref false;
14176
716fec31f9ea Added show_all_types flag, such that all type information in the term
skalberg
parents: 12785
diff changeset
    50
val show_all_types = ref false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
14975
2736b0984253 tuned pp;
wenzelm
parents: 14837
diff changeset
    52
fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
2736b0984253 tuned pp;
wenzelm
parents: 14837
diff changeset
    53
  Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
14837
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
    54
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
    55
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    57
(** misc utils **)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    58
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    59
(* apply print (ast) translation function *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
23937
66e1f24d655d eliminated transform_failure (to avoid critical section for main transactions);
wenzelm
parents: 23660
diff changeset
    61
fun apply_trans ctxt fns args =
16611
edb368e2878f proper treatment of advanced trfuns: pass thy argument;
wenzelm
parents: 15973
diff changeset
    62
  let
edb368e2878f proper treatment of advanced trfuns: pass thy argument;
wenzelm
parents: 15973
diff changeset
    63
    fun app_first [] = raise Match
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    64
      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
23937
66e1f24d655d eliminated transform_failure (to avoid critical section for main transactions);
wenzelm
parents: 23660
diff changeset
    65
  in app_first fns end;
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    66
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    67
fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
4147
e57d03a5fc73 print translation: added show_sorts argument;
wenzelm
parents: 3816
diff changeset
    68
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    70
(* simple_ast_of *)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    71
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    72
fun simple_ast_of (Const (c, _)) = Ast.Constant c
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    73
  | simple_ast_of (Free (x, _)) = Ast.Variable x
14783
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14696
diff changeset
    74
  | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    75
  | simple_ast_of (t as _ $ _) =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    76
      let val (f, args) = strip_comb t in
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    77
        Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    78
      end
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    79
  | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    80
  | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    81
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    82
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    83
3776
38f8ec304b95 added sort_to_ast;
wenzelm
parents: 2913
diff changeset
    84
(** sort_to_ast, typ_to_ast **)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    85
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
    86
fun ast_of_termT ctxt trf tm =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
  let
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    88
    fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    89
      | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    90
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    91
      | ast_of (Const (a, _)) = trans a []
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    92
      | ast_of (t as _ $ _) =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    93
          (case strip_comb t of
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    94
            (Const (a, _), args) => trans a args
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    95
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    96
      | ast_of t = simple_ast_of t
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    97
    and trans a args =
23937
66e1f24d655d eliminated transform_failure (to avoid critical section for main transactions);
wenzelm
parents: 23660
diff changeset
    98
      ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    99
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   100
  in ast_of tm end;
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
   101
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   102
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   103
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   104
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   105
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   106
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   107
(** term_to_ast **)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   108
11795
12a0fb3ac366 be more careful about token class markers;
wenzelm
parents: 9910
diff changeset
   109
fun mark_freevars ((t as Const (c, _)) $ u) =
18139
wenzelm
parents: 17412
diff changeset
   110
      if member (op =) SynExt.standard_token_markers c then (t $ u)
11795
12a0fb3ac366 be more careful about token class markers;
wenzelm
parents: 9910
diff changeset
   111
      else t $ mark_freevars u
12a0fb3ac366 be more careful about token class markers;
wenzelm
parents: 9910
diff changeset
   112
  | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   113
  | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   114
  | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
6767
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   115
  | mark_freevars (t as Var (xi, T)) =
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   116
      if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   117
      else Lexicon.const "_var" $ t
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   118
  | mark_freevars a = a;
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   119
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   120
fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   121
  let
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    fun prune_typs (t_seen as (Const _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
      | prune_typs (t as Free (x, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
          if ty = dummyT then (t, seen)
18139
wenzelm
parents: 17412
diff changeset
   125
          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
      | prune_typs (t as Var (xi, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
          if ty = dummyT then (t, seen)
18139
wenzelm
parents: 17412
diff changeset
   129
          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
      | prune_typs (t_seen as (Bound _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
      | prune_typs (Abs (x, ty, t), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
          let val (t', seen') = prune_typs (t, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
          in (Abs (x, ty, t'), seen') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
      | prune_typs (t1 $ t2, seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
            val (t1', seen') = prune_typs (t1, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
            val (t2', seen'') = prune_typs (t2, seen');
6767
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   139
          in (t1' $ t2', seen'') end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   141
    fun ast_of tm =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   142
      (case strip_comb tm of
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   143
        (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
   144
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   145
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
21748
7df0f4e08dde support printing of idtdummy;
wenzelm
parents: 19482
diff changeset
   146
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
7df0f4e08dde support printing of idtdummy;
wenzelm
parents: 19482
diff changeset
   147
          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
   148
      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   149
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
21748
7df0f4e08dde support printing of idtdummy;
wenzelm
parents: 19482
diff changeset
   150
      | (Const ("_idtdummy", T), ts) =>
7df0f4e08dde support printing of idtdummy;
wenzelm
parents: 19482
diff changeset
   151
          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
14176
716fec31f9ea Added show_all_types flag, such that all type information in the term
skalberg
parents: 12785
diff changeset
   152
      | (c' as Const (c, T), ts) =>
14696
wenzelm
parents: 14176
diff changeset
   153
          if show_all_types
wenzelm
parents: 14176
diff changeset
   154
          then Ast.mk_appl (constrain c' T) (map ast_of ts)
wenzelm
parents: 14176
diff changeset
   155
          else trans c T ts
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   156
      | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   158
    and trans a T args =
23937
66e1f24d655d eliminated transform_failure (to avoid critical section for main transactions);
wenzelm
parents: 23660
diff changeset
   159
      ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   160
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   162
    and constrain t T =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   163
      if show_types andalso T <> dummyT then
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   164
        Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   165
          ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   166
      else simple_ast_of t
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
  in
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   168
    tm
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   169
    |> SynTrans.prop_tr'
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   170
    |> (if show_types then #1 o prune_typs o rpair [] else I)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   171
    |> mark_freevars
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   172
    |> ast_of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   175
fun term_to_ast ctxt trf tm =
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   176
  ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
14696
wenzelm
parents: 14176
diff changeset
   177
    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   181
(** type prtabs **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
datatype symb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
  Arg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
  TypArg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
  String of string |
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   187
  Space of string |
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
  Break of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
  Block of int * symb list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   191
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
   192
18957
8c3abd63bce3 TableFun: renamed xxx_multi to xxx_list;
wenzelm
parents: 18857
diff changeset
   193
fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19374
diff changeset
   194
fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   195
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   196
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   197
(* xprod_to_fmt *)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   198
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   199
fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   200
  | 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
   201
      let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   202
        fun arg (s, p) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   203
          (if s = "type" then TypArg else Arg)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   204
          (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
   205
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   206
        fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   207
              apfst (cons (String s)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   208
          | 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
   209
              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   210
          | xsyms_to_syms (SynExt.Space s :: xsyms) =
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   211
              apfst (cons (Space s)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   212
          | xsyms_to_syms (SynExt.Bg i :: xsyms) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   213
              let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   214
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   215
                val (syms, xsyms'') = xsyms_to_syms xsyms';
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   216
              in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   217
                (Block (i, bsyms) :: syms, xsyms'')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   218
              end
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   219
          | xsyms_to_syms (SynExt.Brk i :: xsyms) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   220
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   221
          | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   222
          | xsyms_to_syms [] = ([], []);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   223
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   224
        fun nargs (Arg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   225
          | nargs (TypArg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   226
          | nargs (String _ :: syms) = nargs syms
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   227
          | nargs (Space _ :: syms) = nargs syms
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   228
          | nargs (Break _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   229
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   230
          | nargs [] = 0;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   231
      in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   232
        (case xsyms_to_syms xsymbs of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   233
          (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   234
        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   235
      end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   236
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   238
(* empty, extend, merge prtabs *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   239
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   240
val empty_prtabs = [];
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   241
25393
0856e0141062 replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm
parents: 25386
diff changeset
   242
fun update_prtabs mode xprods prtabs =
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   243
  let
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19374
diff changeset
   244
    val fmts = map_filter xprod_to_fmt xprods;
25393
0856e0141062 replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm
parents: 25386
diff changeset
   245
    val tab' = fold (Symtab.update_list (op =)) fmts (mode_tab prtabs mode);
25386
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   246
  in AList.update (op =) (mode, tab') prtabs end;
15753
eb014dfc57ee tuned extend_prtabs;
wenzelm
parents: 15574
diff changeset
   247
25386
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   248
fun remove_prtabs mode xprods prtabs =
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   249
  let
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   250
    val tab = mode_tab prtabs mode;
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   251
    val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   252
      if null (Symtab.lookup_list tab c) then NONE
82b62fe11d7a remove_prtabs: tuned, avoid excessive garbage;
wenzelm
parents: 24612
diff changeset
   253
      else xprod_to_fmt xprod) xprods;
25393
0856e0141062 replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm
parents: 25386
diff changeset
   254
    val tab' = fold (Symtab.remove_list (op =)) fmts tab;
0856e0141062 replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm
parents: 25386
diff changeset
   255
  in AList.update (op =) (mode, tab') prtabs end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   257
fun merge_prtabs prtabs1 prtabs2 =
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   258
  let
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 18977
diff changeset
   259
    val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
18957
8c3abd63bce3 TableFun: renamed xxx_multi to xxx_list;
wenzelm
parents: 18857
diff changeset
   260
    fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
12292
c4090cc2aa15 Symtab.merge_multi';
wenzelm
parents: 12252
diff changeset
   261
  in map merge modes end;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   262
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   265
(** pretty term or typ asts **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   267
fun is_chain [Block (_, pr)] = is_chain pr
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   268
  | is_chain [Arg _] = true
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   269
  | is_chain _  = false;
506
e0ca460d6e51 improved show_brackets again - Trueprop does not create () any more.
nipkow
parents: 505
diff changeset
   270
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   271
fun const_markup c = Pretty.markup (Markup.const c) o single;
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   272
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   273
fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
  let
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   275
    fun token_trans c [Ast.Variable x] =
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   276
          (case tokentrf c of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   277
            NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   278
          | SOME f => SOME (f x))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   279
      | token_trans _ _ = NONE;
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   280
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   281
    (*default applications: prefix / postfix*)
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   282
    val appT =
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   283
      if type_mode then TypeExt.tappl_ast_tr'
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   284
      else if curried then SynTrans.applC_ast_tr'
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   285
      else SynTrans.appl_ast_tr';
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   286
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   287
    fun synT _ ([], args) = ([], args)
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   288
      | synT markup (Arg p :: symbs, t :: args) =
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   289
          let val (Ts, args') = synT markup (symbs, args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
          in (astT (t, p) @ Ts, args') end
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   291
      | synT markup (TypArg p :: symbs, t :: args) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   292
          let
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   293
            val (Ts, args') = synT markup (symbs, args);
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   294
          in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   295
            if type_mode then (astT (t, p) @ Ts, args')
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   296
            else (pretty I ctxt 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
   297
          end
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   298
      | synT markup (String s :: symbs, args) =
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   299
          let val (Ts, args') = synT markup (symbs, args);
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   300
          in (markup (Pretty.str s) :: Ts, args') end
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   301
      | synT markup (Space s :: symbs, args) =
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   302
          let val (Ts, args') = synT markup (symbs, args);
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   303
          in (Pretty.str s :: Ts, args') end
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   304
      | synT markup (Block (i, bsymbs) :: symbs, args) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
          let
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   306
            val (bTs, args') = synT markup (bsymbs, args);
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   307
            val (Ts, args'') = synT markup (symbs, args');
14837
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   308
            val T =
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   309
              if i < 0 then Pretty.unbreakable (Pretty.block bTs)
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   310
              else Pretty.blk (i, bTs);
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   311
          in (T :: Ts, args'') end
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   312
      | synT markup (Break i :: symbs, args) =
14837
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   313
          let
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   314
            val (Ts, args') = synT markup (symbs, args);
14837
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   315
            val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
827c68f8267c added pp_show_brackets; support unbreakable blocks;
wenzelm
parents: 14783
diff changeset
   316
          in (T :: Ts, args') end
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   317
      | synT _ (_ :: _, []) = sys_error "synT"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   319
    and parT markup (pr, args, p, p': int) = #1 (synT markup
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   320
          (if p > p' orelse
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   321
            (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   322
            then [Block (1, Space "(" :: pr @ [Space ")"])]
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   323
            else pr, args))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
19374
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   325
    and atomT a =
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   326
      (case try (unprefix Lexicon.constN) a of
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   327
        SOME c => const_markup c (Pretty.str (extern_const c))
19374
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   328
      | NONE =>
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   329
          (case try (unprefix Lexicon.fixedN) a of
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   330
            SOME x =>
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   331
              (case tokentrf "_free" of
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   332
                SOME f => Pretty.raw_str (f x)
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   333
              | NONE => Pretty.str x)
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   334
          | NONE => Pretty.str a))
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   335
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   336
    and prefixT (_, a, [], _) = [atomT a]
16611
edb368e2878f proper treatment of advanced trfuns: pass thy argument;
wenzelm
parents: 15973
diff changeset
   337
      | prefixT (c, _, args, p) = astT (appT (c, args), p)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   339
    and splitT 0 ([x], ys) = (x, ys)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   340
      | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   341
      | 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
   342
      | splitT _ _ = sys_error "splitT"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   343
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
    and combT (tup as (c, a, args, p)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
        val nargs = length args;
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   347
        val markup = const_markup (unprefix Lexicon.constN a)
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   348
          handle Fail _ => I;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   349
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   350
        (*find matching table entry, or print as prefix / postfix*)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   351
        fun prnt ([], []) = prefixT tup
18957
8c3abd63bce3 TableFun: renamed xxx_multi to xxx_list;
wenzelm
parents: 18857
diff changeset
   352
          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   353
          | prnt ((pr, n, p') :: prnps, tbs) =
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   354
              if nargs = n then parT markup (pr, args, p, p')
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   355
              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
   356
                astT (appT (splitT n ([c], args)), p)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   357
              else prnt (prnps, tbs);
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   358
      in
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   359
        (case token_trans a args of     (*try token translation function*)
19374
ae4a225e0c1f pretty: late externing of consts (support authentic syntax);
wenzelm
parents: 19046
diff changeset
   360
          SOME s => [Pretty.raw_str s]
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   361
        | NONE =>                       (*try print translation functions*)
23937
66e1f24d655d eliminated transform_failure (to avoid critical section for main transactions);
wenzelm
parents: 23660
diff changeset
   362
            astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   363
      end
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   364
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   365
    and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   366
      | astT (Ast.Variable x, _) = [Pretty.str x]
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   367
      | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   368
      | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   369
      | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   370
  in astT (ast0, p0) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
(* pretty_term_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   375
fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 23937
diff changeset
   376
  pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   377
    trf tokentrf false curried ast 0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
(* pretty_typ_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 21748
diff changeset
   382
fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 23937
diff changeset
   383
  pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
23630
bc22daeed49e pretty: markup for syntax/name of authentic consts;
wenzelm
parents: 23615
diff changeset
   384
    trf tokentrf true false ast 0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
end;