# HG changeset patch
# User haftmann
# Date 1231363984 -3600
# Node ID 4638ab6c878f80507cbe61028b67680b60f97726
# Parent  d23fdfa46b6a3d18eb6d699ed536357528727c1a# Parent  172213e44992099dbd9493b37a7671667c05b8a0
merged

diff -r d23fdfa46b6a -r 4638ab6c878f src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Jan 07 20:27:55 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -160,7 +160,7 @@
 
 fun add_locale_cmd name expr elems thy =
   thy 
-  |> Expression.add_locale_cmd name name expr elems
+  |> Expression.add_locale_cmd name "" expr elems
   |> snd
   |> LocalTheory.exit;
 
diff -r d23fdfa46b6a -r 4638ab6c878f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Jan 07 20:27:55 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -18,9 +18,9 @@
     Proof.context -> (term * term list) list list * Proof.context;
 
   (* Declaring locales *)
-  val add_locale: string -> bstring -> expression_i -> Element.context_i list ->
+  val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
     theory -> string * local_theory;
-  val add_locale_cmd: string -> bstring -> expression -> Element.context list ->
+  val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
     theory -> string * local_theory;
 
   (* Interpretation *)
@@ -698,18 +698,20 @@
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    bname predicate_name raw_imprt raw_body thy =
+    bname raw_predicate_bname raw_imprt raw_body thy =
   let
     val name = Sign.full_bname thy bname;
-    val _ = Locale.test_locale thy name andalso
+    val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), (parms, ctxt')) =
       prep_decl raw_imprt raw_body (ProofContext.init thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
+    val predicate_bname = if raw_predicate_bname = "" then bname
+      else raw_predicate_bname;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
-      define_preds predicate_name parms text thy;
+      define_preds predicate_bname parms text thy;
 
     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
     val _ = if null extraTs then ()
@@ -787,7 +789,7 @@
         fold store_dep (deps ~~ prep_result propss results) #>
         (* propagate registrations *)
         (fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
-          (Locale.get_global_registrations thy) thy));
+          (Locale.get_registrations thy) thy));
   in
     goal_ctxt |>
       Proof.theorem_i NONE after_qed (prep_propp propss) |>
@@ -824,7 +826,7 @@
         let
           val thms' = map (Element.morph_witness export') thms;
           val morph' = morph $> Element.satisfy_morphism thms';
