authentic syntax for classes and type constructors;
read/intern formal entities just after raw parsing, extern just before final pretty printing;
discontinued _class token translation;
moved Local_Syntax.extern_term to Syntax/printer.ML;
misc tuning;
--- a/src/Pure/Isar/local_syntax.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Isar/local_syntax.ML Wed Mar 03 00:28:22 2010 +0100
@@ -4,13 +4,11 @@
Local syntax depending on theory syntax.
*)
-val show_structs = Unsynchronized.ref false;
-
signature LOCAL_SYNTAX =
sig
type T
val syn_of: T -> Syntax.syntax
- val structs_of: T -> string list
+ val idents_of: T -> {structs: string list, fixes: string list}
val init: theory -> T
val rebuild: theory -> T -> T
datatype kind = Type | Const | Fixed
@@ -19,7 +17,6 @@
val restore_mode: T -> T -> T
val update_modesyntax: theory -> bool -> Syntax.mode ->
(kind * (string * typ * mixfix)) list -> T -> T
- val extern_term: T -> term -> term
end;
structure Local_Syntax: LOCAL_SYNTAX =
@@ -49,8 +46,7 @@
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents, ...}) = idents;
-val structs_of = #1 o idents_of;
+fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
(* build syntax *)
@@ -125,21 +121,4 @@
fun update_modesyntax thy add mode args syntax =
syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
-
-(* extern_term *)
-
-fun extern_term syntax =
- let
- val (structs, fixes) = idents_of syntax;
- fun map_free (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
- Term.Const (Syntax.mark_fixed x, T)
- else if i = 1 andalso not (! show_structs) then
- Syntax.const "_struct" $ Syntax.const "_indexdefault"
- else t
- end
- | map_free t = t;
- in Term.map_aterms map_free end;
-
end;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 03 00:28:22 2010 +0100
@@ -363,15 +363,11 @@
(Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
-fun class_markup _ c = (* FIXME authentic syntax *)
- Pretty.mark (Markup.tclassN, []) (Pretty.str c);
-
fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
val token_trans =
Syntax.tokentrans_mode ""
- [("class", class_markup),
- ("tfree", plain_markup Markup.tfree),
+ [("tfree", plain_markup Markup.tfree),
("tvar", plain_markup Markup.tvar),
("free", free_or_skolem),
("bound", plain_markup Markup.bound),
@@ -601,14 +597,12 @@
{get_sort = get_sort thy (Variable.def_sort ctxt),
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
- map_free = intern_skolem ctxt (Variable.def_type ctxt false),
- map_type = Sign.intern_tycons thy,
- map_sort = Sign.intern_sort thy}
+ map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
end;
fun decode_term ctxt =
- let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt
- in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
+ let val {get_sort, map_const, map_free} = term_context ctxt
+ in Syntax.decode_term get_sort map_const map_free end;
end;
@@ -677,26 +671,23 @@
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token Markup.sort text;
- val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
- (Sign.intern_sort (theory_of ctxt)) (syms, pos)
+ val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
in S end;
fun parse_typ ctxt text =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = theory_of ctxt;
val get_sort = get_sort thy (Variable.def_sort ctxt);
-
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Sign.intern_tycons thy
- (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
- handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
fun parse_term T ctxt text =
let
val thy = theory_of ctxt;
- val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
+ val {get_sort, map_const, map_free} = term_context ctxt;
val (T', _) = TypeInfer.paramify_dummies T 0;
val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -704,29 +695,35 @@
fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
- val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
- map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
+ val t =
+ Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+ ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
in t end;
-fun unparse_sort ctxt S =
- Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S);
+fun unparse_sort ctxt =
+ Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+ ctxt (syn_of ctxt);
-fun unparse_typ ctxt T =
- Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T);
+fun unparse_typ ctxt =
+ let
+ val thy = theory_of ctxt;
+ val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+ in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
-fun unparse_term ctxt t =
+fun unparse_term ctxt =
let
val thy = theory_of ctxt;
val syntax = syntax_of ctxt;
val consts = consts_of ctxt;
+ val extern =
+ {extern_class = Sign.extern_class thy,
+ extern_type = Sign.extern_type thy,
+ extern_const = Consts.extern consts};
in
- t
- |> Sign.extern_term thy
- |> Local_Syntax.extern_term syntax
- |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
- (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
+ Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+ (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
end;
in
@@ -1010,18 +1007,20 @@
in Syntax.Constant d end
| const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+val typ = Simple_Syntax.read_typ;
+
in
val _ = Context.>> (Context.map_theory
- (Sign.add_syntax
- [("_context_const", "id => logic", Delimfix "CONST _"),
- ("_context_const", "id => aprop", Delimfix "CONST _"),
- ("_context_const", "longid => logic", Delimfix "CONST _"),
- ("_context_const", "longid => aprop", Delimfix "CONST _"),
- ("_context_xconst", "id => logic", Delimfix "XCONST _"),
- ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
- ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
- ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
+ (Sign.add_syntax_i
+ [("_context_const", typ "id => logic", Delimfix "CONST _"),
+ ("_context_const", typ "id => aprop", Delimfix "CONST _"),
+ ("_context_const", typ "longid => logic", Delimfix "CONST _"),
+ ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
+ ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
Sign.add_advanced_trfuns
([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
@@ -1032,8 +1031,8 @@
local
-fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+fun type_syntax (Type (c, args), mx) =
+ SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
| type_syntax _ = NONE;
fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
@@ -1345,7 +1344,7 @@
val prt_term = Syntax.pretty_term ctxt;
(*structures*)
- val structs = Local_Syntax.structs_of (syntax_of ctxt);
+ val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
val prt_structs =
if null structs then []
else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
@@ -1415,3 +1414,4 @@
end;
end;
+
--- a/src/Pure/ML/ml_antiquote.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 03 00:28:22 2010 +0100
@@ -104,7 +104,7 @@
fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
Sign.read_class thy s
- |> syn ? Long_Name.base_name (* FIXME authentic syntax *)
+ |> syn ? Syntax.mark_class
|> ML_Syntax.print_string);
val _ = inline "class" (class false);
@@ -130,7 +130,7 @@
val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c)); (* FIXME authentic syntax *)
+val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
(* constants *)
--- a/src/Pure/Syntax/printer.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Mar 03 00:28:22 2010 +0100
@@ -11,29 +11,32 @@
val show_types: bool Unsynchronized.ref
val show_no_free_types: bool Unsynchronized.ref
val show_all_types: bool Unsynchronized.ref
+ val show_structs: bool Unsynchronized.ref
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
signature PRINTER =
sig
include PRINTER0
- val term_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+ 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 sort_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> 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 -> SynExt.xprod list -> prtabs -> prtabs
val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
val merge_prtabs: prtabs -> prtabs -> prtabs
- val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
- val pretty_typ_ast: Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
end;
structure Printer: PRINTER =
@@ -47,6 +50,7 @@
val show_brackets = Unsynchronized.ref false;
val show_no_free_types = Unsynchronized.ref false;
val show_all_types = Unsynchronized.ref false;
+val show_structs = Unsynchronized.ref false;
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -84,8 +88,7 @@
fun ast_of_termT ctxt trf tm =
let
- fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
- | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
| ast_of (Const (a, _)) = trans a []
| ast_of (t as _ $ _) =
@@ -105,19 +108,30 @@
(** term_to_ast **)
-fun mark_freevars ((t as Const (c, _)) $ u) =
- if member (op =) SynExt.standard_token_markers c then (t $ u)
- else t $ mark_freevars u
- | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
- | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
- | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
- | mark_freevars (t as Var (xi, T)) =
- if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
- else Lexicon.const "_var" $ t
- | mark_freevars a = a;
+fun ast_of_term idents consts ctxt trf
+ show_all_types no_freeTs show_types show_sorts show_structs tm =
+ let
+ val {structs, fixes} = idents;
-fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
- let
+ fun mark_atoms ((t as Const (c, T)) $ u) =
+ if member (op =) consts c then (t $ u)
+ else Const (Lexicon.mark_const c, 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 (Const (c, T)) = 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
+ Term.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 = SynExt.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)
@@ -148,9 +162,9 @@
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)
- | (c' as Const (c, T), ts) =>
+ | (const as Const (c, T), ts) =>
if show_all_types
- then Ast.mk_appl (constrain c' T) (map ast_of ts)
+ then Ast.mk_appl (constrain const T) (map ast_of ts)
else trans c T ts
| (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
@@ -162,18 +176,18 @@
if show_types andalso T <> dummyT then
Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
- else simple_ast_of t
+ else simple_ast_of t;
in
tm
|> SynTrans.prop_tr'
- |> (if show_types then #1 o prune_typs o rpair [] else I)
- |> mark_freevars
+ |> show_types ? (#1 o prune_typs o rpair [])
+ |> mark_atoms
|> ast_of
end;
-fun term_to_ast ctxt trf tm =
- ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
- (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
+fun term_to_ast idents consts ctxt trf tm =
+ ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+ (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
@@ -267,8 +281,10 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
let
+ val {extern_class, extern_type, extern_const} = extern;
+
fun token_trans a x =
(case tokentrf a of
NONE =>
@@ -291,7 +307,7 @@
val (Ts, args') = synT markup (symbs, args);
in
if type_mode then (astT (t, p) @ Ts, args')
- else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
+ else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
end
| synT markup (String s :: symbs, args) =
let val (Ts, args') = synT markup (symbs, args);
@@ -312,7 +328,6 @@
val (Ts, args') = synT markup (symbs, args);
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- | synT _ (_ :: _, []) = sys_error "synT"
and parT markup (pr, args, p, p': int) = #1 (synT markup
(if p > p' orelse
@@ -320,13 +335,12 @@
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
- and atomT a =
- (case try Lexicon.unmark_const a of
- SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
- | NONE =>
- (case try Lexicon.unmark_fixed a of
- SOME x => the (token_trans "_free" x)
- | NONE => Pretty.str a))
+ and atomT a = a |> Lexicon.unmark
+ {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
+ case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
+ case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
+ case_fixed = fn x => the (token_trans "_free" x),
+ case_default = Pretty.str}
and prefixT (_, a, [], _) = [atomT a]
| prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -334,15 +348,16 @@
and splitT 0 ([x], ys) = (x, ys)
| splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
- | splitT _ _ = sys_error "splitT"
and combT (tup as (c, a, args, p)) =
let
val nargs = length args;
- val markup = Pretty.mark
- (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
- (Markup.fixed (Lexicon.unmark_fixed a)))
- handle Fail _ => I;
+ val markup = a |> Lexicon.unmark
+ {case_class = Pretty.mark o Markup.tclass,
+ case_type = Pretty.mark o Markup.tycon,
+ case_const = Pretty.mark o Markup.const,
+ case_fixed = Pretty.mark o Markup.fixed,
+ case_default = K I};
(*find matching table entry, or print as prefix / postfix*)
fun prnt ([], []) = prefixT tup
@@ -371,15 +386,16 @@
(* pretty_term_ast *)
-fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
- pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
+ pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf false curried ast 0;
(* pretty_typ_ast *)
-fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
- pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
+ pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
+ ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf true false ast 0;
end;
--- a/src/Pure/Syntax/syn_ext.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Mar 03 00:28:22 2010 +0100
@@ -282,7 +282,8 @@
if not (exists is_index args) then (const, typ, [])
else
let
- val indexed_const = if const <> "" then "_indexed_" ^ const
+ val indexed_const =
+ if const <> "" then const ^ "_indexed"
else err_in_mfix "Missing constant name for indexed syntax" mfix;
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
@@ -387,7 +388,7 @@
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
val standard_token_classes =
- ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
+ ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
--- a/src/Pure/Syntax/syn_trans.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Wed Mar 03 00:28:22 2010 +0100
@@ -34,16 +34,16 @@
val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
val pure_trfuns:
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (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 *
- (string * (bool -> typ -> term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (bool -> typ -> term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list
end;
signature SYN_TRANS =
@@ -131,7 +131,7 @@
fun mk_type ty =
Lexicon.const "_constrain" $
- Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
+ Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
| ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
@@ -143,7 +143,7 @@
(* meta propositions *)
-fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
+fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
| aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
@@ -195,7 +195,8 @@
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
- list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts)
+ list_comb (c $ update_name_tr [t] $
+ (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -368,7 +369,7 @@
fun is_prop Ts t =
fastype_of1 (Ts, t) = propT handle TERM _ => false;
- fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
+ fun is_term (Const ("Pure.term", _) $ _) = true
| is_term _ = false;
fun tr' _ (t as Const _) = t
@@ -381,7 +382,7 @@
| tr' Ts (t as Bound _) =
if is_prop Ts t then aprop t else t
| tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
- | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
+ | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
else tr' Ts t1 $ tr' Ts t2
| tr' Ts (t as t1 $ t2) =
@@ -568,7 +569,7 @@
val free_fixed = Term.map_aterms
(fn t as Const (c, T) =>
- (case try (unprefix Lexicon.fixedN) c of
+ (case try Lexicon.unmark_fixed c of
NONE => t
| SOME x => Free (x, T))
| t => t);
--- a/src/Pure/Syntax/syntax.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Mar 03 00:28:22 2010 +0100
@@ -29,7 +29,10 @@
val mode_default: mode
val mode_input: mode
val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syn: syntax
+ val empty_syntax: syntax
+ val basic_syntax:
+ {read_class: theory -> xstring -> string,
+ read_type: theory -> xstring -> string} -> syntax
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -41,25 +44,24 @@
val ambiguity_limit: int Unsynchronized.ref
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> Proof.context ->
+ (string -> bool * string) -> (string -> string option) -> Proof.context ->
(string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> sort
+ ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+ val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
ParseRule of 'a * 'a |
PrintRule of 'a * 'a |
ParsePrintRule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val standard_unparse_term: (string -> xstring) ->
- Proof.context -> syntax -> bool -> term -> Pretty.T
- val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
- val update_consts: string list -> syntax -> syntax
+ 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 standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> syntax -> typ -> Pretty.T
+ val standard_unparse_sort: {extern_class: string -> xstring} ->
+ Proof.context -> syntax -> sort -> Pretty.T
val update_trfuns:
(string * ((ast list -> ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
@@ -300,7 +302,7 @@
lexicon =
if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
gram = if changed then Parser.extend_gram gram xprods else gram,
- consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
+ consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -381,9 +383,9 @@
(* basic syntax *)
-val basic_syn =
+fun basic_syntax read =
empty_syntax
- |> update_syntax mode_default TypeExt.type_ext
+ |> update_syntax mode_default (TypeExt.type_ext read)
|> update_syntax mode_default SynExt.pure_ext;
val basic_nonterms =
@@ -547,26 +549,25 @@
map (Pretty.string_of_term pp) (take limit results)))
end;
-fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
- ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
- |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
+ |> map (TypeExt.decode_term get_sort map_const map_free)
|> disambig (Printer.pp_show_brackets pp) check;
(* read types *)
-fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
+fun standard_parse_typ ctxt syn get_sort (syms, pos) =
(case read ctxt (K false) syn SynExt.typeT (syms, pos) of
- [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
+ [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
| _ => error (ambiguity_msg pos));
(* read sorts *)
-fun standard_parse_sort ctxt syn map_sort (syms, pos) =
+fun standard_parse_sort ctxt syn (syms, pos) =
(case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
- [t] => TypeExt.sort_of_term map_sort t
+ [t] => TypeExt.sort_of_term t
| _ => error (ambiguity_msg pos));
@@ -640,8 +641,8 @@
fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
let
- val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
- val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+ 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 ()))
@@ -650,14 +651,16 @@
in
-fun standard_unparse_term extern =
- unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_term idents extern =
+ unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-fun standard_unparse_typ ctxt syn =
- unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ 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_sort ctxt syn =
- unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
+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;
end;
@@ -667,7 +670,6 @@
fun ext_syntax f decls = update_syntax mode_default (f decls);
-val update_consts = ext_syntax SynExt.syn_ext_const_names;
val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
--- a/src/Pure/Syntax/type_ext.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML Wed Mar 03 00:28:22 2010 +0100
@@ -1,19 +1,17 @@
(* Title: Pure/Syntax/type_ext.ML
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-Utilities for input and output of types. Also the concrete syntax of
-types, which is required to bootstrap Pure.
+Utilities for input and output of types. The concrete syntax of types.
*)
signature TYPE_EXT0 =
sig
- val sort_of_term: (sort -> sort) -> term -> sort
- val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
- val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
+ val sort_of_term: term -> sort
+ val term_sorts: term -> (indexname * sort) list
+ val typ_of_term: (indexname -> sort) -> term -> typ
val type_constraint: typ -> term -> term
val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> term -> term
+ (string -> bool * string) -> (string -> string option) -> term -> term
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
@@ -25,7 +23,9 @@
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val sortT: typ
- val type_ext: SynExt.syn_ext
+ val type_ext:
+ {read_class: theory -> string -> string,
+ read_type: theory -> string -> string} -> SynExt.syn_ext
end;
structure TypeExt: TYPE_EXT =
@@ -35,30 +35,28 @@
(* sort_of_term *)
-fun sort_of_term (map_sort: sort -> sort) tm =
+fun sort_of_term tm =
let
- fun classes (Const (c, _)) = [c]
- | classes (Free (c, _)) = [c]
- | classes (Const ("_class", _) $ Free (c, _)) = [c]
- | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
- | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+ fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+ fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+ fun classes (Const (s, _)) = [class s]
+ | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+ | classes _ = err ();
fun sort (Const ("_topsort", _)) = []
- | sort (Const (c, _)) = [c]
- | sort (Free (c, _)) = [c]
- | sort (Const ("_class", _) $ Free (c, _)) = [c]
+ | sort (Const (s, _)) = [class s]
| sort (Const ("_sort", _) $ cs) = classes cs
- | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
- in map_sort (sort tm) end;
+ | sort _ = err ();
+ in sort tm end;
(* term_sorts *)
-fun term_sorts map_sort tm =
+fun term_sorts tm =
let
- val sort_of = sort_of_term map_sort;
+ val sort_of = sort_of_term;
fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
insert (op =) ((x, ~1), sort_of cs)
@@ -76,11 +74,11 @@
(* typ_of_term *)
-fun typ_of_term get_sort map_sort t =
+fun typ_of_term get_sort tm =
let
- fun typ_of (Free (x, _)) =
- if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
- else Type (x, [])
+ fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+ fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
| typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
| typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
| typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
@@ -90,17 +88,16 @@
| typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
| typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
TVar (xi, get_sort xi)
- | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
- | typ_of tm =
+ | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+ | typ_of t =
let
- val (t, ts) = Term.strip_comb tm;
+ val (head, args) = Term.strip_comb t;
val a =
- (case t of
- Const (x, _) => x
- | Free (x, _) => x
- | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
- in Type (a, map typ_of ts) end;
- in typ_of t end;
+ (case head of
+ Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+ | _ => err ());
+ in Type (a, map typ_of args) end;
+ in typ_of tm end;
(* decode_term -- transform parse tree into raw term *)
@@ -109,30 +106,30 @@
if T = dummyT then t
else Const ("_type_constraint_", T --> T) $ t;
-fun decode_term get_sort map_const map_free map_type map_sort tm =
+fun decode_term get_sort map_const map_free tm =
let
- val sort_env = term_sorts map_sort tm;
- val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
+ val sort_env = term_sorts tm;
+ val decodeT = typ_of_term (get_sort sort_env);
fun decode (Const ("_constrain", _) $ t $ typ) =
type_constraint (decodeT typ) (decode t)
| decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
if T = dummyT then Abs (x, decodeT typ, decode t)
- else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
- | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
+ else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+ | decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
let val c =
(case try Lexicon.unmark_const a of
SOME c => c
| NONE => snd (map_const a))
- in Const (c, map_type T) end
+ in Const (c, T) end
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
- (SOME x, _) => Free (x, map_type T)
- | (_, (true, c)) => Const (c, map_type T)
- | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
- | decode (Var (xi, T)) = Var (xi, map_type T)
+ (SOME x, _) => Free (x, T)
+ | (_, (true, c)) => Const (c, T)
+ | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
+ | decode (Var (xi, T)) = Var (xi, T)
| decode (t as Bound _) = t;
in decode tm end;
@@ -144,10 +141,9 @@
fun term_of_sort S =
let
- fun class c = Lexicon.const "_class" $ Lexicon.free c;
+ val class = Lexicon.const o Lexicon.mark_class;
- fun classes [] = sys_error "term_of_sort"
- | classes [c] = class c
+ fun classes [c] = class c
| classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
in
(case S of
@@ -165,7 +161,8 @@
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 a, map term_of Ts)
+ fun term_of (Type (a, Ts)) =
+ Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) = 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;
@@ -193,15 +190,29 @@
(* parse ast translations *)
-fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
- | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+val class_ast = Ast.Constant o Lexicon.mark_class;
+val type_ast = Ast.Constant o Lexicon.mark_type;
+
+fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
+ | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
+
+fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
+ Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
+ | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
-fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
- Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
- | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
+fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
+ | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
+
+fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
+ Ast.Appl [type_ast (read_type c), ty]
+ | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+
+fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
+ Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
+ | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
- Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
+ Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
| bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
@@ -212,10 +223,10 @@
| tappl_ast_tr' (f, ty :: tys) =
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
-fun fun_ast_tr' (*"fun"*) asts =
+fun fun_ast_tr' (*"\\<^type>fun"*) asts =
if no_brackets () orelse no_type_brackets () then raise Match
else
- (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
+ (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
(dom as _ :: _ :: _, cod)
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
| _ => raise Match);
@@ -229,20 +240,20 @@
local open Lexicon SynExt in
-val type_ext = syn_ext' false (K false)
+fun type_ext {read_class, read_type} = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
- Mfix ("_", idT --> typeT, "", [], max_pri),
- Mfix ("_", longidT --> typeT, "", [], max_pri),
+ Mfix ("_", idT --> typeT, "_type_name", [], max_pri),
+ Mfix ("_", longidT --> typeT, "_type_name", [], max_pri),
Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri),
- Mfix ("_", idT --> sortT, "", [], max_pri),
- Mfix ("_", longidT --> sortT, "", [], max_pri),
+ Mfix ("_", idT --> sortT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> sortT, "_class_name", [], max_pri),
Mfix ("{}", sortT, "_topsort", [], max_pri),
Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri),
- Mfix ("_", idT --> classesT, "", [], max_pri),
- Mfix ("_", longidT --> classesT, "", [], max_pri),
+ Mfix ("_", idT --> classesT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> classesT, "_class_name", [], max_pri),
Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_,_", [longidT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
@@ -251,16 +262,21 @@
Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
Mfix ("_", typeT --> typesT, "", [], max_pri),
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri),
- Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0),
+ Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0),
Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0),
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
- Mfix ("'_", typeT, "dummy", [], max_pri)]
+ Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
[]
(map SynExt.mk_trfun
- [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+ [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
+ ("_classes", classes_tr o read_class o ProofContext.theory_of),
+ ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
+ ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
+ ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
+ ("_bracket", K bracket_ast_tr)],
[],
[],
- map SynExt.mk_trfun [("fun", K fun_ast_tr')])
+ map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
--- a/src/Pure/pure_thy.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/pure_thy.ML Wed Mar 03 00:28:22 2010 +0100
@@ -225,6 +225,8 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
+
+val tycon = Syntax.mark_type;
val const = Syntax.mark_const;
val typeT = Syntax.typeT;
@@ -318,21 +320,21 @@
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
- [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
- ("_type_constraint_", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
- (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
+ [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+ ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
+ ("_type_constraint_", typ "'a", NoSyn),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
+ (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)
--- a/src/Pure/sign.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/sign.ML Wed Mar 03 00:28:22 2010 +0100
@@ -56,10 +56,7 @@
val intern_sort: theory -> sort -> sort
val extern_sort: theory -> sort -> sort
val intern_typ: theory -> typ -> typ
- val extern_typ: theory -> typ -> typ
val intern_term: theory -> term -> term
- val extern_term: theory -> term -> term
- val intern_tycons: theory -> typ -> typ
val the_type_decl: theory -> string -> Type.decl
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
@@ -157,7 +154,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
@@ -266,41 +263,10 @@
| map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
| map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
-val add_classesT = Term.fold_atyps
- (fn TFree (_, S) => fold (insert (op =)) S
- | TVar (_, S) => fold (insert (op =)) S
- | _ => I);
-
-fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
- | add_tyconsT _ = I;
-
-val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
-
-fun mapping add_names f t =
- let
- fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
- val tab = map_filter f' (add_names t []);
- fun get x = the_default x (AList.lookup (op =) tab x);
- in get end;
-
-fun typ_mapping f g thy T =
- T |> map_typ
- (mapping add_classesT (f thy) T)
- (mapping add_tyconsT (g thy) T);
-
-fun term_mapping f g h thy t =
- t |> map_term
- (mapping (Term.fold_types add_classesT) (f thy) t)
- (mapping (Term.fold_types add_tyconsT) (g thy) t)
- (mapping add_consts (h thy) t);
-
in
-val intern_typ = typ_mapping intern_class intern_type;
-val extern_typ = typ_mapping extern_class extern_type;
-val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
-val intern_tycons = typ_mapping (K I) intern_type;
+fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
+fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
end;
@@ -424,6 +390,27 @@
val cert_arity = prep_arity (K I) certify_sort;
+(* type syntax entities *)
+
+local
+
+fun read_type thy text =
+ let
+ val (syms, pos) = Syntax.read_token text;
+ val c = intern_type thy (Symbol_Pos.content syms);
+ val _ = the_type_decl thy c;
+ val _ = Position.report (Markup.tycon c) pos;
+ in c end;
+
+in
+
+val _ = Context.>>
+ (Context.map_theory
+ (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
+
+end;
+
+
(** signature extension functions **) (*exception ERROR/TYPE*)
@@ -438,11 +425,13 @@
(* add type constructors *)
+val type_syntax = Syntax.mark_type oo full_name;
+
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
+ (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
val decls = map (fn (a, n, _) => (a, n)) types;
val tsig' = fold (Type.add_type naming) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -452,9 +441,8 @@
fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
val tsig' = fold (Type.add_nonterminal naming) ns tsig;
- in (naming, syn', tsig', consts) end);
+ in (naming, syn, tsig', consts) end);
(* add type abbreviations *)
@@ -465,7 +453,7 @@
val ctxt = ProofContext.init thy;
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
+ [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
@@ -495,8 +483,8 @@
fun type_notation add mode args =
let
- fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+ fun type_syntax (Type (c, args), mx) =
+ SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
| type_syntax _ = NONE;
in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
@@ -579,9 +567,8 @@
fun primitive_class (bclass, classes) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
- in (naming, syn', tsig', consts) end)
+ in (naming, syn, tsig', consts) end)
|> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);