1.1 --- a/src/HOL/Statespace/state_space.ML Wed Jan 07 20:27:55 2009 +0100
1.2 +++ b/src/HOL/Statespace/state_space.ML Wed Jan 07 22:33:04 2009 +0100
1.3 @@ -160,7 +160,7 @@
1.4
1.5 fun add_locale_cmd name expr elems thy =
1.6 thy
1.7 - |> Expression.add_locale_cmd name name expr elems
1.8 + |> Expression.add_locale_cmd name "" expr elems
1.9 |> snd
1.10 |> LocalTheory.exit;
1.11
2.1 --- a/src/Pure/Isar/expression.ML Wed Jan 07 20:27:55 2009 +0100
2.2 +++ b/src/Pure/Isar/expression.ML Wed Jan 07 22:33:04 2009 +0100
2.3 @@ -18,9 +18,9 @@
2.4 Proof.context -> (term * term list) list list * Proof.context;
2.5
2.6 (* Declaring locales *)
2.7 - val add_locale: string -> bstring -> expression_i -> Element.context_i list ->
2.8 + val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
2.9 theory -> string * local_theory;
2.10 - val add_locale_cmd: string -> bstring -> expression -> Element.context list ->
2.11 + val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
2.12 theory -> string * local_theory;
2.13
2.14 (* Interpretation *)
2.15 @@ -698,18 +698,20 @@
2.16 | defines_to_notes _ e = e;
2.17
2.18 fun gen_add_locale prep_decl
2.19 - bname predicate_name raw_imprt raw_body thy =
2.20 + bname raw_predicate_bname raw_imprt raw_body thy =
2.21 let
2.22 val name = Sign.full_bname thy bname;
2.23 - val _ = Locale.test_locale thy name andalso
2.24 + val _ = Locale.defined thy name andalso
2.25 error ("Duplicate definition of locale " ^ quote name);
2.26
2.27 val ((fixed, deps, body_elems), (parms, ctxt')) =
2.28 prep_decl raw_imprt raw_body (ProofContext.init thy);
2.29 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
2.30
2.31 + val predicate_bname = if raw_predicate_bname = "" then bname
2.32 + else raw_predicate_bname;
2.33 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
2.34 - define_preds predicate_name parms text thy;
2.35 + define_preds predicate_bname parms text thy;
2.36
2.37 val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
2.38 val _ = if null extraTs then ()
2.39 @@ -787,7 +789,7 @@
2.40 fold store_dep (deps ~~ prep_result propss results) #>
2.41 (* propagate registrations *)
2.42 (fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
2.43 - (Locale.get_global_registrations thy) thy));
2.44 + (Locale.get_registrations thy) thy));
2.45 in
2.46 goal_ctxt |>
2.47 Proof.theorem_i NONE after_qed (prep_propp propss) |>
2.48 @@ -824,7 +826,7 @@
2.49 let
2.50 val thms' = map (Element.morph_witness export') thms;
2.51 val morph' = morph $> Element.satisfy_morphism thms';
2.52 - val add = Locale.add_global_registration (name, (morph', export));
2.53 + val add = Locale.add_registration (name, (morph', export));
2.54 in ((name, morph') :: regs, add thy) end
2.55 | store (Eqns [], []) (regs, thy) =
2.56 let val add = fold_rev (fn (name, morph) =>
2.57 @@ -842,7 +844,7 @@
2.58 val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
2.59 val add =
2.60 fold_rev (fn (name, morph) =>
2.61 - Locale.amend_global_registration eq_morph (name, morph) #>
2.62 + Locale.amend_registration eq_morph (name, morph) #>
2.63 Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
2.64 PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
2.65 snd
3.1 --- a/src/Pure/Isar/isar_syn.ML Wed Jan 07 20:27:55 2009 +0100
3.2 +++ b/src/Pure/Isar/isar_syn.ML Wed Jan 07 22:33:04 2009 +0100
3.3 @@ -393,7 +393,7 @@
3.4 (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
3.5 >> (fn ((name, (expr, elems)), begin) =>
3.6 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
3.7 - (Expression.add_locale_cmd name name expr elems #> snd)));
3.8 + (Expression.add_locale_cmd name "" expr elems #> snd)));
3.9
3.10 val _ =
3.11 OuterSyntax.command "sublocale"
4.1 --- a/src/Pure/Isar/locale.ML Wed Jan 07 20:27:55 2009 +0100
4.2 +++ b/src/Pure/Isar/locale.ML Wed Jan 07 22:33:04 2009 +0100
4.3 @@ -31,7 +31,6 @@
4.4 sig
4.5 type locale
4.6
4.7 - val test_locale: theory -> string -> bool
4.8 val register_locale: bstring ->
4.9 (string * sort) list * (Binding.T * typ option * mixfix) list ->
4.10 term option * term list ->
4.11 @@ -44,6 +43,7 @@
4.12 val extern: theory -> string -> xstring
4.13
4.14 (* Specification *)
4.15 + val defined: theory -> string -> bool
4.16 val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
4.17 val instance_of: theory -> string -> Morphism.morphism -> term list
4.18 val specification_of: theory -> string -> term option * term list
4.19 @@ -71,11 +71,11 @@
4.20 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
4.21
4.22 (* Registrations *)
4.23 - val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
4.24 + val add_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
4.25 theory -> theory
4.26 - val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
4.27 + val amend_registration: Morphism.morphism -> (string * Morphism.morphism) ->
4.28 theory -> theory
4.29 - val get_global_registrations: theory -> (string * Morphism.morphism) list
4.30 + val get_registrations: theory -> (string * Morphism.morphism) list
4.31
4.32 (* Diagnostic *)
4.33 val print_locales: theory -> unit
4.34 @@ -109,107 +109,79 @@
4.35 datatype ctxt = datatype Element.ctxt;
4.36
4.37
4.38 -(*** Basics ***)
4.39 +
4.40 +(*** Theory data ***)
4.41
4.42 datatype locale = Loc of {
4.43 - (* extensible lists are in reverse order: decls, notes, dependencies *)
4.44 + (** static part **)
4.45 parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
4.46 (* type and term parameters *)
4.47 spec: term option * term list,
4.48 (* assumptions (as a single predicate expression) and defines *)
4.49 + (** dynamic part **)
4.50 decls: (declaration * stamp) list * (declaration * stamp) list,
4.51 (* type and term syntax declarations *)
4.52 notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
4.53 (* theorem declarations *)
4.54 dependencies: ((string * Morphism.morphism) * stamp) list
4.55 (* locale dependencies (sublocale relation) *)
4.56 -}
4.57 +};
4.58
4.59 -
4.60 -(*** Theory data ***)
4.61 +fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
4.62 + Loc {parameters = parameters, spec = spec, decls = decls,
4.63 + notes = notes, dependencies = dependencies};
4.64 +fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
4.65 + mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
4.66 +fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
4.67 + Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
4.68 + mk_locale ((parameters, spec),
4.69 + (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
4.70 + merge (eq_snd op =) (notes, notes')),
4.71 + merge (eq_snd op =) (dependencies, dependencies')));
4.72
4.73 structure LocalesData = TheoryDataFun
4.74 (
4.75 - type T = NameSpace.T * locale Symtab.table;
4.76 - (* locale namespace and locales of the theory *)
4.77 -
4.78 + type T = locale NameSpace.table;
4.79 val empty = NameSpace.empty_table;
4.80 val copy = I;
4.81 val extend = I;
4.82 -
4.83 - fun join_locales _
4.84 - (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
4.85 - Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
4.86 - Loc {
4.87 - parameters = parameters,
4.88 - spec = spec,
4.89 - decls =
4.90 - (merge (eq_snd op =) (decls1, decls1'),
4.91 - merge (eq_snd op =) (decls2, decls2')),
4.92 - notes = merge (eq_snd op =) (notes, notes'),
4.93 - dependencies = merge (eq_snd op =) (dependencies, dependencies')};
4.94 -
4.95 - fun merge _ = NameSpace.join_tables join_locales;
4.96 + fun merge _ = NameSpace.join_tables (K merge_locale);
4.97 );
4.98
4.99 val intern = NameSpace.intern o #1 o LocalesData.get;
4.100 val extern = NameSpace.extern o #1 o LocalesData.get;
4.101
4.102 -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
4.103 +fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
4.104 +
4.105 +fun defined thy = is_some o get_locale thy;
4.106
4.107 fun the_locale thy name = case get_locale thy name
4.108 - of SOME loc => loc
4.109 + of SOME (Loc loc) => loc
4.110 | NONE => error ("Unknown locale " ^ quote name);
4.111
4.112 -fun test_locale thy name = case get_locale thy name
4.113 - of SOME _ => true | NONE => false;
4.114 -
4.115 fun register_locale bname parameters spec decls notes dependencies thy =
4.116 thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
4.117 - Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
4.118 - dependencies = dependencies}) #> snd);
4.119 + mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
4.120
4.121 -fun change_locale name f thy =
4.122 - let
4.123 - val Loc {parameters, spec, decls, notes, dependencies} =
4.124 - the_locale thy name;
4.125 - val (parameters', spec', decls', notes', dependencies') =
4.126 - f (parameters, spec, decls, notes, dependencies);
4.127 - in
4.128 - thy
4.129 - |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
4.130 - spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
4.131 - end;
4.132 +fun change_locale name =
4.133 + LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
4.134
4.135 fun print_locales thy =
4.136 - let val (space, locs) = LocalesData.get thy in
4.137 - Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
4.138 - |> Pretty.writeln
4.139 - end;
4.140 + Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
4.141 + |> Pretty.writeln;
4.142
4.143
4.144 (*** Primitive operations ***)
4.145
4.146 -fun params_of thy name =
4.147 - let
4.148 - val Loc {parameters = (_, params), ...} = the_locale thy name
4.149 - in params end;
4.150 +fun params_of thy = snd o #parameters o the_locale thy;
4.151
4.152 -fun instance_of thy name morph =
4.153 - params_of thy name |>
4.154 - map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
4.155 +fun instance_of thy name morph = params_of thy name |>
4.156 + map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
4.157
4.158 -fun specification_of thy name =
4.159 - let
4.160 - val Loc {spec, ...} = the_locale thy name
4.161 - in spec end;
4.162 +fun specification_of thy = #spec o the_locale thy;
4.163
4.164 -fun declarations_of thy name =
4.165 - let
4.166 - val Loc {decls, ...} = the_locale thy name
4.167 - in
4.168 - decls |> apfst (map fst) |> apsnd (map fst)
4.169 - end;
4.170 +fun declarations_of thy name = the_locale thy name |>
4.171 + #decls |> apfst (map fst) |> apsnd (map fst);
4.172
4.173
4.174 (*** Activate context elements of locale ***)
4.175 @@ -267,7 +239,7 @@
4.176 then error "Roundup bound exceeded (sublocale relation probably not terminating)."
4.177 else
4.178 let
4.179 - val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
4.180 + val {parameters = (_, params), dependencies, ...} = the_locale thy name;
4.181 val instance = instance_of thy name morph;
4.182 in
4.183 if member (ident_eq thy) marked (name, instance)
4.184 @@ -304,7 +276,7 @@
4.185
4.186 fun activate_decls thy (name, morph) ctxt =
4.187 let
4.188 - val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
4.189 + val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
4.190 in
4.191 ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
4.192 fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
4.193 @@ -312,7 +284,7 @@
4.194
4.195 fun activate_notes activ_elem transfer thy (name, morph) input =
4.196 let
4.197 - val Loc {notes, ...} = the_locale thy name;
4.198 + val {notes, ...} = the_locale thy name;
4.199 fun activate ((kind, facts), _) input =
4.200 let
4.201 val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
4.202 @@ -323,7 +295,7 @@
4.203
4.204 fun activate_all name thy activ_elem transfer (marked, input) =
4.205 let
4.206 - val Loc {parameters = (_, params), spec = (asm, defs), ...} =
4.207 + val {parameters = (_, params), spec = (asm, defs), ...} =
4.208 the_locale thy name;
4.209 in
4.210 input |>
4.211 @@ -342,9 +314,9 @@
4.212 local
4.213
4.214 fun init_global_elem (Notes (kind, facts)) thy =
4.215 - let
4.216 - val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
4.217 - in Old_Locale.global_note_qualified kind facts' thy |> snd end
4.218 + let
4.219 + val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
4.220 + in Old_Locale.global_note_qualified kind facts' thy |> snd end
4.221
4.222 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
4.223 ProofContext.add_fixes_i fixes |> snd
4.224 @@ -408,42 +380,40 @@
4.225
4.226 (*** Registrations: interpretations in theories ***)
4.227
4.228 -(* FIXME only global variant needed *)
4.229 -structure RegistrationsData = GenericDataFun
4.230 +structure RegistrationsData = TheoryDataFun
4.231 (
4.232 type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
4.233 -(* FIXME mixins need to be stamped *)
4.234 + (* FIXME mixins need to be stamped *)
4.235 (* registrations, in reverse order of declaration *)
4.236 val empty = [];
4.237 val extend = I;
4.238 + val copy = I;
4.239 fun merge _ data : T = Library.merge (eq_snd op =) data;
4.240 (* FIXME consolidate with dependencies, consider one data slot only *)
4.241 );
4.242
4.243 -val get_global_registrations =
4.244 - Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
4.245 +val get_registrations =
4.246 + RegistrationsData.get #> map fst #> map (apsnd op $>);
4.247
4.248 -fun add_global reg =
4.249 - (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
4.250 -
4.251 -fun add_global_registration (name, (base_morph, export)) thy =
4.252 - roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
4.253 +fun add_registration (name, (base_morph, export)) thy =
4.254 + roundup thy (fn _ => fn (name', morph') =>
4.255 + (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
4.256 (name, base_morph) (get_global_idents thy, thy) |>
4.257 snd (* FIXME ?? uncurry put_global_idents *);
4.258
4.259 -fun amend_global_registration morph (name, base_morph) thy =
4.260 +fun amend_registration morph (name, base_morph) thy =
4.261 let
4.262 - val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
4.263 + val regs = (RegistrationsData.get #> map fst) thy;
4.264 val base = instance_of thy name base_morph;
4.265 fun match (name', (morph', _)) =
4.266 name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
4.267 val i = find_index match (rev regs);
4.268 - val _ = if i = ~1 then error ("No interpretation of locale " ^
4.269 + val _ = if i = ~1 then error ("No registration of locale " ^
4.270 quote (extern thy name) ^ " and parameter instantiation " ^
4.271 space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
4.272 else ();
4.273 in
4.274 - (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
4.275 + RegistrationsData.map (nth_map (length regs - 1 - i)
4.276 (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
4.277 end;
4.278
4.279 @@ -456,16 +426,15 @@
4.280 let
4.281 val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
4.282 val ctxt'' = ctxt' |> ProofContext.theory (
4.283 - change_locale loc
4.284 - (fn (parameters, spec, decls, notes, dependencies) =>
4.285 - (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
4.286 + (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
4.287 + #>
4.288 (* Registrations *)
4.289 (fn thy => fold_rev (fn (name, morph) =>
4.290 let
4.291 val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
4.292 Attrib.map_facts (Attrib.attribute_i thy)
4.293 in Old_Locale.global_note_qualified kind args'' #> snd end)
4.294 - (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
4.295 + (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
4.296 in ctxt'' end;
4.297
4.298
4.299 @@ -476,9 +445,8 @@
4.300 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
4.301
4.302 fun add_decls add loc decl =
4.303 - ProofContext.theory (change_locale loc
4.304 - (fn (parameters, spec, decls, notes, dependencies) =>
4.305 - (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
4.306 + ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
4.307 + #>
4.308 add_thmss loc Thm.internalK
4.309 [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
4.310
4.311 @@ -492,10 +460,7 @@
4.312
4.313 (* Dependencies *)
4.314
4.315 -fun add_dependency loc dep =
4.316 - change_locale loc
4.317 - (fn (parameters, spec, decls, notes, dependencies) =>
4.318 - (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
4.319 +fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
4.320
4.321
4.322 (*** Reasoning about locales ***)
5.1 --- a/src/Pure/Isar/theory_target.ML Wed Jan 07 20:27:55 2009 +0100
5.2 +++ b/src/Pure/Isar/theory_target.ML Wed Jan 07 22:33:04 2009 +0100
5.3 @@ -334,7 +334,7 @@
5.4
5.5 fun init_target _ NONE = global_target
5.6 | init_target thy (SOME target) =
5.7 - make_target target (Locale.test_locale thy (Locale.intern thy target))
5.8 + make_target target (Locale.defined thy (Locale.intern thy target))
5.9 true (Class_Target.is_class thy target) ([], [], []) [];
5.10
5.11 fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
5.12 @@ -384,7 +384,7 @@
5.13
5.14 fun context "-" thy = init NONE thy
5.15 | context target thy = init (SOME (locale_intern
5.16 - (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
5.17 + (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
5.18
5.19 fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
5.20 fun instantiation_cmd raw_arities thy =