-          val add = Locale.add_global_registration (name, (morph', export));
+          val add = Locale.add_registration (name, (morph', export));
         in ((name, morph') :: regs, add thy) end
       | store (Eqns [], []) (regs, thy) =
         let val add = fold_rev (fn (name, morph) =>
@@ -842,7 +844,7 @@
           val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
           val add =
             fold_rev (fn (name, morph) =>
-              Locale.amend_global_registration eq_morph (name, morph) #>
+              Locale.amend_registration eq_morph (name, morph) #>
               Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
             PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
             snd
diff -r d23fdfa46b6a -r 4638ab6c878f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 07 20:27:55 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -393,7 +393,7 @@
     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd name name expr elems #> snd)));
+            (Expression.add_locale_cmd name "" expr elems #> snd)));
 
 val _ =
   OuterSyntax.command "sublocale"
diff -r d23fdfa46b6a -r 4638ab6c878f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jan 07 20:27:55 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -31,7 +31,6 @@
 sig
   type locale
 
-  val test_locale: theory -> string -> bool
   val register_locale: bstring ->
     (string * sort) list * (Binding.T * typ option * mixfix) list ->
     term option * term list ->
@@ -44,6 +43,7 @@
   val extern: theory -> string -> xstring
 
   (* Specification *)
+  val defined: theory -> string -> bool
   val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
   val instance_of: theory -> string -> Morphism.morphism -> term list
   val specification_of: theory -> string -> term option * term list
@@ -71,11 +71,11 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations *)
-  val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+  val add_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
     theory -> theory
-  val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
+  val amend_registration: Morphism.morphism -> (string * Morphism.morphism) ->
     theory -> theory
-  val get_global_registrations: theory -> (string * Morphism.morphism) list
+  val get_registrations: theory -> (string * Morphism.morphism) list
 
   (* Diagnostic *)
   val print_locales: theory -> unit
@@ -109,107 +109,79 @@
 datatype ctxt = datatype Element.ctxt;
 
 
-(*** Basics ***)
+
+(*** Theory data ***)
 
 datatype locale = Loc of {
-  (* extensible lists are in reverse order: decls, notes, dependencies *)
+  (** static part **)
   parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
+  (** dynamic part **)
   decls: (declaration * stamp) list * (declaration * stamp) list,
     (* type and term syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
     (* theorem declarations *)
   dependencies: ((string * Morphism.morphism) * stamp) list
     (* locale dependencies (sublocale relation) *)
-}
+};
 
-
-(*** Theory data ***)
+fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
+  Loc {parameters = parameters, spec = spec, decls = decls,
+    notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
+  mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
+  Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
+    mk_locale ((parameters, spec),
+      (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+        merge (eq_snd op =) (notes, notes')),
+          merge (eq_snd op =) (dependencies, dependencies')));
 
 structure LocalesData = TheoryDataFun
 (
-  type T = NameSpace.T * locale Symtab.table;
-    (* locale namespace and locales of the theory *)
-
+  type T = locale NameSpace.table;
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
-
-  fun join_locales _
-   (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
-    Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
-      Loc {
-        parameters = parameters,
-        spec = spec,
-        decls =
-         (merge (eq_snd op =) (decls1, decls1'),
-          merge (eq_snd op =) (decls2, decls2')),
-        notes = merge (eq_snd op =) (notes, notes'),
-        dependencies = merge (eq_snd op =) (dependencies, dependencies')};
-
-  fun merge _ = NameSpace.join_tables join_locales;
+  fun merge _ = NameSpace.join_tables (K merge_locale);
 );
 
 val intern = NameSpace.intern o #1 o LocalesData.get;
 val extern = NameSpace.extern o #1 o LocalesData.get;
 
-fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
+fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
+
+fun defined thy = is_some o get_locale thy;
 
 fun the_locale thy name = case get_locale thy name
- of SOME loc => loc
+ of SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun test_locale thy name = case get_locale thy name
- of SOME _ => true | NONE => false;
-
 fun register_locale bname parameters spec decls notes dependencies thy =
   thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
-    Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
-      dependencies = dependencies}) #> snd);
+    mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
 
-fun change_locale name f thy =
-  let
-    val Loc {parameters, spec, decls, notes, dependencies} =
-        the_locale thy name;
-    val (parameters', spec', decls', notes', dependencies') =
-      f (parameters, spec, decls, notes, dependencies);
-  in
-    thy
-    |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
-      spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
-  end;
+fun change_locale name =
+  LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
 
 fun print_locales thy =
-  let val (space, locs) = LocalesData.get thy in
-    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
-    |> Pretty.writeln
-  end;
+  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
+  |> Pretty.writeln;
 
 
 (*** Primitive operations ***)
 
-fun params_of thy name =
-  let
-    val Loc {parameters = (_, params), ...} = the_locale thy name
-  in params end;
+fun params_of thy = snd o #parameters o the_locale thy;
 
-fun instance_of thy name morph =
-  params_of thy name |>
-    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
+fun instance_of thy name morph = params_of thy name |>
+  map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
 
-fun specification_of thy name =
-  let
-    val Loc {spec, ...} = the_locale thy name
-  in spec end;
+fun specification_of thy = #spec o the_locale thy;
 
-fun declarations_of thy name =
-  let
-    val Loc {decls, ...} = the_locale thy name
-  in
-    decls |> apfst (map fst) |> apsnd (map fst)
-  end;
+fun declarations_of thy name = the_locale thy name |>
+  #decls |> apfst (map fst) |> apsnd (map fst);
 
 
 (*** Activate context elements of locale ***)
@@ -267,7 +239,7 @@
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   else
     let
-      val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
+      val {parameters = (_, params), dependencies, ...} = the_locale thy name;
       val instance = instance_of thy name morph;
     in
       if member (ident_eq thy) marked (name, instance)
@@ -304,7 +276,7 @@
 
 fun activate_decls thy (name, morph) ctxt =
   let
-    val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
+    val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   in
     ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
@@ -312,7 +284,7 @@
 
 fun activate_notes activ_elem transfer thy (name, morph) input =
   let
-    val Loc {notes, ...} = the_locale thy name;
+    val {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
@@ -323,7 +295,7 @@
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
-    val Loc {parameters = (_, params), spec = (asm, defs), ...} =
+    val {parameters = (_, params), spec = (asm, defs), ...} =
       the_locale thy name;
   in
     input |>
@@ -342,9 +314,9 @@
 local
 
 fun init_global_elem (Notes (kind, facts)) thy =
-      let
-        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
-      in Old_Locale.global_note_qualified kind facts' thy |> snd end
+  let
+    val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+  in Old_Locale.global_note_qualified kind facts' thy |> snd end
 
 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
       ProofContext.add_fixes_i fixes |> snd
@@ -408,42 +380,40 @@
 
 (*** Registrations: interpretations in theories ***)
 
-(* FIXME only global variant needed *)
-structure RegistrationsData = GenericDataFun
+structure RegistrationsData = TheoryDataFun
 (
   type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
-(* FIXME mixins need to be stamped *)
+    (* FIXME mixins need to be stamped *)
     (* registrations, in reverse order of declaration *)
   val empty = [];
   val extend = I;
+  val copy = I;
   fun merge _ data : T = Library.merge (eq_snd op =) data;
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-val get_global_registrations =
-  Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
+val get_registrations =
+  RegistrationsData.get #> map fst #> map (apsnd op $>);
 
-fun add_global reg =
-  (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
-
-fun add_global_registration (name, (base_morph, export)) thy =
-  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
+fun add_registration (name, (base_morph, export)) thy =
+  roundup thy (fn _ => fn (name', morph') =>
+    (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
     (name, base_morph) (get_global_idents thy, thy) |>
     snd (* FIXME ?? uncurry put_global_idents *);
 
-fun amend_global_registration morph (name, base_morph) thy =
+fun amend_registration morph (name, base_morph) thy =
   let
-    val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+    val regs = (RegistrationsData.get #> map fst) thy;
     val base = instance_of thy name base_morph;
     fun match (name', (morph', _)) =
       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
     val i = find_index match (rev regs);
-    val _ = if i = ~1 then error ("No interpretation of locale " ^
+    val _ = if i = ~1 then error ("No registration of locale " ^
         quote (extern thy name) ^ " and parameter instantiation " ^
         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
       else ();
   in
-    (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+    RegistrationsData.map (nth_map (length regs - 1 - i)
       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   end;
 
@@ -456,16 +426,15 @@
   let
     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
     val ctxt'' = ctxt' |> ProofContext.theory (
-      change_locale loc
-        (fn (parameters, spec, decls, notes, dependencies) =>
-          (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
+      (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
+        #>
       (* Registrations *)
       (fn thy => fold_rev (fn (name, morph) =>
             let
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in Old_Locale.global_note_qualified kind args'' #> snd end)
-        (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   in ctxt'' end;
 
 
@@ -476,9 +445,8 @@
 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
 
 fun add_decls add loc decl =
-  ProofContext.theory (change_locale loc
-    (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
+  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
+    #>
   add_thmss loc Thm.internalK
     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
 
@@ -492,10 +460,7 @@
 
 (* Dependencies *)
 
-fun add_dependency loc dep =
-  change_locale loc
-    (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
+fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
 
 
 (*** Reasoning about locales ***)
diff -r d23fdfa46b6a -r 4638ab6c878f src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Jan 07 20:27:55 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -334,7 +334,7 @@
 
 fun init_target _ NONE = global_target
   | init_target thy (SOME target) =
-      make_target target (Locale.test_locale thy (Locale.intern thy target))
+      make_target target (Locale.defined thy (Locale.intern thy target))
       true (Class_Target.is_class thy target) ([], [], []) [];
 
 fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
@@ -384,7 +384,7 @@
 
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (locale_intern
-      (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
+      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
 fun instantiation_cmd raw_arities thy =