--- a/src/Pure/Isar/proof_context.ML Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 09 23:29:04 2010 +0100
@@ -28,6 +28,7 @@
val full_name: Proof.context -> binding -> string
val syn_of: Proof.context -> Syntax.syntax
val tsig_of: Proof.context -> Type.tsig
+ val default_sort: Proof.context -> indexname -> sort
val consts_of: Proof.context -> Consts.T
val the_const_constraint: Proof.context -> string -> typ
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
@@ -127,6 +128,9 @@
Context.generic -> Context.generic
val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
+ val class_alias: binding -> class -> Proof.context -> Proof.context
+ val type_alias: binding -> string -> Proof.context -> Proof.context
+ val const_alias: binding -> string -> Proof.context -> Proof.context
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -249,6 +253,7 @@
val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
val tsig_of = #1 o #tsigs o rep_context;
+fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_context;
val the_const_constraint = Consts.the_constraint o consts_of;
@@ -473,7 +478,7 @@
in
if Syntax.is_tid c then
(Position.report Markup.tfree pos;
- TFree (c, the_default (Type.defaultS tsig) (Variable.def_sort ctxt (c, ~1))))
+ TFree (c, default_sort ctxt (c, ~1)))
else
let
val d = Type.intern_type tsig c;
@@ -745,7 +750,7 @@
val t =
Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
- handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
+ handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
in t end;
@@ -1011,7 +1016,7 @@
-(** parameters **)
+(** basic logical entities **)
(* variables *)
@@ -1043,7 +1048,7 @@
end;
-(* authentic logical entities *)
+(* authentic syntax *)
val _ = Context.>>
(Context.map_theory
@@ -1121,8 +1126,14 @@
in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
+end;
-end;
+
+(* aliases *)
+
+fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
+fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
+fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
(* local constants *)
--- a/src/Pure/consts.ML Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/consts.ML Tue Mar 09 23:29:04 2010 +0100
@@ -19,6 +19,7 @@
val is_monomorphic: T -> string -> bool (*exception TYPE*)
val the_constraint: T -> string -> typ (*exception TYPE*)
val space_of: T -> Name_Space.T
+ val alias: Name_Space.naming -> binding -> string -> T -> T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val extern: T -> string -> xstring
@@ -122,6 +123,9 @@
fun space_of (Consts {decls = (space, _), ...}) = space;
+fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
+ ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
+
val is_concealed = Name_Space.is_concealed o space_of;
val intern = Name_Space.intern o space_of;
--- a/src/Pure/sign.ML Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/sign.ML Tue Mar 09 23:29:04 2010 +0100
@@ -47,6 +47,9 @@
val class_space: theory -> Name_Space.T
val type_space: theory -> Name_Space.T
val const_space: theory -> Name_Space.T
+ val class_alias: binding -> class -> theory -> theory
+ val type_alias: binding -> string -> theory -> theory
+ val const_alias: binding -> string -> theory -> theory
val intern_class: theory -> xstring -> string
val extern_class: theory -> string -> xstring
val intern_type: theory -> xstring -> string
@@ -233,6 +236,10 @@
val type_space = Type.type_space o tsig_of;
val const_space = Consts.space_of o consts_of;
+fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
+fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
+fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
+
val intern_class = Name_Space.intern o class_space;
val extern_class = Name_Space.extern o class_space;
val intern_type = Name_Space.intern o type_space;
--- a/src/Pure/type.ML Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/type.ML Tue Mar 09 23:29:04 2010 +0100
@@ -21,6 +21,7 @@
log_types: string list}
val empty_tsig: tsig
val class_space: tsig -> Name_Space.T
+ val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
val intern_class: tsig -> xstring -> string
val extern_class: tsig -> string -> xstring
val defaultS: tsig -> sort
@@ -40,6 +41,7 @@
val set_mode: mode -> Proof.context -> Proof.context
val restore_mode: Proof.context -> Proof.context -> Proof.context
val type_space: tsig -> Name_Space.T
+ val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
val intern_type: tsig -> xstring -> string
val extern_type: tsig -> string -> xstring
val is_logtype: tsig -> string -> bool
@@ -141,6 +143,9 @@
val class_space = #1 o #classes o rep_tsig;
+fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
+ ((Name_Space.alias naming binding name space, classes), default, types));
+
val intern_class = Name_Space.intern o class_space;
val extern_class = Name_Space.extern o class_space;
@@ -182,6 +187,9 @@
val type_space = #1 o #types o rep_tsig;
+fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
+ (classes, default, (Name_Space.alias naming binding name space, types)));
+
val intern_type = Name_Space.intern o type_space;
val extern_type = Name_Space.extern o type_space;