moved unparse material to syntax_phases.ML;
authorwenzelm
Wed Apr 06 12:58:13 2011 +0200 (2011-04-06)
changeset 4224529e3967550d5
parent 42244 15bba1fb39d1
child 42246 8f798ba04393
moved unparse material to syntax_phases.ML;
src/HOL/Groups.thy
src/HOL/Library/Cardinality.thy
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/record.ML
src/HOL/Typerep.thy
src/HOL/ex/Numeral.thy
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/type_ext.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Groups.thy	Wed Apr 06 12:55:53 2011 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed Apr 06 12:58:13 2011 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4      if not (null ts) orelse T = dummyT
     1.5        orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
     1.6      then raise Match
     1.7 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
     1.8 +    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T);
     1.9  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.10  *} -- {* show types that are presumably too general *}
    1.11  
     2.1 --- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:55:53 2011 +0200
     2.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:58:13 2011 +0200
     2.3 @@ -37,7 +37,7 @@
     2.4  typed_print_translation {*
     2.5  let
     2.6    fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
     2.7 -    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
     2.8 +    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
     2.9  in [(@{const_syntax card}, card_univ_tr')]
    2.10  end
    2.11  *}
     3.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 12:55:53 2011 +0200
     3.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 12:58:13 2011 +0200
     3.3 @@ -72,7 +72,9 @@
     3.4  fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
     3.5        let val t' =
     3.6          if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
     3.7 -        else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
     3.8 +        else
     3.9 +          Syntax.const Syntax.constrainC $ syntax_numeral t $
    3.10 +            Syntax_Phases.term_of_typ show_sorts T
    3.11        in list_comb (t', ts) end
    3.12    | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
    3.13        if T = dummyT then list_comb (syntax_numeral t, ts)
     4.1 --- a/src/HOL/Tools/record.ML	Wed Apr 06 12:55:53 2011 +0200
     4.2 +++ b/src/HOL/Tools/record.ML	Wed Apr 06 12:58:13 2011 +0200
     4.3 @@ -708,7 +708,7 @@
     4.4  
     4.5                      val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
     4.6                        handle Type.TYPE_MATCH => err "type is no proper record (extension)";
     4.7 -                    val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
     4.8 +                    val term_of_typ = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
     4.9                      val alphas' =
    4.10                        map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
    4.11  
    4.12 @@ -819,7 +819,7 @@
    4.13      val T = decode_type thy t;
    4.14      val varifyT = varifyT (Term.maxidx_of_typ T);
    4.15  
    4.16 -    val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
    4.17 +    val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
    4.18  
    4.19      fun strip_fields T =
    4.20        (case T of
    4.21 @@ -865,7 +865,7 @@
    4.22  
    4.23      fun mk_type_abbr subst name args =
    4.24        let val abbrT = Type (name, map (varifyT o TFree) args)
    4.25 -      in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
    4.26 +      in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
    4.27  
    4.28      fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
    4.29    in
     5.1 --- a/src/HOL/Typerep.thy	Wed Apr 06 12:55:53 2011 +0200
     5.2 +++ b/src/HOL/Typerep.thy	Wed Apr 06 12:58:13 2011 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4            (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
     5.5            (Const (@{const_syntax TYPE}, _) :: ts) =
     5.6          Term.list_comb
     5.7 -          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
     5.8 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
     5.9      | typerep_tr' _ T ts = raise Match;
    5.10  in [(@{const_syntax typerep}, typerep_tr')] end
    5.11  *}
     6.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 06 12:55:53 2011 +0200
     6.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 12:58:13 2011 +0200
     6.3 @@ -309,7 +309,7 @@
     6.4        case T of
     6.5          Type (@{type_name fun}, [_, T']) =>
     6.6            if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
     6.7 -          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
     6.8 +          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ show_sorts T'
     6.9        | T' => if T' = dummyT then t' else raise Match
    6.10      end;
    6.11  in [(@{const_syntax of_num}, num_tr')] end
     7.1 --- a/src/Pure/Syntax/printer.ML	Wed Apr 06 12:55:53 2011 +0200
     7.2 +++ b/src/Pure/Syntax/printer.ML	Wed Apr 06 12:58:13 2011 +0200
     7.3 @@ -23,17 +23,12 @@
     7.4    val show_question_marks_raw: Config.raw
     7.5    val show_question_marks: bool Config.T
     7.6    val pretty_priority: int Config.T
     7.7 +  val apply_trans: 'a -> ('a -> 'b -> 'c) list -> 'b -> 'c
     7.8  end;
     7.9  
    7.10  signature PRINTER =
    7.11  sig
    7.12    include PRINTER0
    7.13 -  val sort_to_ast: Proof.context ->
    7.14 -    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    7.15 -  val typ_to_ast: Proof.context ->
    7.16 -    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    7.17 -  val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
    7.18 -    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    7.19    type prtabs
    7.20    val empty_prtabs: prtabs
    7.21    val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
    7.22 @@ -52,7 +47,6 @@
    7.23  structure Printer: PRINTER =
    7.24  struct
    7.25  
    7.26 -
    7.27  (** options for printing **)
    7.28  
    7.29  val show_brackets_default = Unsynchronized.ref false;
    7.30 @@ -81,150 +75,6 @@
    7.31  
    7.32  
    7.33  
    7.34 -(** misc utils **)
    7.35 -
    7.36 -(* apply print (ast) translation function *)
    7.37 -
    7.38 -fun apply_trans ctxt fns args =
    7.39 -  let
    7.40 -    fun app_first [] = raise Match
    7.41 -      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
    7.42 -  in app_first fns end;
    7.43 -
    7.44 -fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
    7.45 -
    7.46 -
    7.47 -(* simple_ast_of *)
    7.48 -
    7.49 -fun simple_ast_of ctxt =
    7.50 -  let
    7.51 -    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
    7.52 -    fun ast_of (Const (c, _)) = Ast.Constant c
    7.53 -      | ast_of (Free (x, _)) = Ast.Variable x
    7.54 -      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
    7.55 -      | ast_of (t as _ $ _) =
    7.56 -          let val (f, args) = strip_comb t
    7.57 -          in Ast.mk_appl (ast_of f) (map ast_of args) end
    7.58 -      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
    7.59 -      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
    7.60 -  in ast_of end;
    7.61 -
    7.62 -
    7.63 -
    7.64 -(** sort_to_ast, typ_to_ast **)
    7.65 -
    7.66 -fun ast_of_termT ctxt trf tm =
    7.67 -  let
    7.68 -    val ctxt' = Config.put show_sorts false ctxt;
    7.69 -    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
    7.70 -      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
    7.71 -      | ast_of (Const (a, _)) = trans a []
    7.72 -      | ast_of (t as _ $ _) =
    7.73 -          (case strip_comb t of
    7.74 -            (Const (a, _), args) => trans a args
    7.75 -          | (f, args) => Ast.Appl (map ast_of (f :: args)))
    7.76 -      | ast_of t = simple_ast_of ctxt t
    7.77 -    and trans a args =
    7.78 -      ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
    7.79 -        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    7.80 -  in ast_of tm end;
    7.81 -
    7.82 -fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
    7.83 -fun typ_to_ast ctxt trf T =
    7.84 -  ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
    7.85 -
    7.86 -
    7.87 -
    7.88 -(** term_to_ast **)
    7.89 -
    7.90 -fun term_to_ast idents consts ctxt trf tm =
    7.91 -  let
    7.92 -    val show_types =
    7.93 -      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
    7.94 -      Config.get ctxt show_all_types;
    7.95 -    val show_sorts = Config.get ctxt show_sorts;
    7.96 -    val show_structs = Config.get ctxt show_structs;
    7.97 -    val show_free_types = Config.get ctxt show_free_types;
    7.98 -    val show_all_types = Config.get ctxt show_all_types;
    7.99 -
   7.100 -    val {structs, fixes} = idents;
   7.101 -
   7.102 -    fun mark_atoms ((t as Const (c, T)) $ u) =
   7.103 -          if member (op =) Syn_Ext.standard_token_markers c
   7.104 -          then t $ u else mark_atoms t $ mark_atoms u
   7.105 -      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   7.106 -      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   7.107 -      | mark_atoms (t as Const (c, T)) =
   7.108 -          if member (op =) consts c then t
   7.109 -          else Const (Lexicon.mark_const c, T)
   7.110 -      | mark_atoms (t as Free (x, T)) =
   7.111 -          let val i = find_index (fn s => s = x) structs + 1 in
   7.112 -            if i = 0 andalso member (op =) fixes x then
   7.113 -              Const (Lexicon.mark_fixed x, T)
   7.114 -            else if i = 1 andalso not show_structs then
   7.115 -              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
   7.116 -            else Lexicon.const "_free" $ t
   7.117 -          end
   7.118 -      | mark_atoms (t as Var (xi, T)) =
   7.119 -          if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
   7.120 -          else Lexicon.const "_var" $ t
   7.121 -      | mark_atoms a = a;
   7.122 -
   7.123 -    fun prune_typs (t_seen as (Const _, _)) = t_seen
   7.124 -      | prune_typs (t as Free (x, ty), seen) =
   7.125 -          if ty = dummyT then (t, seen)
   7.126 -          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
   7.127 -          else (t, t :: seen)
   7.128 -      | prune_typs (t as Var (xi, ty), seen) =
   7.129 -          if ty = dummyT then (t, seen)
   7.130 -          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
   7.131 -          else (t, t :: seen)
   7.132 -      | prune_typs (t_seen as (Bound _, _)) = t_seen
   7.133 -      | prune_typs (Abs (x, ty, t), seen) =
   7.134 -          let val (t', seen') = prune_typs (t, seen);
   7.135 -          in (Abs (x, ty, t'), seen') end
   7.136 -      | prune_typs (t1 $ t2, seen) =
   7.137 -          let
   7.138 -            val (t1', seen') = prune_typs (t1, seen);
   7.139 -            val (t2', seen'') = prune_typs (t2, seen');
   7.140 -          in (t1' $ t2', seen'') end;
   7.141 -
   7.142 -    fun ast_of tm =
   7.143 -      (case strip_comb tm of
   7.144 -        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
   7.145 -      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   7.146 -          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   7.147 -      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   7.148 -          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
   7.149 -      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
   7.150 -          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   7.151 -      | (Const ("_idtdummy", T), ts) =>
   7.152 -          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
   7.153 -      | (const as Const (c, T), ts) =>
   7.154 -          if show_all_types
   7.155 -          then Ast.mk_appl (constrain const T) (map ast_of ts)
   7.156 -          else trans c T ts
   7.157 -      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
   7.158 -
   7.159 -    and trans a T args =
   7.160 -      ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
   7.161 -        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
   7.162 -
   7.163 -    and constrain t T =
   7.164 -      if show_types andalso T <> dummyT then
   7.165 -        Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
   7.166 -          ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
   7.167 -      else simple_ast_of ctxt t;
   7.168 -  in
   7.169 -    tm
   7.170 -    |> Syn_Trans.prop_tr'
   7.171 -    |> show_types ? (#1 o prune_typs o rpair [])
   7.172 -    |> mark_atoms
   7.173 -    |> ast_of
   7.174 -  end;
   7.175 -
   7.176 -
   7.177 -
   7.178  (** type prtabs **)
   7.179  
   7.180  datatype symb =
   7.181 @@ -311,6 +161,12 @@
   7.182  
   7.183  (** pretty term or typ asts **)
   7.184  
   7.185 +fun apply_trans ctxt fns args =
   7.186 +  let
   7.187 +    fun app_first [] = raise Match
   7.188 +      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   7.189 +  in app_first fns end;
   7.190 +
   7.191  fun is_chain [Block (_, pr)] = is_chain pr
   7.192    | is_chain [Arg _] = true
   7.193    | is_chain _  = false;
     8.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 12:55:53 2011 +0200
     8.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 12:58:13 2011 +0200
     8.3 @@ -20,6 +20,7 @@
     8.4      string -> (string * (Proof.context -> string -> Pretty.T)) list ->
     8.5      (string * string * (Proof.context -> string -> Pretty.T)) list
     8.6    val standard_token_classes: string list
     8.7 +  val standard_token_markers: string list
     8.8  end;
     8.9  
    8.10  signature SYN_EXT =
    8.11 @@ -83,7 +84,6 @@
    8.12      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    8.13      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    8.14    val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
    8.15 -  val standard_token_markers: string list
    8.16    val pure_ext: syn_ext
    8.17  end;
    8.18  
     9.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 12:55:53 2011 +0200
     9.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 12:58:13 2011 +0200
     9.3 @@ -42,7 +42,6 @@
     9.4      (string * (term list -> term)) list *
     9.5      (string * (term list -> term)) list *
     9.6      (string * (Ast.ast list -> Ast.ast)) list
     9.7 -  val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
     9.8    val struct_trfuns: string list ->
     9.9      (string * (Ast.ast list -> Ast.ast)) list *
    9.10      (string * (term list -> term)) list *
    9.11 @@ -354,15 +353,6 @@
    9.12    | idtyp_ast_tr' _ _ = raise Match;
    9.13  
    9.14  
    9.15 -(* type propositions *)
    9.16 -
    9.17 -fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
    9.18 -      Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
    9.19 -  | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
    9.20 -      Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
    9.21 -  | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
    9.22 -
    9.23 -
    9.24  (* meta propositions *)
    9.25  
    9.26  fun prop_tr' tm =
    9.27 @@ -408,20 +398,6 @@
    9.28      | _ => raise Match);
    9.29  
    9.30  
    9.31 -(* type reflection *)
    9.32 -
    9.33 -fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
    9.34 -      Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
    9.35 -  | type_tr' _ _ _ = raise Match;
    9.36 -
    9.37 -
    9.38 -(* type constraints *)
    9.39 -
    9.40 -fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
    9.41 -      Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
    9.42 -  | type_constraint_tr' _ _ _ = raise Match;
    9.43 -
    9.44 -
    9.45  (* dependent / nondependent quantifiers *)
    9.46  
    9.47  fun var_abs mark (x, T, b) =
    9.48 @@ -533,11 +509,6 @@
    9.49      ("\\<^const>==>", impl_ast_tr'),
    9.50      ("_index", index_ast_tr')]);
    9.51  
    9.52 -val pure_trfunsT =
    9.53 - [("_type_prop", type_prop_tr'),
    9.54 -  ("\\<^const>TYPE", type_tr'),
    9.55 -  ("_type_constraint_", type_constraint_tr')];
    9.56 -
    9.57  fun struct_trfuns structs =
    9.58    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
    9.59  
    10.1 --- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 12:55:53 2011 +0200
    10.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 12:58:13 2011 +0200
    10.3 @@ -95,6 +95,9 @@
    10.4    val string_of_sort_global: theory -> sort -> string
    10.5    val pp: Proof.context -> Pretty.pp
    10.6    val pp_global: theory -> Pretty.pp
    10.7 +  val lookup_tokentr:
    10.8 +    (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list ->
    10.9 +      string list -> string -> (Proof.context -> string -> Pretty.T) option
   10.10    type ruletab
   10.11    type syntax
   10.12    val rep_syntax: syntax ->
   10.13 @@ -135,13 +138,6 @@
   10.14      Parse_Print_Rule of 'a * 'a
   10.15    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   10.16    val is_const: syntax -> string -> bool
   10.17 -  val standard_unparse_sort: {extern_class: string -> xstring} ->
   10.18 -    Proof.context -> syntax -> sort -> Pretty.T
   10.19 -  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
   10.20 -    Proof.context -> syntax -> typ -> Pretty.T
   10.21 -  val standard_unparse_term: {structs: string list, fixes: string list} ->
   10.22 -    {extern_class: string -> xstring, extern_type: string -> xstring,
   10.23 -      extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   10.24    val update_trfuns:
   10.25      (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   10.26      (string * ((term list -> term) * stamp)) list *
   10.27 @@ -415,7 +411,6 @@
   10.28  
   10.29  (* print (ast) translations *)
   10.30  
   10.31 -fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
   10.32  fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
   10.33  fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
   10.34  fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
   10.35 @@ -425,12 +420,14 @@
   10.36  (** tables of token translation functions **)
   10.37  
   10.38  fun lookup_tokentr tabs modes =
   10.39 -  let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   10.40 +  let val trs =
   10.41 +    distinct (eq_fst (op = : string * string -> bool))
   10.42 +      (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   10.43    in fn c => Option.map fst (AList.lookup (op =) trs c) end;
   10.44  
   10.45  fun merge_tokentrtabs tabs1 tabs2 =
   10.46    let
   10.47 -    fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
   10.48 +    fun eq_tr ((c1, (_, s1: stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
   10.49  
   10.50      fun name (s, _) = implode (tl (Symbol.explode s));
   10.51  
   10.52 @@ -754,37 +751,6 @@
   10.53  
   10.54  
   10.55  
   10.56 -(** unparse terms, typs, sorts **)
   10.57 -
   10.58 -local
   10.59 -
   10.60 -fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   10.61 -  let
   10.62 -    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   10.63 -    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
   10.64 -  in
   10.65 -    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
   10.66 -      (lookup_tokentr tokentrtab (print_mode_value ()))
   10.67 -      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
   10.68 -  end;
   10.69 -
   10.70 -in
   10.71 -
   10.72 -fun standard_unparse_sort {extern_class} ctxt syn =
   10.73 -  unparse_t (K Printer.sort_to_ast)
   10.74 -    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
   10.75 -    Markup.sort ctxt syn false;
   10.76 -
   10.77 -fun standard_unparse_typ extern ctxt syn =
   10.78 -  unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
   10.79 -
   10.80 -fun standard_unparse_term idents extern =
   10.81 -  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
   10.82 -
   10.83 -end;
   10.84 -
   10.85 -
   10.86 -
   10.87  (** modify syntax **)
   10.88  
   10.89  fun ext_syntax f decls = update_syntax mode_default (f decls);
   10.90 @@ -813,6 +779,5 @@
   10.91  
   10.92  forget_structure "Syn_Ext";
   10.93  forget_structure "Type_Ext";
   10.94 -forget_structure "Syn_Trans";
   10.95  forget_structure "Mixfix";
   10.96 -forget_structure "Printer";
   10.97 +
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 12:55:53 2011 +0200
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 12:58:13 2011 +0200
    11.3 @@ -12,6 +12,7 @@
    11.4    val decode_term: Proof.context ->
    11.5      Position.reports * term Exn.result -> Position.reports * term Exn.result
    11.6    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    11.7 +  val term_of_typ: bool -> typ -> term
    11.8  end
    11.9  
   11.10  structure Syntax_Phases: SYNTAX_PHASES =
   11.11 @@ -390,17 +391,214 @@
   11.12  
   11.13  
   11.14  
   11.15 +(** encode parse trees **)
   11.16 +
   11.17 +(* term_of_sort *)
   11.18 +
   11.19 +fun term_of_sort S =
   11.20 +  let
   11.21 +    val class = Lexicon.const o Lexicon.mark_class;
   11.22 +
   11.23 +    fun classes [c] = class c
   11.24 +      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   11.25 +  in
   11.26 +    (case S of
   11.27 +      [] => Lexicon.const "_topsort"
   11.28 +    | [c] => class c
   11.29 +    | cs => Lexicon.const "_sort" $ classes cs)
   11.30 +  end;
   11.31 +
   11.32 +
   11.33 +(* term_of_typ *)
   11.34 +
   11.35 +fun term_of_typ show_sorts ty =
   11.36 +  let
   11.37 +    fun of_sort t S =
   11.38 +      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   11.39 +      else t;
   11.40 +
   11.41 +    fun term_of (Type (a, Ts)) =
   11.42 +          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
   11.43 +      | term_of (TFree (x, S)) =
   11.44 +          if is_some (Lexicon.decode_position x) then Lexicon.free x
   11.45 +          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   11.46 +      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   11.47 +  in term_of ty end;
   11.48 +
   11.49 +
   11.50 +(* simple_ast_of *)
   11.51 +
   11.52 +fun simple_ast_of ctxt =
   11.53 +  let
   11.54 +    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
   11.55 +    fun ast_of (Const (c, _)) = Ast.Constant c
   11.56 +      | ast_of (Free (x, _)) = Ast.Variable x
   11.57 +      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
   11.58 +      | ast_of (t as _ $ _) =
   11.59 +          let val (f, args) = strip_comb t
   11.60 +          in Ast.mk_appl (ast_of f) (map ast_of args) end
   11.61 +      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
   11.62 +      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   11.63 +  in ast_of end;
   11.64 +
   11.65 +
   11.66 +(* sort_to_ast and typ_to_ast *)
   11.67 +
   11.68 +fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
   11.69 +
   11.70 +fun ast_of_termT ctxt trf tm =
   11.71 +  let
   11.72 +    val ctxt' = Config.put show_sorts false ctxt;
   11.73 +    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
   11.74 +      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
   11.75 +      | ast_of (Const (a, _)) = trans a []
   11.76 +      | ast_of (t as _ $ _) =
   11.77 +          (case strip_comb t of
   11.78 +            (Const (a, _), args) => trans a args
   11.79 +          | (f, args) => Ast.Appl (map ast_of (f :: args)))
   11.80 +      | ast_of t = simple_ast_of ctxt t
   11.81 +    and trans a args =
   11.82 +      ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args)
   11.83 +        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   11.84 +  in ast_of tm end;
   11.85 +
   11.86 +fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
   11.87 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ (Config.get ctxt show_sorts) T);
   11.88 +
   11.89 +
   11.90 +(* term_to_ast *)
   11.91 +
   11.92 +fun term_to_ast idents consts ctxt trf tm =
   11.93 +  let
   11.94 +    val show_types =
   11.95 +      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
   11.96 +      Config.get ctxt show_all_types;
   11.97 +    val show_sorts = Config.get ctxt show_sorts;
   11.98 +    val show_structs = Config.get ctxt show_structs;
   11.99 +    val show_free_types = Config.get ctxt show_free_types;
  11.100 +    val show_all_types = Config.get ctxt show_all_types;
  11.101 +
  11.102 +    val {structs, fixes} = idents;
  11.103 +
  11.104 +    fun mark_atoms ((t as Const (c, T)) $ u) =
  11.105 +          if member (op =) Syntax.standard_token_markers c
  11.106 +          then t $ u else mark_atoms t $ mark_atoms u
  11.107 +      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
  11.108 +      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
  11.109 +      | mark_atoms (t as Const (c, T)) =
  11.110 +          if member (op =) consts c then t
  11.111 +          else Const (Lexicon.mark_const c, T)
  11.112 +      | mark_atoms (t as Free (x, T)) =
  11.113 +          let val i = find_index (fn s => s = x) structs + 1 in
  11.114 +            if i = 0 andalso member (op =) fixes x then
  11.115 +              Const (Lexicon.mark_fixed x, T)
  11.116 +            else if i = 1 andalso not show_structs then
  11.117 +              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
  11.118 +            else Lexicon.const "_free" $ t
  11.119 +          end
  11.120 +      | mark_atoms (t as Var (xi, T)) =
  11.121 +          if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
  11.122 +          else Lexicon.const "_var" $ t
  11.123 +      | mark_atoms a = a;
  11.124 +
  11.125 +    fun prune_typs (t_seen as (Const _, _)) = t_seen
  11.126 +      | prune_typs (t as Free (x, ty), seen) =
  11.127 +          if ty = dummyT then (t, seen)
  11.128 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
  11.129 +          else (t, t :: seen)
  11.130 +      | prune_typs (t as Var (xi, ty), seen) =
  11.131 +          if ty = dummyT then (t, seen)
  11.132 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
  11.133 +          else (t, t :: seen)
  11.134 +      | prune_typs (t_seen as (Bound _, _)) = t_seen
  11.135 +      | prune_typs (Abs (x, ty, t), seen) =
  11.136 +          let val (t', seen') = prune_typs (t, seen);
  11.137 +          in (Abs (x, ty, t'), seen') end
  11.138 +      | prune_typs (t1 $ t2, seen) =
  11.139 +          let
  11.140 +            val (t1', seen') = prune_typs (t1, seen);
  11.141 +            val (t2', seen'') = prune_typs (t2, seen');
  11.142 +          in (t1' $ t2', seen'') end;
  11.143 +
  11.144 +    fun ast_of tm =
  11.145 +      (case strip_comb tm of
  11.146 +        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
  11.147 +      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
  11.148 +          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
  11.149 +      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
  11.150 +          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
  11.151 +      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
  11.152 +          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
  11.153 +      | (Const ("_idtdummy", T), ts) =>
  11.154 +          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
  11.155 +      | (const as Const (c, T), ts) =>
  11.156 +          if show_all_types
  11.157 +          then Ast.mk_appl (constrain const T) (map ast_of ts)
  11.158 +          else trans c T ts
  11.159 +      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
  11.160 +
  11.161 +    and trans a T args =
  11.162 +      ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args)
  11.163 +        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
  11.164 +
  11.165 +    and constrain t T =
  11.166 +      if show_types andalso T <> dummyT then
  11.167 +        Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
  11.168 +          ast_of_termT ctxt trf (term_of_typ show_sorts T)]
  11.169 +      else simple_ast_of ctxt t;
  11.170 +  in
  11.171 +    tm
  11.172 +    |> Syn_Trans.prop_tr'
  11.173 +    |> show_types ? (#1 o prune_typs o rpair [])
  11.174 +    |> mark_atoms
  11.175 +    |> ast_of
  11.176 +  end;
  11.177 +
  11.178 +
  11.179 +
  11.180  (** unparse **)
  11.181  
  11.182 +(** unparse terms, typs, sorts **)
  11.183 +
  11.184 +local
  11.185 +
  11.186 +fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
  11.187 +
  11.188 +fun unparse_t t_to_ast prt_t markup ctxt curried t =
  11.189 +  let
  11.190 +    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
  11.191 +      Syntax.rep_syntax (ProofContext.syn_of ctxt);
  11.192 +    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
  11.193 +  in
  11.194 +    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
  11.195 +      (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
  11.196 +      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
  11.197 +  end;
  11.198 +
  11.199 +in
  11.200 +
  11.201 +fun standard_unparse_sort {extern_class} ctxt =
  11.202 +  unparse_t (K sort_to_ast)
  11.203 +    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
  11.204 +    Markup.sort ctxt false;
  11.205 +
  11.206 +fun standard_unparse_typ extern ctxt =
  11.207 +  unparse_t (K typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt false;
  11.208 +
  11.209 +fun standard_unparse_term idents extern =
  11.210 +  unparse_t (term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
  11.211 +
  11.212 +end;
  11.213 +
  11.214 +
  11.215  fun unparse_sort ctxt =
  11.216 -  Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
  11.217 -    ctxt (ProofContext.syn_of ctxt);
  11.218 +  standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} ctxt;
  11.219  
  11.220  fun unparse_typ ctxt =
  11.221    let
  11.222      val tsig = ProofContext.tsig_of ctxt;
  11.223      val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
  11.224 -  in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
  11.225 +  in standard_unparse_typ extern ctxt end;
  11.226  
  11.227  fun unparse_term ctxt =
  11.228    let
  11.229 @@ -412,11 +610,47 @@
  11.230        extern_type = Type.extern_type tsig,
  11.231        extern_const = Consts.extern consts};
  11.232    in
  11.233 -    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
  11.234 -      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
  11.235 +    standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
  11.236 +      (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
  11.237    end;
  11.238  
  11.239  
  11.240 +
  11.241 +(** translations **)
  11.242 +
  11.243 +(* type propositions *)
  11.244 +
  11.245 +fun type_prop_tr' _ T [Const ("\\<^const>Pure.sort_constraint", _)] =
  11.246 +      Lexicon.const "_sort_constraint" $ term_of_typ true T
  11.247 +  | type_prop_tr' show_sorts T [t] =
  11.248 +      Lexicon.const "_ofclass" $ term_of_typ show_sorts T $ t
  11.249 +  | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
  11.250 +
  11.251 +
  11.252 +(* type reflection *)
  11.253 +
  11.254 +fun type_tr' show_sorts (Type ("itself", [T])) ts =
  11.255 +      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ show_sorts T, ts)
  11.256 +  | type_tr' _ _ _ = raise Match;
  11.257 +
  11.258 +
  11.259 +(* type constraints *)
  11.260 +
  11.261 +fun type_constraint_tr' show_sorts (Type ("fun", [T, _])) (t :: ts) =
  11.262 +      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ show_sorts T, ts)
  11.263 +  | type_constraint_tr' _ _ _ = raise Match;
  11.264 +
  11.265 +
  11.266 +(* setup translations *)
  11.267 +
  11.268 +val _ = Context.>> (Context.map_theory
  11.269 +  (Sign.add_trfunsT
  11.270 +   [("_type_prop", type_prop_tr'),
  11.271 +    ("\\<^const>TYPE", type_tr'),
  11.272 +    ("_type_constraint_", type_constraint_tr')]));
  11.273 +
  11.274 +
  11.275 +
  11.276  (** install operations **)
  11.277  
  11.278  val _ = Syntax.install_operations
    12.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Apr 06 12:55:53 2011 +0200
    12.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Apr 06 12:58:13 2011 +0200
    12.3 @@ -10,7 +10,6 @@
    12.4    val is_position: term -> bool
    12.5    val strip_positions: term -> term
    12.6    val strip_positions_ast: Ast.ast -> Ast.ast
    12.7 -  val term_of_typ: bool -> typ -> term
    12.8    val no_brackets: unit -> bool
    12.9    val no_type_brackets: unit -> bool
   12.10  end;
   12.11 @@ -18,7 +17,6 @@
   12.12  signature TYPE_EXT =
   12.13  sig
   12.14    include TYPE_EXT0
   12.15 -  val term_of_sort: sort -> term
   12.16    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   12.17    val type_ext: Syn_Ext.syn_ext
   12.18  end;
   12.19 @@ -52,42 +50,6 @@
   12.20  
   12.21  
   12.22  
   12.23 -(** output utils **)
   12.24 -
   12.25 -(* term_of_sort *)
   12.26 -
   12.27 -fun term_of_sort S =
   12.28 -  let
   12.29 -    val class = Lexicon.const o Lexicon.mark_class;
   12.30 -
   12.31 -    fun classes [c] = class c
   12.32 -      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   12.33 -  in
   12.34 -    (case S of
   12.35 -      [] => Lexicon.const "_topsort"
   12.36 -    | [c] => class c
   12.37 -    | cs => Lexicon.const "_sort" $ classes cs)
   12.38 -  end;
   12.39 -
   12.40 -
   12.41 -(* term_of_typ *)
   12.42 -
   12.43 -fun term_of_typ show_sorts ty =
   12.44 -  let
   12.45 -    fun of_sort t S =
   12.46 -      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   12.47 -      else t;
   12.48 -
   12.49 -    fun term_of (Type (a, Ts)) =
   12.50 -          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
   12.51 -      | term_of (TFree (x, S)) =
   12.52 -          if is_some (Lexicon.decode_position x) then Lexicon.free x
   12.53 -          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   12.54 -      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   12.55 -  in term_of ty end;
   12.56 -
   12.57 -
   12.58 -
   12.59  (** the type syntax **)
   12.60  
   12.61  (* print mode *)
    13.1 --- a/src/Pure/pure_thy.ML	Wed Apr 06 12:55:53 2011 +0200
    13.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 06 12:58:13 2011 +0200
    13.3 @@ -146,7 +146,6 @@
    13.4    #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
    13.5    #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
    13.6    #> Sign.add_trfuns Syntax.pure_trfuns
    13.7 -  #> Sign.add_trfunsT Syntax.pure_trfunsT
    13.8    #> Sign.local_path
    13.9    #> Sign.add_consts_i
   13.10     [(Binding.name "term", typ "'a => prop", NoSyn),