--- a/src/HOL/Groups.thy Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Groups.thy Wed Apr 06 12:58:13 2011 +0200
@@ -130,7 +130,7 @@
if not (null ts) orelse T = dummyT
orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
then raise Match
- else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+ else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
*} -- {* show types that are presumably too general *}
--- a/src/HOL/Library/Cardinality.thy Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Library/Cardinality.thy Wed Apr 06 12:58:13 2011 +0200
@@ -37,7 +37,7 @@
typed_print_translation {*
let
fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
- Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
+ Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
in [(@{const_syntax card}, card_univ_tr')]
end
*}
--- a/src/HOL/Tools/numeral_syntax.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Wed Apr 06 12:58:13 2011 +0200
@@ -72,7 +72,9 @@
fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
- else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
+ else
+ Syntax.const Syntax.constrainC $ syntax_numeral t $
+ Syntax_Phases.term_of_typ show_sorts T
in list_comb (t', ts) end
| numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
if T = dummyT then list_comb (syntax_numeral t, ts)
--- a/src/HOL/Tools/record.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Tools/record.ML Wed Apr 06 12:58:13 2011 +0200
@@ -708,7 +708,7 @@
val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
- val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
+ val term_of_typ = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
val alphas' =
map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
@@ -819,7 +819,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
+ val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
fun strip_fields T =
(case T of
@@ -865,7 +865,7 @@
fun mk_type_abbr subst name args =
let val abbrT = Type (name, map (varifyT o TFree) args)
- in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
+ in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
--- a/src/HOL/Typerep.thy Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Typerep.thy Wed Apr 06 12:58:13 2011 +0200
@@ -36,7 +36,7 @@
(Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
- (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
+ (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
| typerep_tr' _ T ts = raise Match;
in [(@{const_syntax typerep}, typerep_tr')] end
*}
--- a/src/HOL/ex/Numeral.thy Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Apr 06 12:58:13 2011 +0200
@@ -309,7 +309,7 @@
case T of
Type (@{type_name fun}, [_, T']) =>
if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
- else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+ else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
end;
in [(@{const_syntax of_num}, num_tr')] end
--- a/src/Pure/Syntax/printer.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Wed Apr 06 12:58:13 2011 +0200
@@ -23,17 +23,12 @@
val show_question_marks_raw: Config.raw
val show_question_marks: bool Config.T
val pretty_priority: int Config.T
+ val apply_trans: 'a -> ('a -> 'b -> 'c) list -> 'b -> 'c
end;
signature PRINTER =
sig
include PRINTER0
- val sort_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
- val typ_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
- val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
@@ -52,7 +47,6 @@
structure Printer: PRINTER =
struct
-
(** options for printing **)
val show_brackets_default = Unsynchronized.ref false;
@@ -81,150 +75,6 @@
-(** misc utils **)
-
-(* apply print (ast) translation function *)
-
-fun apply_trans ctxt fns args =
- let
- fun app_first [] = raise Match
- | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
- in app_first fns end;
-
-fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
-
-
-(* simple_ast_of *)
-
-fun simple_ast_of ctxt =
- let
- val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
- fun ast_of (Const (c, _)) = Ast.Constant c
- | ast_of (Free (x, _)) = Ast.Variable x
- | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
- | ast_of (t as _ $ _) =
- let val (f, args) = strip_comb t
- in Ast.mk_appl (ast_of f) (map ast_of args) end
- | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
- | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
- in ast_of end;
-
-
-
-(** sort_to_ast, typ_to_ast **)
-
-fun ast_of_termT ctxt trf tm =
- let
- val ctxt' = Config.put show_sorts false ctxt;
- fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
- | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
- | ast_of (Const (a, _)) = trans a []
- | ast_of (t as _ $ _) =
- (case strip_comb t of
- (Const (a, _), args) => trans a args
- | (f, args) => Ast.Appl (map ast_of (f :: args)))
- | ast_of t = simple_ast_of ctxt t
- and trans a args =
- ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
- handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
- in ast_of tm end;
-
-fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T =
- ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
-
-
-
-(** term_to_ast **)
-
-fun term_to_ast idents consts ctxt trf tm =
- let
- val show_types =
- Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
- Config.get ctxt show_all_types;
- val show_sorts = Config.get ctxt show_sorts;
- val show_structs = Config.get ctxt show_structs;
- val show_free_types = Config.get ctxt show_free_types;
- val show_all_types = Config.get ctxt show_all_types;
-
- val {structs, fixes} = idents;
-
- fun mark_atoms ((t as Const (c, T)) $ u) =
- if member (op =) Syn_Ext.standard_token_markers c
- then t $ u else mark_atoms t $ mark_atoms u
- | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
- | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
- | mark_atoms (t as Const (c, T)) =
- if member (op =) consts c then t
- else Const (Lexicon.mark_const c, T)
- | mark_atoms (t as Free (x, T)) =
- let val i = find_index (fn s => s = x) structs + 1 in
- if i = 0 andalso member (op =) fixes x then
- Const (Lexicon.mark_fixed x, T)
- else if i = 1 andalso not show_structs then
- Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
- else Lexicon.const "_free" $ t
- end
- | mark_atoms (t as Var (xi, T)) =
- if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
- else Lexicon.const "_var" $ t
- | mark_atoms a = a;
-
- fun prune_typs (t_seen as (Const _, _)) = t_seen
- | prune_typs (t as Free (x, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
- else (t, t :: seen)
- | prune_typs (t as Var (xi, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
- else (t, t :: seen)
- | prune_typs (t_seen as (Bound _, _)) = t_seen
- | prune_typs (Abs (x, ty, t), seen) =
- let val (t', seen') = prune_typs (t, seen);
- in (Abs (x, ty, t'), seen') end
- | prune_typs (t1 $ t2, seen) =
- let
- val (t1', seen') = prune_typs (t1, seen);
- val (t2', seen'') = prune_typs (t2, seen');
- in (t1' $ t2', seen'') end;
-
- fun ast_of tm =
- (case strip_comb tm of
- (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
- | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
- | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
- | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
- | (Const ("_idtdummy", T), ts) =>
- Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
- | (const as Const (c, T), ts) =>
- if show_all_types
- then Ast.mk_appl (constrain const T) (map ast_of ts)
- else trans c T ts
- | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
-
- and trans a T args =
- ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
- handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
-
- and constrain t T =
- if show_types andalso T <> dummyT then
- Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
- ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
- else simple_ast_of ctxt t;
- in
- tm
- |> Syn_Trans.prop_tr'
- |> show_types ? (#1 o prune_typs o rpair [])
- |> mark_atoms
- |> ast_of
- end;
-
-
-
(** type prtabs **)
datatype symb =
@@ -311,6 +161,12 @@
(** pretty term or typ asts **)
+fun apply_trans ctxt fns args =
+ let
+ fun app_first [] = raise Match
+ | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
+ in app_first fns end;
+
fun is_chain [Block (_, pr)] = is_chain pr
| is_chain [Arg _] = true
| is_chain _ = false;
--- a/src/Pure/Syntax/syn_ext.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Wed Apr 06 12:58:13 2011 +0200
@@ -20,6 +20,7 @@
string -> (string * (Proof.context -> string -> Pretty.T)) list ->
(string * string * (Proof.context -> string -> Pretty.T)) list
val standard_token_classes: string list
+ val standard_token_markers: string list
end;
signature SYN_EXT =
@@ -83,7 +84,6 @@
(string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
- val standard_token_markers: string list
val pure_ext: syn_ext
end;
--- a/src/Pure/Syntax/syn_trans.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Wed Apr 06 12:58:13 2011 +0200
@@ -42,7 +42,6 @@
(string * (term list -> term)) list *
(string * (term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list
- val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
val struct_trfuns: string list ->
(string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
@@ -354,15 +353,6 @@
| idtyp_ast_tr' _ _ = raise Match;
-(* type propositions *)
-
-fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
- Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
- | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
- Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
- | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
-
-
(* meta propositions *)
fun prop_tr' tm =
@@ -408,20 +398,6 @@
| _ => raise Match);
-(* type reflection *)
-
-fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
- Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
- | type_tr' _ _ _ = raise Match;
-
-
-(* type constraints *)
-
-fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
- Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
- | type_constraint_tr' _ _ _ = raise Match;
-
-
(* dependent / nondependent quantifiers *)
fun var_abs mark (x, T, b) =
@@ -533,11 +509,6 @@
("\\<^const>==>", impl_ast_tr'),
("_index", index_ast_tr')]);
-val pure_trfunsT =
- [("_type_prop", type_prop_tr'),
- ("\\<^const>TYPE", type_tr'),
- ("_type_constraint_", type_constraint_tr')];
-
fun struct_trfuns structs =
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
--- a/src/Pure/Syntax/syntax.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Apr 06 12:58:13 2011 +0200
@@ -95,6 +95,9 @@
val string_of_sort_global: theory -> sort -> string
val pp: Proof.context -> Pretty.pp
val pp_global: theory -> Pretty.pp
+ val lookup_tokentr:
+ (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list ->
+ string list -> string -> (Proof.context -> string -> Pretty.T) option
type ruletab
type syntax
val rep_syntax: syntax ->
@@ -135,13 +138,6 @@
Parse_Print_Rule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val standard_unparse_sort: {extern_class: string -> xstring} ->
- Proof.context -> syntax -> sort -> Pretty.T
- val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
- Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_term: {structs: string list, fixes: string list} ->
- {extern_class: string -> xstring, extern_type: string -> xstring,
- extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
val update_trfuns:
(string * ((Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
@@ -415,7 +411,6 @@
(* print (ast) translations *)
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
@@ -425,12 +420,14 @@
(** tables of token translation functions **)
fun lookup_tokentr tabs modes =
- let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
+ let val trs =
+ distinct (eq_fst (op = : string * string -> bool))
+ (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
in fn c => Option.map fst (AList.lookup (op =) trs c) end;
fun merge_tokentrtabs tabs1 tabs2 =
let
- fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
+ fun eq_tr ((c1, (_, s1: stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
fun name (s, _) = implode (tl (Symbol.explode s));
@@ -754,37 +751,6 @@
-(** unparse terms, typs, sorts **)
-
-local
-
-fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
- let
- val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
- val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
- in
- Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
- (lookup_tokentr tokentrtab (print_mode_value ()))
- (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
- end;
-
-in
-
-fun standard_unparse_sort {extern_class} ctxt syn =
- unparse_t (K Printer.sort_to_ast)
- (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
- Markup.sort ctxt syn false;
-
-fun standard_unparse_typ extern ctxt syn =
- unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-
-fun standard_unparse_term idents extern =
- unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-
-end;
-
-
-
(** modify syntax **)
fun ext_syntax f decls = update_syntax mode_default (f decls);
@@ -813,6 +779,5 @@
forget_structure "Syn_Ext";
forget_structure "Type_Ext";
-forget_structure "Syn_Trans";
forget_structure "Mixfix";
-forget_structure "Printer";
+
--- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 12:58:13 2011 +0200
@@ -12,6 +12,7 @@
val decode_term: Proof.context ->
Position.reports * term Exn.result -> Position.reports * term Exn.result
val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
+ val term_of_typ: bool -> typ -> term
end
structure Syntax_Phases: SYNTAX_PHASES =
@@ -390,17 +391,214 @@
+(** encode parse trees **)
+
+(* term_of_sort *)
+
+fun term_of_sort S =
+ let
+ val class = Lexicon.const o Lexicon.mark_class;
+
+ fun classes [c] = class c
+ | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
+ in
+ (case S of
+ [] => Lexicon.const "_topsort"
+ | [c] => class c
+ | cs => Lexicon.const "_sort" $ classes cs)
+ end;
+
+
+(* term_of_typ *)
+
+fun term_of_typ show_sorts ty =
+ let
+ fun of_sort t S =
+ if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
+ else t;
+
+ fun term_of (Type (a, Ts)) =
+ Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
+ | term_of (TFree (x, S)) =
+ if is_some (Lexicon.decode_position x) then Lexicon.free x
+ else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
+ | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
+ in term_of ty end;
+
+
+(* simple_ast_of *)
+
+fun simple_ast_of ctxt =
+ let
+ val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
+ fun ast_of (Const (c, _)) = Ast.Constant c
+ | ast_of (Free (x, _)) = Ast.Variable x
+ | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
+ | ast_of (t as _ $ _) =
+ let val (f, args) = strip_comb t
+ in Ast.mk_appl (ast_of f) (map ast_of args) end
+ | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+ | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+ in ast_of end;
+
+
+(* sort_to_ast and typ_to_ast *)
+
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
+
+fun ast_of_termT ctxt trf tm =
+ let
+ val ctxt' = Config.put show_sorts false ctxt;
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
+ | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
+ | ast_of (Const (a, _)) = trans a []
+ | ast_of (t as _ $ _) =
+ (case strip_comb t of
+ (Const (a, _), args) => trans a args
+ | (f, args) => Ast.Appl (map ast_of (f :: args)))
+ | ast_of t = simple_ast_of ctxt t
+ and trans a args =
+ ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args)
+ handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
+ in ast_of tm end;
+
+fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ (Config.get ctxt show_sorts) T);
+
+
+(* term_to_ast *)
+
+fun term_to_ast idents consts ctxt trf tm =
+ let
+ val show_types =
+ Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+ Config.get ctxt show_all_types;
+ val show_sorts = Config.get ctxt show_sorts;
+ val show_structs = Config.get ctxt show_structs;
+ val show_free_types = Config.get ctxt show_free_types;
+ val show_all_types = Config.get ctxt show_all_types;
+
+ val {structs, fixes} = idents;
+
+ fun mark_atoms ((t as Const (c, T)) $ u) =
+ if member (op =) Syntax.standard_token_markers c
+ then t $ u else mark_atoms t $ mark_atoms u
+ | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+ | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+ | mark_atoms (t as Const (c, T)) =
+ if member (op =) consts c then t
+ else Const (Lexicon.mark_const c, T)
+ | mark_atoms (t as Free (x, T)) =
+ let val i = find_index (fn s => s = x) structs + 1 in
+ if i = 0 andalso member (op =) fixes x then
+ Const (Lexicon.mark_fixed x, T)
+ else if i = 1 andalso not show_structs then
+ Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+ else Lexicon.const "_free" $ t
+ end
+ | mark_atoms (t as Var (xi, T)) =
+ if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
+ else Lexicon.const "_var" $ t
+ | mark_atoms a = a;
+
+ fun prune_typs (t_seen as (Const _, _)) = t_seen
+ | prune_typs (t as Free (x, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
+ else (t, t :: seen)
+ | prune_typs (t as Var (xi, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+ else (t, t :: seen)
+ | prune_typs (t_seen as (Bound _, _)) = t_seen
+ | prune_typs (Abs (x, ty, t), seen) =
+ let val (t', seen') = prune_typs (t, seen);
+ in (Abs (x, ty, t'), seen') end
+ | prune_typs (t1 $ t2, seen) =
+ let
+ val (t1', seen') = prune_typs (t1, seen);
+ val (t2', seen'') = prune_typs (t2, seen');
+ in (t1' $ t2', seen'') end;
+
+ fun ast_of tm =
+ (case strip_comb tm of
+ (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
+ | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+ | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ | (Const ("_idtdummy", T), ts) =>
+ Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
+ | (const as Const (c, T), ts) =>
+ if show_all_types
+ then Ast.mk_appl (constrain const T) (map ast_of ts)
+ else trans c T ts
+ | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
+
+ and trans a T args =
+ ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args)
+ handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
+
+ and constrain t T =
+ if show_types andalso T <> dummyT then
+ Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
+ ast_of_termT ctxt trf (term_of_typ show_sorts T)]
+ else simple_ast_of ctxt t;
+ in
+ tm
+ |> Syn_Trans.prop_tr'
+ |> show_types ? (#1 o prune_typs o rpair [])
+ |> mark_atoms
+ |> ast_of
+ end;
+
+
+
(** unparse **)
+(** unparse terms, typs, sorts **)
+
+local
+
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+
+fun unparse_t t_to_ast prt_t markup ctxt curried t =
+ let
+ val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
+ Syntax.rep_syntax (ProofContext.syn_of ctxt);
+ val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
+ in
+ Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
+ (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
+ (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
+ end;
+
+in
+
+fun standard_unparse_sort {extern_class} ctxt =
+ unparse_t (K sort_to_ast)
+ (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+ Markup.sort ctxt false;
+
+fun standard_unparse_typ extern ctxt =
+ unparse_t (K typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt false;
+
+fun standard_unparse_term idents extern =
+ unparse_t (term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
+
+end;
+
+
fun unparse_sort ctxt =
- Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
- ctxt (ProofContext.syn_of ctxt);
+ standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} ctxt;
fun unparse_typ ctxt =
let
val tsig = ProofContext.tsig_of ctxt;
val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
- in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
+ in standard_unparse_typ extern ctxt end;
fun unparse_term ctxt =
let
@@ -412,11 +610,47 @@
extern_type = Type.extern_type tsig,
extern_const = Consts.extern consts};
in
- Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
- (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
+ standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+ (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
end;
+
+(** translations **)
+
+(* type propositions *)
+
+fun type_prop_tr' _ T [Const ("\\<^const>Pure.sort_constraint", _)] =
+ Lexicon.const "_sort_constraint" $ term_of_typ true T
+ | type_prop_tr' show_sorts T [t] =
+ Lexicon.const "_ofclass" $ term_of_typ show_sorts T $ t
+ | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
+
+
+(* type reflection *)
+
+fun type_tr' show_sorts (Type ("itself", [T])) ts =
+ Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ show_sorts T, ts)
+ | type_tr' _ _ _ = raise Match;
+
+
+(* type constraints *)
+
+fun type_constraint_tr' show_sorts (Type ("fun", [T, _])) (t :: ts) =
+ Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ show_sorts T, ts)
+ | type_constraint_tr' _ _ _ = raise Match;
+
+
+(* setup translations *)
+
+val _ = Context.>> (Context.map_theory
+ (Sign.add_trfunsT
+ [("_type_prop", type_prop_tr'),
+ ("\\<^const>TYPE", type_tr'),
+ ("_type_constraint_", type_constraint_tr')]));
+
+
+
(** install operations **)
val _ = Syntax.install_operations
--- a/src/Pure/Syntax/type_ext.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Wed Apr 06 12:58:13 2011 +0200
@@ -10,7 +10,6 @@
val is_position: term -> bool
val strip_positions: term -> term
val strip_positions_ast: Ast.ast -> Ast.ast
- val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
end;
@@ -18,7 +17,6 @@
signature TYPE_EXT =
sig
include TYPE_EXT0
- val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val type_ext: Syn_Ext.syn_ext
end;
@@ -52,42 +50,6 @@
-(** output utils **)
-
-(* term_of_sort *)
-
-fun term_of_sort S =
- let
- val class = Lexicon.const o Lexicon.mark_class;
-
- fun classes [c] = class c
- | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
- in
- (case S of
- [] => Lexicon.const "_topsort"
- | [c] => class c
- | cs => Lexicon.const "_sort" $ classes cs)
- end;
-
-
-(* term_of_typ *)
-
-fun term_of_typ show_sorts ty =
- let
- fun of_sort t S =
- if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
- else t;
-
- fun term_of (Type (a, Ts)) =
- Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
- | term_of (TFree (x, S)) =
- if is_some (Lexicon.decode_position x) then Lexicon.free x
- else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
- | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
- in term_of ty end;
-
-
-
(** the type syntax **)
(* print mode *)
--- a/src/Pure/pure_thy.ML Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/pure_thy.ML Wed Apr 06 12:58:13 2011 +0200
@@ -146,7 +146,6 @@
#> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
#> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
#> Sign.add_trfuns Syntax.pure_trfuns
- #> Sign.add_trfunsT Syntax.pure_trfunsT
#> Sign.local_path
#> Sign.add_consts_i
[(Binding.name "term", typ "'a => prop", NoSyn),