# HG changeset patch
# User ballarin
# Date 1280603660 -7200
# Node ID 3a46cebd79838d0a902a5ca0ab095a10738cadce
# Parent  d44a5f602b8c893bede0c002394c71542b98b74f
Make registrations generic data.

diff -r d44a5f602b8c -r 3a46cebd7983 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -293,8 +293,8 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, base_morph)
-         (Option.map (rpair true) eq_morph) export_morph
+       Context.theory_map (Locale.add_registration (class, base_morph)
+         (Option.map (rpair true) eq_morph) export_morph)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> Theory_Target.init (SOME class)
     |> pair class
diff -r d44a5f602b8c -r 3a46cebd7983 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -205,8 +205,8 @@
 
 fun activate_defs class thms thy = case Element.eq_morphism thy thms
  of SOME eq_morph => fold (fn cls => fn thy =>
-      Locale.amend_registration (cls, base_morphism thy cls)
-        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
+      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
+        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   | NONE => thy;
 
 fun register_operation class (c, (t, some_def)) thy =
diff -r d44a5f602b8c -r 3a46cebd7983 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -821,10 +821,11 @@
 
     fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
       #-> (fn eqns => fold (fn ((dep, morph), wits) =>
-        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
-            (map (Element.morph_witness export') wits))
-          (Element.eq_morphism thy eqns |> Option.map (rpair true))
-          export thy) (deps ~~ witss)));
+        fn thy => Context.theory_map
+          (Locale.add_registration (dep, morph $> Element.satisfy_morphism
+              (map (Element.morph_witness export') wits))
+            (Element.eq_morphism thy eqns |> Option.map (rpair true))
+            export) thy) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
diff -r d44a5f602b8c -r 3a46cebd7983 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -67,10 +67,10 @@
 
   (* Registrations and dependencies *)
   val add_registration: string * morphism -> (morphism * bool) option ->
-    morphism -> theory -> theory
+    morphism -> Context.generic -> Context.generic
   val amend_registration: string * morphism -> morphism * bool ->
-    morphism -> theory -> theory
-  val get_registrations: theory -> string -> morphism list
+    morphism -> Context.generic -> Context.generic
+  val registrations_of_locale: Context.generic -> string -> (string * morphism) list
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -349,7 +349,7 @@
 
 structure Idtab = Table(type key = string * term list val ord = ident_ord);
 
-structure Registrations = Theory_Data
+structure Registrations = Generic_Data
 (
   type T = ((morphism * morphism) * serial) Idtab.table *
     (* registrations, indexed by locale name and instance;
@@ -391,9 +391,10 @@
   (* registration to be amended identified by its serial id *)
   Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
 
-fun get_mixins thy (name, morph) =
+fun get_mixins context (name, morph) =
   let
-    val (regs, mixins) = Registrations.get thy;
+    val thy = Context.theory_of context;
+    val (regs, mixins) = Registrations.get context;
   in
     case Idtab.lookup regs (name, instance_of thy name morph) of
       NONE => []
@@ -403,32 +404,35 @@
 fun compose_mixins mixins =
   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
 
-fun collect_mixins thy (name, morph) =
-  roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins thy dep))
-    Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
-  |> snd |> filter (snd o fst)  (* only inheritable mixins *)
-  |> (fn x => merge (eq_snd op =) (x, get_mixins thy (name, morph)))
-  |> compose_mixins;
+fun collect_mixins context (name, morph) =
+  let
+    val thy = Context.theory_of context;
+  in
+    roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
+      Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
+    |> snd |> filter (snd o fst)  (* only inheritable mixins *)
+    |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
+    |> compose_mixins
+  end;
 
-fun gen_get_registrations thy select = Registrations.get thy
+fun get_registrations context select = Registrations.get context
   |>> Idtab.dest |>> select
   (* with inherited mixins *)
   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
-    (name, base $> (collect_mixins thy (name, base $> export)) $> export)) regs);
+    (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
 
-fun registrations_for_locale thy name =
-  gen_get_registrations thy (filter (curry (op =) name o fst o fst));
+fun registrations_of_locale context name =
+  get_registrations context (filter (curry (op =) name o fst o fst));
 
-val get_registrations = map snd oo registrations_for_locale;
+fun all_registrations context = get_registrations context I;
 
-fun all_registrations thy = gen_get_registrations thy I;
-
-fun activate_notes' activ_elem transfer thy export (name, morph) input =
+fun activate_notes' activ_elem transfer context export (name, morph) input =
   let
+    val thy = Context.theory_of context;
     val {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
-        val mixin = collect_mixins thy (name, morph $> export);
+        val mixin = collect_mixins context (name, morph $> export);
         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
       in activ_elem (Notes (kind, facts')) input end;
   in
@@ -438,15 +442,16 @@
 fun activate_facts' export dep context =
   let
     val thy = Context.theory_of context;
-    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
+    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) context export;
   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
 
 
 (* Add and extend registrations *)
 
-fun amend_registration (name, morph) mixin export thy =
+fun amend_registration (name, morph) mixin export context =
   let
-    val regs = Registrations.get thy |> fst;
+    val thy = Context.theory_of context;
+    val regs = Registrations.get context |> fst;
     val base = instance_of thy name (morph $> export);
   in
     case Idtab.lookup regs (name, base) of
@@ -454,23 +459,24 @@
           quote (extern thy name) ^ " and\nparameter instantiation " ^
           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
           " available")
-      | SOME (_, serial') => add_mixin serial' mixin thy
+      | SOME (_, serial') => add_mixin serial' mixin context
   end;
 
 (* Note that a registration that would be subsumed by an existing one will not be
    generated, and it will not be possible to amend it. *)
 
-fun add_registration (name, base_morph) mixin export thy =
+fun add_registration (name, base_morph) mixin export context =
   let
+    val thy = Context.theory_of context;
     val mix = case mixin of NONE => Morphism.identity
           | SOME (mix, _) => mix;
     val morph = base_morph $> mix;
     val inst = instance_of thy name morph;
   in
-    if member (ident_le thy) (get_idents (Context.Theory thy)) (name, inst)
-    then thy
+    if member (ident_le thy) (get_idents context) (name, inst)
+    then context
     else
-      (get_idents (Context.Theory thy), thy)
+      (get_idents context, context)
       (* add new registrations with inherited mixins *)
       |> roundup thy (add_reg thy export) export (name, morph)
       |> snd
@@ -478,7 +484,7 @@
       |> (case mixin of NONE => I
            | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
-      |> Context.theory_map (activate_facts' export (name, morph))
+      |> activate_facts' export (name, morph)
   end;
 
 
@@ -487,11 +493,12 @@
 fun add_dependency loc (name, morph) export thy =
   let
     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
+    val context' = Context.Theory thy';
     val (_, regs) = fold_rev (roundup thy' cons export)
-      (all_registrations thy') (get_idents (Context.Theory thy'), []);
+      (all_registrations context') (get_idents (context'), []);
   in
     thy'
-    |> fold_rev (fn dep => add_registration dep NONE export) regs
+    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   end;
 
 
@@ -511,7 +518,7 @@
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in PureThy.note_thmss kind args'' #> snd end)
-        (registrations_for_locale thy loc) thy))
+        (registrations_of_locale (Context.Theory thy) loc) thy))
   in ctxt'' end;
 
 
@@ -594,7 +601,7 @@
   end;
 
 fun print_registrations thy raw_name =
-  (case registrations_for_locale thy (intern thy raw_name) of
+  (case registrations_of_locale (Context.Theory thy) (intern thy raw_name) of
       [] => Pretty.str ("no interpretations")
     | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   |> Pretty.writeln;
@@ -607,7 +614,7 @@
         val params = params_of thy name;
         val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
         val registrations = map (instance_of thy name o snd)
-          (registrations_for_locale thy name);
+          (registrations_of_locale (Context.Theory thy) name);
       in 
         Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
       end;
diff -r d44a5f602b8c -r 3a46cebd7983 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Tools/quickcheck.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -228,7 +228,7 @@
     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
     val check_goals = case some_locale
      of NONE => [proto_goal]
-      | SOME locale => map (fn phi => Morphism.term phi proto_goal) (Locale.get_registrations thy locale);
+      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of_locale (Context.Theory thy) (*FIXME*) locale);
     val inst_goals = maps (fn check_goal => map (fn T =>
       Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
         handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals