maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;
--- a/src/Pure/General/name_space.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/General/name_space.ML Sun Mar 18 13:04:22 2012 +0100
@@ -34,7 +34,6 @@
val hide: bool -> string -> T -> T
val merge: T * T -> T
type naming
- val default_naming: naming
val conceal: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
@@ -46,14 +45,18 @@
val parent_path: naming -> naming
val mandatory_path: string -> naming -> naming
val qualified_path: bool -> binding -> naming -> naming
+ val default_naming: naming
+ val local_naming: naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
val alias: naming -> binding -> string -> T -> T
- val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
+ val naming_of: Context.generic -> naming
+ val map_naming: (naming -> naming) -> Context.generic -> Context.generic
+ val declare: Context.generic -> bool -> binding -> T -> string * T
type 'a table = T * 'a Symtab.table
- val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
+ val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
val get: 'a table -> string -> 'a
- val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
+ val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
val empty_table: string -> 'a table
val merge_tables: 'a table * 'a table -> 'a table
val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
@@ -240,7 +243,7 @@
-(** naming contexts **)
+(** naming context **)
(* datatype naming *)
@@ -260,8 +263,6 @@
(conceal, group, theory_name, f path));
-val default_naming = make_naming (false, NONE, "", []);
-
val conceal = map_naming (fn (_, group, theory_name, path) =>
(true, group, theory_name, path));
@@ -285,6 +286,9 @@
fun qualified_path mandatory binding = map_path (fn path =>
path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
+val default_naming = make_naming (false, NONE, "", []);
+val local_naming = default_naming |> add_path "local";
+
(* full name *)
@@ -348,6 +352,28 @@
+(** context naming **)
+
+structure Data_Args =
+struct
+ type T = naming;
+ val empty = default_naming;
+ fun extend _ = default_naming;
+ fun merge _ = default_naming;
+ fun init _ = local_naming;
+end;
+
+structure Global_Naming = Theory_Data(Data_Args);
+structure Local_Naming = Proof_Data(Data_Args);
+
+fun naming_of (Context.Theory thy) = Global_Naming.get thy
+ | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;
+
+fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)
+ | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);
+
+
+
(** entry definition **)
(* declaration *)
@@ -361,8 +387,9 @@
err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
in (kind, internals, entries') end);
-fun declare ctxt strict naming binding space =
+fun declare context strict binding space =
let
+ val naming = naming_of context;
val Naming {group, theory_name, ...} = naming;
val (concealed, spec) = name_spec naming binding;
val (accs, accs') = accesses naming binding;
@@ -380,7 +407,9 @@
val space' = space
|> fold (add_name name) accs
|> new_entry strict (name, (accs', entry));
- val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
+ val _ =
+ Context_Position.report_generic context pos
+ (entry_markup true (kind_of space) (name, entry));
in (name, space') end;
@@ -388,10 +417,10 @@
type 'a table = T * 'a Symtab.table;
-fun check ctxt (space, tab) (xname, pos) =
+fun check context (space, tab) (xname, pos) =
let val name = intern space xname in
(case Symtab.lookup tab name of
- SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
+ SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
| NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
end;
@@ -400,8 +429,8 @@
SOME x => x
| NONE => error (undefined (kind_of space) name));
-fun define ctxt strict naming (binding, x) (space, tab) =
- let val (name, space') = declare ctxt strict naming binding space
+fun define context strict (binding, x) (space, tab) =
+ let val (name, space') = declare context strict binding space
in (name, (space', Symtab.update (name, x) tab)) end;
fun empty_table kind = (empty kind, Symtab.empty);
--- a/src/Pure/Isar/attrib.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Mar 18 13:04:22 2012 +0100
@@ -92,9 +92,7 @@
end;
fun add_attribute name att comment thy = thy
- |> Attributes.map
- (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
- (name, (att, comment)) #> snd);
+ |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
(* name space *)
--- a/src/Pure/Isar/class.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/class.ML Sun Mar 18 13:04:22 2012 +0100
@@ -282,7 +282,7 @@
| _ => NONE)
| NONE => NONE)
| NONE => NONE);
- fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
+ fun subst (c, _) = Option.map snd (AList.lookup (op =) operations c);
val unchecks = these_unchecks thy sort;
in
ctxt
@@ -470,7 +470,7 @@
fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
| matchings _ = I;
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
@@ -522,7 +522,7 @@
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
val algebra = Sign.classes_of thy
- |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
+ |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
--- a/src/Pure/Isar/locale.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/locale.ML Sun Mar 18 13:04:22 2012 +0100
@@ -163,7 +163,7 @@
);
val intern = Name_Space.intern o #1 o Locales.get;
-fun check thy = #1 o Name_Space.check (Proof_Context.init_global thy) (Locales.get thy);
+fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
val get_locale = Symtab.lookup o #2 o Locales.get;
@@ -175,7 +175,7 @@
| NONE => error ("Unknown locale " ^ quote name));
fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
- thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
+ thy |> Locales.map (Name_Space.define (Context.Theory thy) true
(binding,
mk_locale ((parameters, spec, intros, axioms),
((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
--- a/src/Pure/Isar/method.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/method.ML Sun Mar 18 13:04:22 2012 +0100
@@ -326,9 +326,7 @@
end;
fun add_method name meth comment thy = thy
- |> Methods.map
- (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
- (name, (meth, comment)) #> snd);
+ |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
(* get methods *)
--- a/src/Pure/Isar/proof.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/proof.ML Sun Mar 18 13:04:22 2012 +0100
@@ -165,7 +165,7 @@
val init_context =
Proof_Context.set_stmt true #>
- Proof_Context.map_naming (K Proof_Context.local_naming);
+ Proof_Context.map_naming (K Name_Space.local_naming);
fun init ctxt =
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
--- a/src/Pure/Isar/proof_context.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 18 13:04:22 2012 +0100
@@ -21,11 +21,6 @@
val restore_mode: Proof.context -> Proof.context -> Proof.context
val abbrev_mode: Proof.context -> bool
val set_stmt: bool -> Proof.context -> Proof.context
- val local_naming: Name_Space.naming
- val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
- val naming_of: Proof.context -> Name_Space.naming
- val restore_naming: Proof.context -> Proof.context -> Proof.context
- val full_name: Proof.context -> binding -> string
val syntax_of: Proof.context -> Local_Syntax.T
val syn_of: Proof.context -> Syntax.syntax
val tsig_of: Proof.context -> Type.tsig
@@ -37,6 +32,10 @@
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
+ val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
+ val naming_of: Proof.context -> Name_Space.naming
+ val restore_naming: Proof.context -> Proof.context -> Proof.context
+ val full_name: Proof.context -> binding -> string
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
@@ -141,7 +140,6 @@
Context.generic -> Context.generic
val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
- val target_naming_of: Context.generic -> Name_Space.naming
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
@@ -192,24 +190,20 @@
datatype data =
Data of
{mode: mode, (*inner syntax mode*)
- naming: Name_Space.naming, (*local naming conventions*)
syntax: Local_Syntax.T, (*local syntax*)
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort 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_data (mode, naming, syntax, tsig, consts, facts, cases) =
- Data {mode = mode, naming = naming, syntax = syntax,
- tsig = tsig, consts = consts, facts = facts, cases = cases};
-
-val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
+fun make_data (mode, syntax, tsig, consts, facts, cases) =
+ Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
structure Data = Proof_Data
(
type T = data;
fun init thy =
- make_data (mode_default, local_naming, Local_Syntax.init thy,
+ make_data (mode_default, Local_Syntax.init thy,
(Sign.tsig_of thy, Sign.tsig_of thy),
(Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
);
@@ -217,39 +211,35 @@
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
fun map_data f =
- Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} =>
- make_data (f (mode, naming, syntax, tsig, consts, facts, cases)));
+ Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} =>
+ make_data (f (mode, syntax, tsig, consts, facts, cases)));
-fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, syntax, tsig, consts, facts, cases));
+fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
+ (mode, syntax, tsig, consts, facts, cases));
fun map_mode f =
- map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
- (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
-
-fun map_naming f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, f naming, syntax, tsig, consts, facts, cases));
+ map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
+ (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
fun map_syntax f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, f syntax, tsig, consts, facts, cases));
+ map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+ (mode, f syntax, tsig, consts, facts, cases));
fun map_tsig f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, syntax, f tsig, consts, facts, cases));
+ map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+ (mode, syntax, f tsig, consts, facts, cases));
fun map_consts f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, syntax, tsig, f consts, facts, cases));
+ map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+ (mode, syntax, tsig, f consts, facts, cases));
fun map_facts f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, syntax, tsig, consts, f facts, cases));
+ map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+ (mode, syntax, tsig, consts, f facts, cases));
fun map_cases f =
- map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
- (mode, naming, syntax, tsig, consts, facts, f cases));
+ map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+ (mode, syntax, tsig, consts, facts, f cases));
val get_mode = #mode o rep_data;
val restore_mode = set_mode o get_mode;
@@ -258,10 +248,6 @@
fun set_stmt stmt =
map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
-val naming_of = #naming o rep_data;
-val restore_naming = map_naming o K o naming_of
-val full_name = Name_Space.full_name o naming_of;
-
val syntax_of = #syntax o rep_data;
val syn_of = Local_Syntax.syn_of o syntax_of;
val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
@@ -278,6 +264,15 @@
val cases_of = #cases o rep_data;
+(* naming *)
+
+val naming_of = Name_Space.naming_of o Context.Proof;
+val map_naming = Context.proof_map o Name_Space.map_naming;
+val restore_naming = map_naming o K o naming_of;
+
+val full_name = Name_Space.full_name o naming_of;
+
+
(* name spaces *)
val class_space = Type.class_space o tsig_of;
@@ -300,7 +295,7 @@
map_tsig (fn tsig as (local_tsig, global_tsig) =>
let val thy_tsig = Sign.tsig_of thy in
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
- else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
+ else (Type.merge_tsig (Context.pretty 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
@@ -495,12 +490,13 @@
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 ctxt arity (tsig_of ctxt); arity end;
+ in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
in
val read_arity =
prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+
val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
end;
@@ -892,7 +888,7 @@
fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
| update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
- (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
+ (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
in
@@ -908,7 +904,7 @@
in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
fun put_thms do_props thms ctxt = ctxt
- |> map_naming (K local_naming)
+ |> map_naming (K Name_Space.local_naming)
|> Context_Position.set_visible false
|> update_thms do_props (apfst Binding.name thms)
|> Context_Position.restore_visible ctxt
@@ -993,11 +989,6 @@
end;
-(* naming *)
-
-val target_naming_of = Context.cases Sign.naming_of naming_of;
-
-
(* aliases *)
fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
@@ -1020,7 +1011,7 @@
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
val ((lhs, rhs), consts') = consts_of ctxt
- |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
+ |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
in
ctxt
|> (map_consts o apfst) (K consts')
--- a/src/Pure/Isar/typedecl.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/typedecl.ML Sun Mar 18 13:04:22 2012 +0100
@@ -41,7 +41,7 @@
end;
fun basic_typedecl (b, n, mx) lthy =
- basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
+ basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
(b, n, mx) lthy;
--- a/src/Pure/ML/ml_context.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/ML/ml_context.ML Sun Mar 18 13:04:22 2012 +0100
@@ -109,9 +109,7 @@
);
fun add_antiq name scan thy = thy
- |> Antiq_Parsers.map
- (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
- (name, scan) #> snd);
+ |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
@@ -120,7 +118,7 @@
let
val thy = Proof_Context.theory_of ctxt;
val ((xname, _), pos) = Args.dest_src src;
- val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
+ val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
--- a/src/Pure/Thy/thy_output.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 18 13:04:22 2012 +0100
@@ -89,17 +89,11 @@
Name_Space.merge_tables (options1, options2));
);
-fun add_command name cmd thy =
- thy |> Antiquotations.map
- (apfst
- (Name_Space.define
- (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
+fun add_command name cmd thy = thy
+ |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
-fun add_option name opt thy =
- thy |> Antiquotations.map
- (apsnd
- (Name_Space.define
- (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
+fun add_option name opt thy = thy
+ |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
@@ -111,7 +105,7 @@
let
val thy = Proof_Context.theory_of ctxt;
val ((xname, _), pos) = Args.dest_src src;
- val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
+ val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
in
f src state ctxt handle ERROR msg =>
cat_error msg ("The error(s) above occurred in document antiquotation: " ^
@@ -121,7 +115,7 @@
fun option ((xname, pos), s) ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
+ val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
in opt s ctxt end;
fun print_antiquotations ctxt =
--- a/src/Pure/consts.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/consts.ML Sun Mar 18 13:04:22 2012 +0100
@@ -29,10 +29,9 @@
val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
+ val declare: Context.generic -> binding * typ -> T -> T
val constrain: string * typ option -> T -> T
- val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
- binding * term -> T -> (term * term) * T
+ val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T
val revert_abbrev: string -> string -> T -> T
val hide: bool -> string -> T -> T
val empty: T
@@ -232,12 +231,12 @@
(* declarations *)
-fun declare ctxt naming (b, declT) =
+fun declare context (b, declT) =
map_consts (fn (decls, constraints, rev_abbrevs) =>
let
val decl = {T = declT, typargs = typargs_of declT};
val _ = Binding.check b;
- val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
+ val (_, decls') = decls |> Name_Space.define context true (b, (decl, NONE));
in (decls', constraints, rev_abbrevs) end);
@@ -268,9 +267,9 @@
in
-fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
+fun abbreviate context tsig mode (b, raw_rhs) consts =
let
- val pp = Context.pretty ctxt;
+ val pp = Context.pretty_generic context;
val cert_term = certify pp tsig false consts;
val expand_term = certify pp tsig true consts;
val force_expand = mode = Print_Mode.internal;
@@ -284,7 +283,7 @@
|> Term.close_schematic_term;
val normal_rhs = expand_term rhs;
val T = Term.fastype_of rhs;
- val lhs = Const (Name_Space.full_name naming b, T);
+ val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T);
in
consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
let
@@ -292,7 +291,7 @@
val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
val _ = Binding.check b;
val (_, decls') = decls
- |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
+ |> Name_Space.define context true (b, (decl, SOME abbr));
val rev_abbrevs' = rev_abbrevs
|> update_abbrevs mode (rev_abbrev lhs rhs);
in (decls', constraints, rev_abbrevs') end)
--- a/src/Pure/context.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/context.ML Sun Mar 18 13:04:22 2012 +0100
@@ -76,6 +76,7 @@
(*pretty printing context*)
val pretty: Proof.context -> pretty
val pretty_global: theory -> pretty
+ val pretty_generic: generic -> pretty
val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
(*thread data*)
val thread_data: unit -> generic option
@@ -557,8 +558,9 @@
exception PRETTY of generic;
-val pretty = Pretty o PRETTY o Proof;
-val pretty_global = Pretty o PRETTY o Theory;
+val pretty_generic = Pretty o PRETTY;
+val pretty = pretty_generic o Proof;
+val pretty_global = pretty_generic o Theory;
fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
--- a/src/Pure/context_position.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/context_position.ML Sun Mar 18 13:04:22 2012 +0100
@@ -12,6 +12,7 @@
val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
val is_visible_proof: Context.generic -> bool
val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
+ val report_generic: Context.generic -> Position.T -> Markup.T -> unit
val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
val report: Proof.context -> Position.T -> Markup.T -> unit
@@ -33,6 +34,11 @@
fun if_visible_proof context f x = if is_visible_proof context then f x else ();
+fun report_generic context pos markup =
+ if Config.get_generic context visible then
+ Output.report (Position.reported_text pos markup "")
+ else ();
+
fun reported_text ctxt pos markup txt =
if is_visible ctxt then Position.reported_text pos markup txt else "";
--- a/src/Pure/display.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/display.ML Sun Mar 18 13:04:22 2012 +0100
@@ -185,7 +185,8 @@
val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
val defs = Theory.defs_of thy;
val {restricts, reducts} = Defs.dest defs;
- val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
+ val tsig = Sign.tsig_of thy;
+ val consts = Sign.consts_of thy;
val {constants, constraints} = Consts.dest consts;
val extern_const = Name_Space.extern ctxt (#1 constants);
val {classes, default, types, ...} = Type.rep_tsig tsig;
--- a/src/Pure/facts.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/facts.ML Sun Mar 18 13:04:22 2012 +0100
@@ -32,10 +32,9 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
- val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
- val add_dynamic: Proof.context -> Name_Space.naming ->
- binding * (Context.generic -> thm list) -> T -> string * T
+ val add_global: Context.generic -> binding * thm list -> T -> string * T
+ val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
+ val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
@@ -191,11 +190,11 @@
local
-fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
+fun add context strict do_props (b, ths) (Facts {facts, props}) =
let
val (name, facts') =
if Binding.is_empty b then ("", facts)
- else Name_Space.define ctxt strict naming (b, Static ths) facts;
+ else Name_Space.define context strict (b, Static ths) facts;
val props' =
if do_props
then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
@@ -204,16 +203,16 @@
in
-fun add_global ctxt = add ctxt true false;
-fun add_local ctxt = add ctxt false;
+fun add_global context = add context true false;
+fun add_local context = add context false;
end;
(* add dynamic entries *)
-fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
- let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
+fun add_dynamic context (b, f) (Facts {facts, props}) =
+ let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
in (name, make_facts facts' props) end;
--- a/src/Pure/global_theory.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/global_theory.ML Sun Mar 18 13:04:22 2012 +0100
@@ -156,13 +156,11 @@
then app_att thms thy |-> register_proofs
else
let
- val naming = Sign.naming_of thy;
- val name = Name_Space.full_name naming b;
+ val name = Sign.full_name thy b;
val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
val thms'' = map (Thm.transfer thy') thms';
val thy'' = thy'
- |> (Data.map o apfst)
- (Facts.add_global (Proof_Context.init_global thy') naming (b, thms'') #> snd);
+ |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
in (thms'', thy'') end;
@@ -196,8 +194,7 @@
(* add_thms_dynamic *)
fun add_thms_dynamic (b, f) thy = thy
- |> (Data.map o apfst)
- (Facts.add_dynamic (Proof_Context.init_global thy) (Sign.naming_of thy) (b, f) #> snd);
+ |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
(* note_thmss *)
--- a/src/Pure/sign.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/sign.ML Sun Mar 18 13:04:22 2012 +0100
@@ -7,17 +7,6 @@
signature SIGN =
sig
- val rep_sg: theory ->
- {naming: Name_Space.naming,
- syn: Syntax.syntax,
- tsig: Type.tsig,
- consts: Consts.T}
- val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
- val naming_of: theory -> Name_Space.naming
- val full_name: theory -> binding -> string
- val full_name_path: theory -> string -> binding -> string
- val full_bname: theory -> bstring -> string
- val full_bname_path: theory -> string -> bstring -> string
val syn_of: theory -> Syntax.syntax
val tsig_of: theory -> Type.tsig
val classes_of: theory -> Sorts.algebra
@@ -42,6 +31,14 @@
val the_const_type: theory -> string -> typ
val declared_tyname: theory -> string -> bool
val declared_const: theory -> string -> bool
+ val naming_of: theory -> Name_Space.naming
+ val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
+ val restore_naming: theory -> theory -> theory
+ val inherit_naming: theory -> Proof.context -> Context.generic
+ val full_name: theory -> binding -> string
+ val full_name_path: theory -> string -> binding -> string
+ val full_bname: theory -> bstring -> string
+ val full_bname_path: theory -> string -> bstring -> string
val const_monomorphic: theory -> string -> bool
val const_typargs: theory -> string * typ -> typ list
val const_instance: theory -> string * typ list -> typ
@@ -67,7 +64,7 @@
val cert_prop: theory -> term -> term
val no_frees: Proof.context -> term -> term
val no_vars: Proof.context -> term -> term
- val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
+ val add_type: Proof.context -> binding * int * mixfix -> theory -> theory
val add_types_global: (binding * int * mixfix) list -> theory -> theory
val add_nonterminals: Proof.context -> binding list -> theory -> theory
val add_nonterminals_global: binding list -> theory -> theory
@@ -113,7 +110,6 @@
val mandatory_path: string -> theory -> theory
val qualified_path: bool -> binding -> theory -> theory
val local_path: theory -> theory
- val restore_naming: theory -> theory -> theory
val hide_class: bool -> string -> theory -> theory
val hide_type: bool -> string -> theory -> theory
val hide_const: bool -> string -> theory -> theory
@@ -125,56 +121,37 @@
(** datatype sign **)
datatype sign = Sign of
- {naming: Name_Space.naming, (*common naming conventions*)
- syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*)
+ {syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*)
tsig: Type.tsig, (*order-sorted signature of types*)
consts: Consts.T}; (*polymorphic constants*)
-fun make_sign (naming, syn, tsig, consts) =
- Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
+fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
structure Data = Theory_Data_PP
(
type T = sign;
- fun extend (Sign {syn, tsig, consts, ...}) =
- make_sign (Name_Space.default_naming, syn, tsig, consts);
+ fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
- val empty =
- make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
+ val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
- val ctxt = Syntax.init_pretty pp;
- val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
- val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
+ val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
+ val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
- val naming = Name_Space.default_naming;
val syn = Syntax.merge_syntax (syn1, syn2);
- val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
+ val tsig = Type.merge_tsig pp (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
- in make_sign (naming, syn, tsig, consts) end;
+ in make_sign (syn, tsig, consts) end;
);
fun rep_sg thy = Data.get thy |> (fn Sign args => args);
-fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
- make_sign (f (naming, syn, tsig, consts)));
-
-fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
-fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
-fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
-fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
-
+fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
-(* naming *)
-
-val naming_of = #naming o rep_sg;
-
-val full_name = Name_Space.full_name o naming_of;
-fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
-
-fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
-fun full_bname_path thy path = full_name_path thy path o Binding.name;
+fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
+fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
+fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
(* syntax *)
@@ -222,6 +199,21 @@
val declared_const = can o the_const_constraint;
+(* naming *)
+
+val naming_of = Name_Space.naming_of o Context.Theory;
+val map_naming = Context.theory_map o Name_Space.map_naming;
+val restore_naming = map_naming o K o naming_of;
+fun inherit_naming thy =
+ Context.Proof o Context.proof_map (Name_Space.map_naming (K (naming_of thy)));
+
+val full_name = Name_Space.full_name o naming_of;
+fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
+
+fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
+fun full_bname_path thy path = full_name_path thy path o Binding.name;
+
+
(** name spaces **)
@@ -330,22 +322,21 @@
(* add type constructors *)
-fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
+fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
let
- fun type_syntax (b, n, mx) =
- (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
- val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
- val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
- in (naming, syn', tsig', consts) end);
+ val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
+ val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
+ val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
+ in (syn', tsig', consts) end);
fun add_types_global types thy =
- add_types (Syntax.init_pretty_global thy) types thy;
+ fold (add_type (Syntax.init_pretty_global thy)) types thy;
(* add nonterminals *)
-fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
- (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
+fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) =>
+ (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts));
fun add_nonterminals_global ns thy =
add_nonterminals (Syntax.init_pretty_global thy) ns thy;
@@ -353,8 +344,8 @@
(* add type abbreviations *)
-fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
- (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
+fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) =>
+ (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts));
(* modify syntax *)
@@ -409,7 +400,7 @@
val args = map prep raw_args;
in
thy
- |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
+ |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
|> add_syntax_i (map #2 args)
|> pair (map #3 args)
end;
@@ -437,7 +428,7 @@
val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
val (res, consts') = consts_of thy
- |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
+ |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t);
in (res, thy |> map_consts (K consts')) end;
fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
@@ -458,18 +449,16 @@
fun primitive_class (bclass, classes) thy =
thy
- |> map_sign (fn (naming, syn, tsig, consts) =>
- let
- val ctxt = Syntax.init_pretty_global thy;
- val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
- in (naming, syn, tsig', consts) end)
+ |> map_sign (fn (syn, tsig, consts) =>
+ let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
+ in (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.init_pretty_global thy) arg);
+ thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
fun primitive_arity arg thy =
- thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
+ thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
(* add translation functions *)
@@ -512,8 +501,6 @@
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
-val restore_naming = map_naming o K o naming_of;
-
(* hide names *)
--- a/src/Pure/simplifier.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/simplifier.ML Sun Mar 18 13:04:22 2012 +0100
@@ -171,7 +171,7 @@
(* get simprocs *)
-fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
val the_simproc = Name_Space.get o get_simprocs;
val _ =
@@ -202,14 +202,12 @@
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
let
- val naming = Proof_Context.target_naming_of context;
val b' = Morphism.binding phi b;
val simproc' = transform_simproc phi simproc;
in
context
|> Data.map (fn (ss, tab) =>
- (ss addsimprocs [simproc'],
- #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab)))
+ (ss addsimprocs [simproc'], #2 (Name_Space.define context true (b', simproc') tab)))
end)
end;
--- a/src/Pure/sorts.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/sorts.ML Sun Mar 18 13:04:22 2012 +0100
@@ -38,15 +38,15 @@
val minimize_sort: algebra -> sort -> sort
val complete_sort: algebra -> sort -> sort
val minimal_sorts: algebra -> sort list -> sort Ord_List.T
- val add_class: Proof.context -> class * class list -> algebra -> algebra
- val add_classrel: Proof.context -> class * class -> algebra -> algebra
- val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
+ val add_class: Context.pretty -> class * class list -> algebra -> algebra
+ val add_classrel: Context.pretty -> class * class -> algebra -> algebra
+ val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
val empty_algebra: algebra
- val merge_algebra: Proof.context -> algebra * algebra -> algebra
- val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
+ val merge_algebra: Context.pretty -> algebra * algebra -> algebra
+ val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
- val class_error: Proof.context -> class_error -> string
+ val class_error: Context.pretty -> class_error -> string
exception CLASS_ERROR of class_error
val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*)
val meet_sort: algebra -> typ * sort
@@ -187,16 +187,16 @@
fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
-fun err_cyclic_classes ctxt css =
+fun err_cyclic_classes pp css =
error (cat_lines (map (fn cs =>
- "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
+ "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
-fun add_class ctxt (c, cs) = map_classes (fn classes =>
+fun add_class pp (c, cs) = map_classes (fn classes =>
let
val classes' = classes |> Graph.new_node (c, serial ())
handle Graph.DUP dup => err_dup_class dup;
val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
- handle Graph.CYCLES css => err_cyclic_classes ctxt css;
+ handle Graph.CYCLES css => err_cyclic_classes pp css;
in classes'' end);
@@ -207,12 +207,14 @@
fun for_classes _ NONE = ""
| for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
-fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
- error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n " ^
- Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n " ^
- Syntax.string_of_arity ctxt (t, Ss', [c']));
+fun err_conflict pp t cc (c, Ss) (c', Ss') =
+ let val ctxt = Syntax.init_pretty pp in
+ error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n " ^
+ Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n " ^
+ Syntax.string_of_arity ctxt (t, Ss', [c']))
+ end;
-fun coregular ctxt algebra t (c, Ss) ars =
+fun coregular pp algebra t (c, Ss) ars =
let
fun conflict (c', Ss') =
if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -222,62 +224,62 @@
else NONE;
in
(case get_first conflict ars of
- SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
+ SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
| NONE => (c, Ss) :: ars)
end;
fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
-fun insert ctxt algebra t (c, Ss) ars =
+fun insert pp algebra t (c, Ss) ars =
(case AList.lookup (op =) ars c of
- NONE => coregular ctxt algebra t (c, Ss) ars
+ NONE => coregular pp algebra t (c, Ss) ars
| SOME Ss' =>
if sorts_le algebra (Ss, Ss') then ars
else if sorts_le algebra (Ss', Ss)
- then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
- else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
+ then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+ else err_conflict pp t NONE (c, Ss) (c, Ss'));
in
-fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
+fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
-fun insert_complete_ars ctxt algebra (t, ars) arities =
+fun insert_complete_ars pp algebra (t, ars) arities =
let val ars' =
Symtab.lookup_list arities t
- |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
+ |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
in Symtab.update (t, ars') arities end;
-fun add_arities ctxt arg algebra =
- algebra |> map_arities (insert_complete_ars ctxt algebra arg);
+fun add_arities pp arg algebra =
+ algebra |> map_arities (insert_complete_ars pp algebra arg);
-fun add_arities_table ctxt algebra =
- Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
+fun add_arities_table pp algebra =
+ Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
end;
(* classrel *)
-fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
Symtab.empty
- |> add_arities_table ctxt algebra arities);
+ |> add_arities_table pp algebra arities);
-fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
+fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
classes |> Graph.add_edge_trans_acyclic rel
- handle Graph.CYCLES css => err_cyclic_classes ctxt css);
+ handle Graph.CYCLES css => err_cyclic_classes pp css);
(* empty and merge *)
val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
-fun merge_algebra ctxt
+fun merge_algebra pp
(Algebra {classes = classes1, arities = arities1},
Algebra {classes = classes2, arities = arities2}) =
let
val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
handle Graph.DUP c => err_dup_class c
- | Graph.CYCLES css => err_cyclic_classes ctxt css;
+ | Graph.CYCLES css => err_cyclic_classes pp css;
val algebra0 = make_algebra (classes', Symtab.empty);
val arities' =
(case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -285,20 +287,20 @@
| (true, false) => (*no completion*)
(arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
if pointer_eq (ars1, ars2) then raise Symtab.SAME
- else insert_ars ctxt algebra0 t ars2 ars1)
+ else insert_ars pp algebra0 t ars2 ars1)
| (false, true) => (*unary completion*)
Symtab.empty
- |> add_arities_table ctxt algebra0 arities1
+ |> add_arities_table pp algebra0 arities1
| (false, false) => (*binary completion*)
Symtab.empty
- |> add_arities_table ctxt algebra0 arities1
- |> add_arities_table ctxt algebra0 arities2);
+ |> add_arities_table pp algebra0 arities1
+ |> add_arities_table pp algebra0 arities2);
in make_algebra (classes', arities') end;
(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
-fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
+fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
fun restrict_arity t (c, Ss) =
@@ -310,7 +312,7 @@
else NONE;
val classes' = classes |> Graph.restrict P;
val arities' = arities |> Symtab.map (map_filter o restrict_arity);
- in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
+ in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
@@ -323,13 +325,14 @@
No_Arity of string * class |
No_Subsort of sort * sort;
-fun class_error ctxt (No_Classrel (c1, c2)) =
- "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
- | class_error ctxt (No_Arity (a, c)) =
- "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
- | class_error ctxt (No_Subsort (S1, S2)) =
- "Cannot derive subsort relation " ^
- Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
+fun class_error pp =
+ let val ctxt = Syntax.init_pretty pp in
+ fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+ | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+ | No_Subsort (S1, S2) =>
+ "Cannot derive subsort relation " ^
+ Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2
+ end;
exception CLASS_ERROR of class_error;
--- a/src/Pure/theory.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/theory.ML Sun Mar 18 13:04:22 2012 +0100
@@ -177,7 +177,7 @@
fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
let
val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
- val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
+ val (_, axioms') = Name_Space.define (Sign.inherit_naming thy ctxt) true axm axioms;
in axioms' end);
--- a/src/Pure/thm.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/thm.ML Sun Mar 18 13:04:22 2012 +0100
@@ -1772,9 +1772,7 @@
fun add_oracle (b, oracle) thy =
let
- val naming = Sign.naming_of thy;
- val (name, tab') =
- Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
+ val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
val thy' = Oracles.put tab' thy;
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
--- a/src/Pure/type.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/type.ML Sun Mar 18 13:04:22 2012 +0100
@@ -87,16 +87,16 @@
val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
- val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
+ val add_class: Context.generic -> binding * class list -> tsig -> tsig
val hide_class: bool -> string -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
- val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
- val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
- val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
+ val add_type: Context.generic -> binding * int -> tsig -> tsig
+ val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
+ val add_nonterminal: Context.generic -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
- val add_arity: Proof.context -> arity -> tsig -> tsig
- val add_classrel: Proof.context -> class * class -> tsig -> tsig
- val merge_tsig: Proof.context -> tsig * tsig -> tsig
+ val add_arity: Context.pretty -> arity -> tsig -> tsig
+ val add_classrel: Context.pretty -> class * class -> tsig -> tsig
+ val merge_tsig: Context.pretty -> tsig * tsig -> tsig
end;
structure Type: TYPE =
@@ -318,8 +318,9 @@
| _ => error (undecl_type a));
fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
- | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
- handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
+ | arity_sorts pp (TSig {classes, ...}) a S =
+ Sorts.mg_domain (#2 classes) a S
+ handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
@@ -584,14 +585,14 @@
(* classes *)
-fun add_class ctxt naming (c, cs) tsig =
+fun add_class context (c, cs) tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
val _ = Binding.check c;
- val (c', space') = space |> Name_Space.declare ctxt true naming c;
- val classes' = classes |> Sorts.add_class ctxt (c', cs');
+ val (c', space') = space |> Name_Space.declare context true c;
+ val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -600,7 +601,7 @@
(* arities *)
-fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val _ =
(case lookup_type tsig t of
@@ -609,18 +610,18 @@
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
+ val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
in ((space, classes'), default, types) end);
(* classrel *)
-fun add_classrel ctxt rel tsig =
+fun add_classrel pp rel tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val rel' = pairself (cert_class tsig) rel
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_classrel ctxt rel';
+ val classes' = classes |> Sorts.add_classrel pp rel';
in ((space, classes'), default, types) end);
@@ -634,8 +635,8 @@
local
-fun new_decl ctxt naming (c, decl) types =
- (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
+fun new_decl context (c, decl) types =
+ (Binding.check c; #2 (Name_Space.define context true (c, decl) types));
fun map_types f = map_tsig (fn (classes, default, types) =>
let
@@ -651,11 +652,11 @@
in
-fun add_type ctxt naming (c, n) =
+fun add_type context (c, n) =
if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
- else map_types (new_decl ctxt naming (c, LogicalType n));
+ else map_types (new_decl context (c, LogicalType n));
-fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
+fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types =>
let
fun err msg =
cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
@@ -669,9 +670,9 @@
(case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
[] => []
| extras => err ("Extra variables on rhs: " ^ commas_quote extras));
- in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
+ in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
-fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
+fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
end;
@@ -681,7 +682,7 @@
(* merge type signatures *)
-fun merge_tsig ctxt (tsig1, tsig2) =
+fun merge_tsig pp (tsig1, tsig2) =
let
val (TSig {classes = (space1, classes1), default = default1, types = types1,
log_types = _}) = tsig1;
@@ -689,7 +690,7 @@
log_types = _}) = tsig2;
val space' = Name_Space.merge (space1, space2);
- val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
+ val classes' = Sorts.merge_algebra pp (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;
--- a/src/Pure/variable.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/variable.ML Sun Mar 18 13:04:22 2012 +0100
@@ -341,12 +341,14 @@
fun new_fixed ((x, x'), pos) ctxt =
if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
else
- ctxt
- |> map_fixes
- (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
- Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
- |> declare_fixed x
- |> declare_constraints (Syntax.free x');
+ let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
+ ctxt
+ |> map_fixes
+ (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
+ Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
+ |> declare_fixed x
+ |> declare_constraints (Syntax.free x')
+ end;
fun new_fixes names' xs xs' ps =
map_names (K names') #>
--- a/src/Tools/Code/code_preproc.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 18 13:04:22 2012 +0100
@@ -431,7 +431,7 @@
|> fold (ensure_fun thy arities eqngr) cs
|> fold (ensure_rhs thy arities eqngr) cs_rhss;
val arities' = fold (add_arity thy vardeps) insts arities;
- val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
+ val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
--- a/src/Tools/Code/code_thingol.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML Sun Mar 18 13:04:22 2012 +0100
@@ -571,10 +571,9 @@
fun not_wellsorted thy permissive some_thm ty sort e =
let
- val ctxt = Syntax.init_pretty_global thy;
- val err_class = Sorts.class_error ctxt e;
+ val err_class = Sorts.class_error (Context.pretty_global thy) e;
val err_typ =
- "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+ "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
Syntax.string_of_sort_global thy sort;
in
translation_error thy permissive some_thm "Wellsortedness error"
@@ -1001,7 +1000,7 @@
fun read_const_exprs thy =
let
fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
- ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+ ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
fun belongs_here thy' c = forall
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');