src/Pure/Syntax/printer.ML
author wenzelm
Sat Oct 17 15:57:51 2009 +0200 (2009-10-17)
changeset 32966 5b21661fe618
parent 32738 15bb09ca0378
child 35262 9ea4445d2ccf
permissions -rw-r--r--
indicate CRITICAL nature of various setmp combinators;
     1 (*  Title:      Pure/Syntax/printer.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Pretty printing of asts, terms, types and print (ast) translation.
     5 *)
     6 
     7 signature PRINTER0 =
     8 sig
     9   val show_brackets: bool Unsynchronized.ref
    10   val show_sorts: bool Unsynchronized.ref
    11   val show_types: bool Unsynchronized.ref
    12   val show_no_free_types: bool Unsynchronized.ref
    13   val show_all_types: bool Unsynchronized.ref
    14   val pp_show_brackets: Pretty.pp -> Pretty.pp
    15 end;
    16 
    17 signature PRINTER =
    18 sig
    19   include PRINTER0
    20   val term_to_ast: Proof.context ->
    21     (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    22   val typ_to_ast: Proof.context ->
    23     (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    24   val sort_to_ast: Proof.context ->
    25     (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    26   type prtabs
    27   val empty_prtabs: prtabs
    28   val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    29   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    30   val merge_prtabs: prtabs -> prtabs -> prtabs
    31   val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
    32     -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    33     -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    34   val pretty_typ_ast: Proof.context -> bool -> prtabs
    35     -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    36     -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    37 end;
    38 
    39 structure Printer: PRINTER =
    40 struct
    41 
    42 
    43 (** options for printing **)
    44 
    45 val show_types = Unsynchronized.ref false;
    46 val show_sorts = Unsynchronized.ref false;
    47 val show_brackets = Unsynchronized.ref false;
    48 val show_no_free_types = Unsynchronized.ref false;
    49 val show_all_types = Unsynchronized.ref false;
    50 
    51 fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
    52   Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
    53 
    54 
    55 
    56 (** misc utils **)
    57 
    58 (* apply print (ast) translation function *)
    59 
    60 fun apply_trans ctxt fns args =
    61   let
    62     fun app_first [] = raise Match
    63       | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
    64   in app_first fns end;
    65 
    66 fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
    67 
    68 
    69 (* simple_ast_of *)
    70 
    71 fun simple_ast_of (Const (c, _)) = Ast.Constant c
    72   | simple_ast_of (Free (x, _)) = Ast.Variable x
    73   | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
    74   | simple_ast_of (t as _ $ _) =
    75       let val (f, args) = strip_comb t in
    76         Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
    77       end
    78   | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
    79   | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
    80 
    81 
    82 
    83 (** sort_to_ast, typ_to_ast **)
    84 
    85 fun ast_of_termT ctxt trf tm =
    86   let
    87     fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
    88       | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    89       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
    90       | ast_of (Const (a, _)) = trans a []
    91       | ast_of (t as _ $ _) =
    92           (case strip_comb t of
    93             (Const (a, _), args) => trans a args
    94           | (f, args) => Ast.Appl (map ast_of (f :: args)))
    95       | ast_of t = simple_ast_of t
    96     and trans a args =
    97       ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
    98         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    99   in ast_of tm end;
   100 
   101 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
   102 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
   103 
   104 
   105 
   106 (** term_to_ast **)
   107 
   108 fun mark_freevars ((t as Const (c, _)) $ u) =
   109       if member (op =) SynExt.standard_token_markers c then (t $ u)
   110       else t $ mark_freevars u
   111   | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
   112   | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
   113   | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
   114   | mark_freevars (t as Var (xi, T)) =
   115       if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
   116       else Lexicon.const "_var" $ t
   117   | mark_freevars a = a;
   118 
   119 fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
   120   let
   121     fun prune_typs (t_seen as (Const _, _)) = t_seen
   122       | prune_typs (t as Free (x, ty), seen) =
   123           if ty = dummyT then (t, seen)
   124           else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
   125           else (t, t :: seen)
   126       | prune_typs (t as Var (xi, ty), seen) =
   127           if ty = dummyT then (t, seen)
   128           else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
   129           else (t, t :: seen)
   130       | prune_typs (t_seen as (Bound _, _)) = t_seen
   131       | prune_typs (Abs (x, ty, t), seen) =
   132           let val (t', seen') = prune_typs (t, seen);
   133           in (Abs (x, ty, t'), seen') end
   134       | prune_typs (t1 $ t2, seen) =
   135           let
   136             val (t1', seen') = prune_typs (t1, seen);
   137             val (t2', seen'') = prune_typs (t2, seen');
   138           in (t1' $ t2', seen'') end;
   139 
   140     fun ast_of tm =
   141       (case strip_comb tm of
   142         (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
   143       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   144           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   145       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   146           Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
   147       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
   148           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   149       | (Const ("_idtdummy", T), ts) =>
   150           Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
   151       | (c' as Const (c, T), ts) =>
   152           if show_all_types
   153           then Ast.mk_appl (constrain c' T) (map ast_of ts)
   154           else trans c T ts
   155       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
   156 
   157     and trans a T args =
   158       ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
   159         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
   160 
   161     and constrain t T =
   162       if show_types andalso T <> dummyT then
   163         Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
   164           ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
   165       else simple_ast_of t
   166   in
   167     tm
   168     |> SynTrans.prop_tr'
   169     |> (if show_types then #1 o prune_typs o rpair [] else I)
   170     |> mark_freevars
   171     |> ast_of
   172   end;
   173 
   174 fun term_to_ast ctxt trf tm =
   175   ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
   176     (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
   177 
   178 
   179 
   180 (** type prtabs **)
   181 
   182 datatype symb =
   183   Arg of int |
   184   TypArg of int |
   185   String of string |
   186   Space of string |
   187   Break of int |
   188   Block of int * symb list;
   189 
   190 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
   191 
   192 fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
   193 fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
   194 
   195 
   196 (* xprod_to_fmt *)
   197 
   198 fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
   199   | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
   200       let
   201         fun arg (s, p) =
   202           (if s = "type" then TypArg else Arg)
   203           (if Lexicon.is_terminal s then SynExt.max_pri else p);
   204 
   205         fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
   206               apfst (cons (String s)) (xsyms_to_syms xsyms)
   207           | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
   208               apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
   209           | xsyms_to_syms (SynExt.Space s :: xsyms) =
   210               apfst (cons (Space s)) (xsyms_to_syms xsyms)
   211           | xsyms_to_syms (SynExt.Bg i :: xsyms) =
   212               let
   213                 val (bsyms, xsyms') = xsyms_to_syms xsyms;
   214                 val (syms, xsyms'') = xsyms_to_syms xsyms';
   215               in
   216                 (Block (i, bsyms) :: syms, xsyms'')
   217               end
   218           | xsyms_to_syms (SynExt.Brk i :: xsyms) =
   219               apfst (cons (Break i)) (xsyms_to_syms xsyms)
   220           | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
   221           | xsyms_to_syms [] = ([], []);
   222 
   223         fun nargs (Arg _ :: syms) = nargs syms + 1
   224           | nargs (TypArg _ :: syms) = nargs syms + 1
   225           | nargs (String _ :: syms) = nargs syms
   226           | nargs (Space _ :: syms) = nargs syms
   227           | nargs (Break _ :: syms) = nargs syms
   228           | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
   229           | nargs [] = 0;
   230       in
   231         (case xsyms_to_syms xsymbs of
   232           (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
   233         | _ => sys_error "xprod_to_fmt: unbalanced blocks")
   234       end;
   235 
   236 
   237 (* empty, extend, merge prtabs *)
   238 
   239 val empty_prtabs = [];
   240 
   241 fun update_prtabs mode xprods prtabs =
   242   let
   243     val fmts = map_filter xprod_to_fmt xprods;
   244     val tab' = fold (Symtab.update_list (op =)) fmts (mode_tab prtabs mode);
   245   in AList.update (op =) (mode, tab') prtabs end;
   246 
   247 fun remove_prtabs mode xprods prtabs =
   248   let
   249     val tab = mode_tab prtabs mode;
   250     val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
   251       if null (Symtab.lookup_list tab c) then NONE
   252       else xprod_to_fmt xprod) xprods;
   253     val tab' = fold (Symtab.remove_list (op =)) fmts tab;
   254   in AList.update (op =) (mode, tab') prtabs end;
   255 
   256 fun merge_prtabs prtabs1 prtabs2 =
   257   let
   258     val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
   259     fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   260   in map merge modes end;
   261 
   262 
   263 
   264 (** pretty term or typ asts **)
   265 
   266 fun is_chain [Block (_, pr)] = is_chain pr
   267   | is_chain [Arg _] = true
   268   | is_chain _  = false;
   269 
   270 fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   271   let
   272     fun token_trans a x =
   273       (case tokentrf a of
   274         NONE =>
   275           if member (op =) SynExt.standard_token_classes a
   276           then SOME (Pretty.str x) else NONE
   277       | SOME f => SOME (f ctxt x));
   278 
   279     (*default applications: prefix / postfix*)
   280     val appT =
   281       if type_mode then TypeExt.tappl_ast_tr'
   282       else if curried then SynTrans.applC_ast_tr'
   283       else SynTrans.appl_ast_tr';
   284 
   285     fun synT _ ([], args) = ([], args)
   286       | synT markup (Arg p :: symbs, t :: args) =
   287           let val (Ts, args') = synT markup (symbs, args);
   288           in (astT (t, p) @ Ts, args') end
   289       | synT markup (TypArg p :: symbs, t :: args) =
   290           let
   291             val (Ts, args') = synT markup (symbs, args);
   292           in
   293             if type_mode then (astT (t, p) @ Ts, args')
   294             else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
   295           end
   296       | synT markup (String s :: symbs, args) =
   297           let val (Ts, args') = synT markup (symbs, args);
   298           in (markup (Pretty.str s) :: Ts, args') end
   299       | synT markup (Space s :: symbs, args) =
   300           let val (Ts, args') = synT markup (symbs, args);
   301           in (Pretty.str s :: Ts, args') end
   302       | synT markup (Block (i, bsymbs) :: symbs, args) =
   303           let
   304             val (bTs, args') = synT markup (bsymbs, args);
   305             val (Ts, args'') = synT markup (symbs, args');
   306             val T =
   307               if i < 0 then Pretty.unbreakable (Pretty.block bTs)
   308               else Pretty.blk (i, bTs);
   309           in (T :: Ts, args'') end
   310       | synT markup (Break i :: symbs, args) =
   311           let
   312             val (Ts, args') = synT markup (symbs, args);
   313             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
   314           in (T :: Ts, args') end
   315       | synT _ (_ :: _, []) = sys_error "synT"
   316 
   317     and parT markup (pr, args, p, p': int) = #1 (synT markup
   318           (if p > p' orelse
   319             (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
   320             then [Block (1, Space "(" :: pr @ [Space ")"])]
   321             else pr, args))
   322 
   323     and atomT a =
   324       (case try (unprefix Lexicon.constN) a of
   325         SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
   326       | NONE =>
   327           (case try (unprefix Lexicon.fixedN) a of
   328             SOME x => the (token_trans "_free" x)
   329           | NONE => Pretty.str a))
   330 
   331     and prefixT (_, a, [], _) = [atomT a]
   332       | prefixT (c, _, args, p) = astT (appT (c, args), p)
   333 
   334     and splitT 0 ([x], ys) = (x, ys)
   335       | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
   336       | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
   337       | splitT _ _ = sys_error "splitT"
   338 
   339     and combT (tup as (c, a, args, p)) =
   340       let
   341         val nargs = length args;
   342         val markup = Pretty.mark
   343           (Markup.const (unprefix Lexicon.constN a) handle Fail _ =>
   344             (Markup.fixed (unprefix Lexicon.fixedN a)))
   345           handle Fail _ => I;
   346 
   347         (*find matching table entry, or print as prefix / postfix*)
   348         fun prnt ([], []) = prefixT tup
   349           | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
   350           | prnt ((pr, n, p') :: prnps, tbs) =
   351               if nargs = n then parT markup (pr, args, p, p')
   352               else if nargs > n andalso not type_mode then
   353                 astT (appT (splitT n ([c], args)), p)
   354               else prnt (prnps, tbs);
   355       in
   356         (case tokentrT a args of
   357           SOME prt => [prt]
   358         | NONE => astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
   359       end
   360 
   361     and tokentrT a [Ast.Variable x] = token_trans a x
   362       | tokentrT _ _ = NONE
   363 
   364     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
   365       | astT (Ast.Variable x, _) = [Pretty.str x]
   366       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
   367       | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
   368       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
   369   in astT (ast0, p0) end;
   370 
   371 
   372 (* pretty_term_ast *)
   373 
   374 fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
   375   pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
   376     trf tokentrf false curried ast 0;
   377 
   378 
   379 (* pretty_typ_ast *)
   380 
   381 fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
   382   pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
   383     trf tokentrf true false ast 0;
   384 
   385 end;