--- a/NEWS Wed Mar 10 08:04:39 2010 +0100
+++ b/NEWS Wed Mar 10 08:04:50 2010 +0100
@@ -76,6 +76,10 @@
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).
+* Command 'typedecl' now works within a local theory context --
+without introducing dependencies on parameters or assumptions, which
+is not possible in Isabelle/Pure.
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Spec.thy Wed Mar 10 08:04:39 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed Mar 10 08:04:50 2010 +0100
@@ -954,7 +954,7 @@
text {*
\begin{matharray}{rcll}
@{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Mar 10 08:04:39 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Mar 10 08:04:50 2010 +0100
@@ -991,7 +991,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcll}
\indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\end{matharray}
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Wed Mar 10 08:04:50 2010 +0100
@@ -88,7 +88,7 @@
let
val args = Name.variant_list [] (replicate arity "'")
val (T, thy') =
- Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
+ Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
val type_name = fst (Term.dest_Type T)
in (((name, type_name), log_new name type_name), thy') end)
end
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 10 08:04:50 2010 +0100
@@ -58,7 +58,7 @@
val goal = List.nth(prems_of thm, i-1);
val ps = Logic.strip_params goal;
val Ts = rev (map snd ps);
- fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]);
+ fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
(* rebuild de bruijn indices *)
val bvs = map_index (Bound o fst) ps;
(* select variables of the right class *)
--- a/src/HOL/Tools/TFL/tfl.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Mar 10 08:04:50 2010 +0100
@@ -360,7 +360,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
-fun mk_const_def sign (c, Ty, rhs) =
+fun legacy_const_def sign (c, Ty, rhs) =
singleton (Syntax.check_terms (ProofContext.init sign))
(Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
@@ -385,7 +385,7 @@
val wfrec_R_M = map_types poly_tvars
(wfrec $ map_types poly_tvars R)
$ functional
- val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
+ val def_term = legacy_const_def thy (x, Ty, wfrec_R_M)
val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (thy', def) end;
end;
@@ -540,7 +540,7 @@
val {lhs,rhs} = S.dest_eq proto_def'
val (c,args) = S.strip_comb lhs
val (name,Ty) = dest_atom c
- val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+ val defn = legacy_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
|> PureThy.add_defs false
--- a/src/HOL/Tools/typedef.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Wed Mar 10 08:04:50 2010 +0100
@@ -130,7 +130,7 @@
in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
fun typedef_result inhabited =
- Typedecl.typedecl (tname, vs, mx)
+ Typedecl.typedecl_global (tname, vs, mx)
#> snd
#> Sign.add_consts_i
[(Rep_name, newT --> oldT, NoSyn),
--- a/src/Pure/General/name_space.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 10 08:04:50 2010 +0100
@@ -47,6 +47,7 @@
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
val declare: bool -> naming -> binding -> T -> string * T
+ val alias: naming -> binding -> string -> T -> T
type 'a table = T * 'a Symtab.table
val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
val empty_table: string -> 'a table
@@ -72,8 +73,7 @@
(* datatype entry *)
type entry =
- {externals: xstring list,
- concealed: bool,
+ {concealed: bool,
group: serial option,
theory_name: string,
pos: Position.T,
@@ -96,7 +96,7 @@
Name_Space of
{kind: string,
internals: (string list * string list) Symtab.table, (*visible, hidden*)
- entries: entry Symtab.table};
+ entries: (xstring list * entry) Symtab.table}; (*externals, entry*)
fun make_name_space (kind, internals, entries) =
Name_Space {kind = kind, internals = internals, entries = entries};
@@ -115,8 +115,7 @@
fun the_entry (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
- | SOME {concealed, group, theory_name, pos, id, ...} =>
- {concealed = concealed, group = group, theory_name = theory_name, pos = pos, id = id});
+ | SOME (_, entry) => entry);
fun is_concealed space name = #concealed (the_entry space name);
@@ -134,7 +133,7 @@
fun get_accesses (Name_Space {entries, ...}) name =
(case Symtab.lookup entries name of
NONE => [name]
- | SOME {externals, ...} => externals);
+ | SOME (externals, _) => externals);
fun valid_accesses (Name_Space {internals, ...}) name =
Symtab.fold (fn (xname, (names, _)) =>
@@ -212,7 +211,7 @@
then raise Symtab.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
val entries' = (entries1, entries2) |> Symtab.join
- (fn name => fn (entry1, entry2) =>
+ (fn name => fn ((_, entry1), (_, entry2)) =>
if #id entry1 = #id entry2 then raise Symtab.SAME
else err_dup kind' (name, entry1) (name, entry2));
in make_name_space (kind', internals', entries') end;
@@ -311,13 +310,13 @@
(* declaration *)
-fun new_entry strict entry =
+fun new_entry strict (name, (externals, entry)) =
map_name_space (fn (kind, internals, entries) =>
let
val entries' =
- (if strict then Symtab.update_new else Symtab.update) entry entries
+ (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
handle Symtab.DUP dup =>
- err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+ err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
in (kind, internals, entries') end);
fun declare strict naming binding space =
@@ -330,16 +329,35 @@
val _ = name = "" andalso err_bad binding;
val entry =
- {externals = accs',
- concealed = concealed,
+ {concealed = concealed,
group = group,
theory_name = theory_name,
pos = Position.default (Binding.pos_of binding),
id = serial ()};
- val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
+ val space' = space
+ |> fold (add_name name) accs
+ |> new_entry strict (name, (accs', entry));
in (name, space') end;
+(* alias *)
+
+fun alias naming binding name space =
+ let
+ val (accs, accs') = accesses naming binding;
+ val space' = space
+ |> fold (add_name name) accs
+ |> map_name_space (fn (kind, internals, entries) =>
+ let
+ val _ = Symtab.defined entries name orelse
+ error ("Undefined " ^ kind ^ " " ^ quote name);
+ val entries' = entries
+ |> Symtab.map_entry name (fn (externals, entry) =>
+ (Library.merge (op =) (externals, accs'), entry))
+ in (kind, internals, entries') end);
+ in space' end;
+
+
(** name spaces coupled with symbol tables **)
--- a/src/Pure/Isar/class.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/class.ML Wed Mar 10 08:04:50 2010 +0100
@@ -338,7 +338,7 @@
val subclass = gen_subclass (K I) user_proof;
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
-val subclass_cmd = gen_subclass Sign.read_class user_proof;
+val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
end; (*local*)
--- a/src/Pure/Isar/class_target.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/class_target.ML Wed Mar 10 08:04:50 2010 +0100
@@ -417,7 +417,8 @@
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
let
- val all_arities = map (fn raw_tyco => Sign.read_arity thy
+ val ctxt = ProofContext.init thy;
+ val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
val (_, sorts, sort) = hd all_arities;
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 10 08:04:50 2010 +0100
@@ -103,16 +103,15 @@
(* types *)
val _ =
- OuterSyntax.command "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
- Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
+ OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
+ (P.type_args -- P.binding -- P.opt_mixfix
+ >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
(P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
- >> (Toplevel.theory o Sign.add_tyabbrs o
- map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+ >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val _ =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
--- a/src/Pure/Isar/proof_context.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 10 08:04:50 2010 +0100
@@ -27,6 +27,8 @@
val restore_naming: Proof.context -> Proof.context -> Proof.context
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
@@ -41,6 +43,9 @@
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
+ val read_class: Proof.context -> xstring -> class
+ val read_arity: Proof.context -> xstring * string list * string -> arity
+ val cert_arity: Proof.context -> arity -> arity
val read_typ: Proof.context -> string -> typ
val read_typ_syntax: Proof.context -> string -> typ
val read_typ_abbrev: Proof.context -> string -> typ
@@ -53,6 +58,7 @@
val inferred_param: string -> Proof.context -> typ * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
val read_type_name: Proof.context -> bool -> string -> typ
+ val read_type_name_proper: Proof.context -> bool -> string -> typ
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> string -> term
val allow_dummies: Proof.context -> Proof.context
@@ -122,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
@@ -167,16 +176,17 @@
datatype ctxt =
Ctxt of
- {mode: mode, (*inner syntax mode*)
- naming: Name_Space.naming, (*local naming conventions*)
- syntax: Local_Syntax.T, (*local syntax*)
- consts: Consts.T * Consts.T, (*local/global consts*)
- facts: Facts.T, (*local facts*)
+ {mode: mode, (*inner syntax mode*)
+ naming: Name_Space.naming, (*local naming conventions*)
+ syntax: Local_Syntax.T, (*local syntax*)
+ tsigs: Type.tsig * Type.tsig, (*local/global type signature -- local name space only*)
+ consts: Consts.T * Consts.T, (*local/global consts -- local name space/abbrevs only*)
+ facts: Facts.T, (*local facts*)
cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*)
-fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
+fun make_ctxt (mode, naming, syntax, tsigs, consts, facts, cases) =
Ctxt {mode = mode, naming = naming, syntax = syntax,
- consts = consts, facts = facts, cases = cases};
+ tsigs = tsigs, consts = consts, facts = facts, cases = cases};
val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
@@ -185,41 +195,46 @@
type T = ctxt;
fun init thy =
make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
+ (Sign.tsig_of thy, Sign.tsig_of thy),
(Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
);
fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
fun map_context f =
- ContextData.map (fn Ctxt {mode, naming, syntax, consts, facts, cases} =>
- make_ctxt (f (mode, naming, syntax, consts, facts, cases)));
+ ContextData.map (fn Ctxt {mode, naming, syntax, tsigs, consts, facts, cases} =>
+ make_ctxt (f (mode, naming, syntax, tsigs, consts, facts, cases)));
-fun set_mode mode = map_context (fn (_, naming, syntax, consts, facts, cases) =>
- (mode, naming, syntax, consts, facts, cases));
+fun set_mode mode = map_context (fn (_, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, syntax, tsigs, consts, facts, cases));
fun map_mode f =
- map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, facts, cases) =>
- (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, facts, cases));
+ map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsigs, consts, facts, cases) =>
+ (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsigs, consts, facts, cases));
fun map_naming f =
- map_context (fn (mode, naming, syntax, consts, facts, cases) =>
- (mode, f naming, syntax, consts, facts, cases));
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, f naming, syntax, tsigs, consts, facts, cases));
fun map_syntax f =
- map_context (fn (mode, naming, syntax, consts, facts, cases) =>
- (mode, naming, f syntax, consts, facts, cases));
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, f syntax, tsigs, consts, facts, cases));
+
+fun map_tsigs f =
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, syntax, f tsigs, consts, facts, cases));
fun map_consts f =
- map_context (fn (mode, naming, syntax, consts, facts, cases) =>
- (mode, naming, syntax, f consts, facts, cases));
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, syntax, tsigs, f consts, facts, cases));
fun map_facts f =
- map_context (fn (mode, naming, syntax, consts, facts, cases) =>
- (mode, naming, syntax, consts, f facts, cases));
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, syntax, tsigs, consts, f facts, cases));
fun map_cases f =
- map_context (fn (mode, naming, syntax, consts, facts, cases) =>
- (mode, naming, syntax, consts, facts, f cases));
+ map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+ (mode, naming, syntax, tsigs, consts, facts, f cases));
val get_mode = #mode o rep_context;
val restore_mode = set_mode o get_mode;
@@ -237,6 +252,9 @@
val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
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;
@@ -246,8 +264,13 @@
(* theory transfer *)
-fun transfer_syntax thy =
- map_syntax (Local_Syntax.rebuild thy) #>
+fun transfer_syntax thy ctxt = ctxt |>
+ map_syntax (Local_Syntax.rebuild thy) |>
+ map_tsigs (fn tsigs as (local_tsig, global_tsig) =>
+ let val thy_tsig = Sign.tsig_of thy in
+ if Type.eq_tsig (thy_tsig, global_tsig) then tsigs
+ else (Type.merge_tsigs (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+ end) |>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
if Consts.eq_consts (thy_consts, global_consts) then consts
@@ -299,23 +322,49 @@
(** prepare types **)
-(* read_typ *)
+(* classes *)
+
+fun read_class ctxt text =
+ let
+ val tsig = tsig_of ctxt;
+ val (syms, pos) = Syntax.read_token text;
+ val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+ handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
+ val _ = Position.report (Markup.tclass c) pos;
+ in c end;
+
+
+(* type arities *)
+
+local
+
+fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
+ let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
+ in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+
+in
+
+val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
+val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
+
+end;
+
+
+(* types *)
fun read_typ_mode mode ctxt s =
Syntax.read_typ (Type.set_mode mode ctxt) s;
-val read_typ = read_typ_mode Type.mode_default;
+val read_typ = read_typ_mode Type.mode_default;
val read_typ_syntax = read_typ_mode Type.mode_syntax;
val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
-(* cert_typ *)
-
fun cert_typ_mode mode ctxt T =
- Sign.certify_typ_mode mode (theory_of ctxt) T
+ Type.cert_typ_mode mode (tsig_of ctxt) T
handle TYPE (msg, _, _) => error msg;
-val cert_typ = cert_typ_mode Type.mode_default;
+val cert_typ = cert_typ_mode Type.mode_default;
val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
@@ -424,16 +473,16 @@
fun read_type_name ctxt strict text =
let
- val thy = theory_of ctxt;
+ val tsig = tsig_of ctxt;
val (c, pos) = token_content text;
in
if Syntax.is_tid c then
(Position.report Markup.tfree pos;
- TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
+ TFree (c, default_sort ctxt (c, ~1)))
else
let
- val d = Sign.intern_type thy c;
- val decl = Sign.the_type_decl thy d;
+ val d = Type.intern_type tsig c;
+ val decl = Type.the_decl tsig d;
val _ = Position.report (Markup.tycon d) pos;
fun err () = error ("Bad type name: " ^ quote d);
val args =
@@ -444,6 +493,12 @@
in Type (d, replicate args dummyT) end
end;
+fun read_type_name_proper ctxt strict text =
+ (case read_type_name ctxt strict text of
+ T as Type _ => T
+ | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+
+
fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
fun read_const ctxt strict text =
@@ -470,8 +525,6 @@
(* local abbreviations *)
-val tsig_of = Sign.tsig_of o ProofContext.theory_of;
-
local
fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
@@ -553,9 +606,9 @@
(* types *)
-fun get_sort thy def_sort raw_env =
+fun get_sort ctxt def_sort raw_env =
let
- val tsig = Sign.tsig_of thy;
+ val tsig = tsig_of ctxt;
fun eq ((xi, S), (xi', S')) =
Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
@@ -571,8 +624,8 @@
| (SOME S, NONE) => S
| (SOME S, SOME S') =>
if Type.eq_sort tsig (S, S') then S'
- else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^
- " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^
+ else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
+ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
" for type variable " ^ quote (Term.string_of_vname' xi)));
in get end;
@@ -594,12 +647,10 @@
in
fun term_context ctxt =
- let val thy = theory_of ctxt in
- {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)}
- end;
+ {get_sort = get_sort ctxt (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)};
fun decode_term ctxt =
let val {get_sort, map_const, map_free} = term_context ctxt
@@ -680,8 +731,7 @@
fun parse_typ ctxt text =
let
- val thy = theory_of ctxt;
- val get_sort = get_sort thy (Variable.def_sort ctxt);
+ val get_sort = get_sort ctxt (Variable.def_sort ctxt);
val (syms, pos) = Syntax.parse_token Markup.typ text;
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);
@@ -689,7 +739,6 @@
fun parse_term T ctxt text =
let
- val thy = theory_of ctxt;
val {get_sort, map_const, map_free} = term_context ctxt;
val (T', _) = TypeInfer.paramify_dummies T 0;
@@ -700,33 +749,33 @@
handle ERROR msg => SOME msg;
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);
+ 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);
in t end;
fun unparse_sort ctxt =
- Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+ Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
ctxt (syn_of ctxt);
fun unparse_typ ctxt =
let
- val thy = theory_of ctxt;
- val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+ val tsig = tsig_of ctxt;
+ val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
fun unparse_term ctxt =
let
- val thy = theory_of ctxt;
+ val tsig = tsig_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_class = Type.extern_class tsig,
+ 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 (PureThy.old_appl_syntax thy))
+ (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
end;
in
@@ -967,7 +1016,7 @@
-(** parameters **)
+(** basic logical entities **)
(* variables *)
@@ -999,7 +1048,14 @@
end;
-(* authentic constants *)
+(* authentic syntax *)
+
+val _ = Context.>>
+ (Context.map_theory
+ (Sign.add_advanced_trfuns
+ (Syntax.type_ast_trs
+ {read_class = read_class,
+ read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
local
@@ -1070,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/Isar/typedecl.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML Wed Mar 10 08:04:50 2010 +0100
@@ -6,26 +6,50 @@
signature TYPEDECL =
sig
- val typedecl: binding * string list * mixfix -> theory -> typ * theory
+ val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
+ val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
end;
structure Typedecl: TYPEDECL =
struct
-fun typedecl (b, vs, mx) thy =
+fun typedecl (b, vs, mx) lthy =
let
- val base_sort = Object_Logic.get_base_sort thy;
- val _ = has_duplicates (op =) vs andalso
- error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
- val name = Sign.full_name thy b;
+ fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
+ val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
+
+ val name = Local_Theory.full_name lthy b;
val n = length vs;
- val T = Type (name, map (fn v => TFree (v, [])) vs);
+ val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
+ val T = Type (name, args);
+
+ val bad_args =
+ #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
+ |> filter_out Term.is_TVar;
+ val _ = not (null bad_args) andalso
+ err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
+
+ val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
in
- thy
- |> Sign.add_types [(b, n, mx)]
- |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+ lthy
+ |> Local_Theory.theory
+ (Sign.add_types [(b, n, NoSyn)] #>
+ (case base_sort of
+ NONE => I
+ | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
+ |> Local_Theory.checkpoint
+ |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
+ |> Local_Theory.type_syntax false
+ (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+ |> ProofContext.type_alias b name
+ |> Variable.declare_typ T
|> pair T
end;
+fun typedecl_global decl =
+ Theory_Target.init NONE
+ #> typedecl decl
+ #> Local_Theory.exit_result_global Morphism.typ;
+
end;
--- a/src/Pure/ML/ml_antiquote.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 10 08:04:50 2010 +0100
@@ -102,8 +102,8 @@
(* type classes *)
-fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
- Sign.read_class thy s
+fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+ ProofContext.read_class ctxt s
|> syn ? Syntax.mark_class
|> ML_Syntax.print_string);
@@ -119,8 +119,8 @@
fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
>> (fn (ctxt, (s, pos)) =>
let
- val Type (c, _) = ProofContext.read_type_name ctxt false s;
- val decl = Sign.the_type_decl (ProofContext.theory_of ctxt) c;
+ val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
+ val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
val res =
(case try check (c, decl) of
SOME res => res
--- a/src/Pure/ROOT.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/ROOT.ML Wed Mar 10 08:04:50 2010 +0100
@@ -148,7 +148,6 @@
use "assumption.ML";
use "display.ML";
use "goal.ML";
-use "axclass.ML";
(* Isar -- Intelligible Semi-Automated Reasoning *)
@@ -209,6 +208,7 @@
use "Isar/local_theory.ML";
use "Isar/overloading.ML";
use "Isar/locale.ML";
+use "axclass.ML";
use "Isar/class_target.ML";
use "Isar/theory_target.ML";
use "Isar/expression.ML";
--- a/src/Pure/Syntax/syntax.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Mar 10 08:04:50 2010 +0100
@@ -29,10 +29,7 @@
val mode_default: mode
val mode_input: mode
val merge_syntaxes: syntax -> syntax -> syntax
- val empty_syntax: syntax
- val basic_syntax:
- {read_class: theory -> xstring -> string,
- read_type: theory -> xstring -> string} -> syntax
+ val basic_syntax: syntax
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -383,9 +380,9 @@
(* basic syntax *)
-fun basic_syntax read =
+val basic_syntax =
empty_syntax
- |> update_syntax mode_default (TypeExt.type_ext read)
+ |> update_syntax mode_default TypeExt.type_ext
|> update_syntax mode_default SynExt.pure_ext;
val basic_nonterms =
--- a/src/Pure/Syntax/type_ext.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML Wed Mar 10 08:04:50 2010 +0100
@@ -15,6 +15,10 @@
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
+ val type_ast_trs:
+ {read_class: Proof.context -> string -> string,
+ read_type: Proof.context -> string -> string} ->
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
end;
signature TYPE_EXT =
@@ -23,9 +27,7 @@
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val sortT: typ
- val type_ext:
- {read_class: theory -> string -> string,
- read_type: theory -> string -> string} -> SynExt.syn_ext
+ val type_ext: SynExt.syn_ext
end;
structure TypeExt: TYPE_EXT =
@@ -240,7 +242,7 @@
local open Lexicon SynExt in
-fun type_ext {read_class, read_type} = syn_ext' false (K false)
+val type_ext = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
Mfix ("_", idT --> typeT, "_type_name", [], max_pri),
@@ -267,19 +269,18 @@
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
["_type_prop"]
- (map SynExt.mk_trfun
- [("_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 [("\\<^type>fun", K fun_ast_tr')])
+ ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
+fun type_ast_trs {read_class, read_type} =
+ [("_class_name", class_name_tr o read_class),
+ ("_classes", classes_tr o read_class),
+ ("_type_name", type_name_tr o read_type),
+ ("_tapp", tapp_ast_tr o read_type),
+ ("_tappl", tappl_ast_tr o read_type),
+ ("_bracket", K bracket_ast_tr)];
+
end;
end;
--- a/src/Pure/axclass.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/axclass.ML Wed Mar 10 08:04:50 2010 +0100
@@ -280,7 +280,7 @@
in (c1, c2) end;
fun read_classrel thy raw_rel =
- cert_classrel thy (pairself (Sign.read_class thy) raw_rel)
+ cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
handle TYPE (msg, _, _) => error msg;
@@ -387,7 +387,7 @@
fun prove_arity raw_arity tac thy =
let
val ctxt = ProofContext.init thy;
- val arity = Sign.cert_arity thy raw_arity;
+ val arity = ProofContext.cert_arity ctxt raw_arity;
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
val ths = Goal.prove_multi ctxt [] [] props
@@ -530,7 +530,7 @@
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
fun ax_arity prep =
- axiomatize prep Logic.mk_arities
+ axiomatize (prep o ProofContext.init) Logic.mk_arities
(map (prefix arity_prefix) o Logic.name_arities) add_arity;
fun class_const c =
@@ -550,11 +550,11 @@
in
val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
+val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
val axiomatize_classrel = ax_classrel cert_classrel;
val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity Sign.cert_arity;
-val axiomatize_arity_cmd = ax_arity Sign.read_arity;
+val axiomatize_arity = ax_arity ProofContext.cert_arity;
+val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
end;
--- a/src/Pure/consts.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/consts.ML Wed Mar 10 08:04:50 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 Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/sign.ML Wed Mar 10 08:04:50 2010 +0100
@@ -47,17 +47,16 @@
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
val extern_type: theory -> string -> xstring
val intern_const: theory -> xstring -> string
val extern_const: theory -> string -> xstring
- val intern_sort: theory -> sort -> sort
- val extern_sort: theory -> sort -> sort
- val intern_typ: theory -> typ -> typ
val intern_term: theory -> term -> term
- val the_type_decl: theory -> string -> Type.decl
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
val certify_class: theory -> class -> class
@@ -71,9 +70,6 @@
val no_frees: Pretty.pp -> term -> term
val no_vars: Pretty.pp -> term -> term
val cert_def: Proof.context -> term -> (string * typ) * term
- val read_class: theory -> xstring -> class
- val read_arity: theory -> xstring * string list * string -> arity
- val cert_arity: theory -> arity -> arity
val add_defsort: string -> theory -> theory
val add_defsort_i: sort -> theory -> theory
val add_types: (binding * int * mixfix) list -> theory -> theory
@@ -154,7 +150,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
@@ -236,10 +232,14 @@
(** intern / extern names **)
-val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
-val type_space = #1 o #types o Type.rep_tsig o tsig_of;
+val class_space = Type.class_space o tsig_of;
+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;
@@ -247,9 +247,6 @@
val intern_const = Name_Space.intern o const_space;
val extern_const = Name_Space.extern o const_space;
-val intern_sort = map o intern_class;
-val extern_sort = map o extern_class;
-
local
fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
@@ -265,7 +262,6 @@
in
-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;
@@ -276,7 +272,6 @@
(* certify wrt. type signature *)
-val the_type_decl = Type.the_decl o tsig_of;
val arity_number = Type.arity_number o tsig_of;
fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
@@ -367,51 +362,6 @@
-(** read and certify entities **) (*exception ERROR*)
-
-(* classes *)
-
-fun read_class thy text =
- let
- val (syms, pos) = Syntax.read_token text;
- val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
- handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
- val _ = Position.report (Markup.tclass c) pos;
- in c end;
-
-
-(* type arities *)
-
-fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
- let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
- in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
-
-val read_arity = prep_arity intern_type Syntax.read_sort_global;
-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*)
(* add default sort *)
--- a/src/Pure/type.ML Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/type.ML Wed Mar 10 08:04:50 2010 +0100
@@ -13,12 +13,17 @@
Abbreviation of string list * typ * bool |
Nonterminal
type tsig
+ val eq_tsig: tsig * tsig -> bool
val rep_tsig: tsig ->
{classes: Name_Space.T * Sorts.algebra,
default: sort,
types: decl Name_Space.table,
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
val logical_types: tsig -> string list
val eq_sort: tsig -> sort * sort -> bool
@@ -35,6 +40,11 @@
val get_mode: Proof.context -> mode
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
val the_decl: tsig -> string -> decl
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
@@ -103,6 +113,13 @@
types: decl Name_Space.table, (*declared types*)
log_types: string list}; (*logical types sorted by number of arguments*)
+fun eq_tsig
+ (TSig {classes = classes1, default = default1, types = types1, log_types = _},
+ TSig {classes = classes2, default = default2, types = types2, log_types = _}) =
+ pointer_eq (classes1, classes2) andalso
+ default1 = default2 andalso
+ pointer_eq (types1, types2);
+
fun rep_tsig (TSig comps) = comps;
fun make_tsig (classes, default, types, log_types) =
@@ -124,6 +141,14 @@
(* classes and sorts *)
+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;
+
fun defaultS (TSig {default, ...}) = default;
fun logical_types (TSig {log_types, ...}) = log_types;
@@ -158,7 +183,18 @@
fun restore_mode ctxt = set_mode (get_mode ctxt);
-(* lookup types *)
+(* types *)
+
+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;
+
+val is_logtype = member (op =) o logical_types;
+
fun undecl_type c = "Undeclared type constructor: " ^ quote c;