# HG changeset patch
# User ballarin
# Date 1150952884 -7200
# Node ID dc92e3aebc71c103de5ba66cf888b5a84e2d493e
# Parent  f0aeb6a145b16039b4c29ee42993a9090f6b20ba
Improved handling of defines imported in duplicate.

diff -r f0aeb6a145b1 -r dc92e3aebc71 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jun 22 05:16:15 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jun 22 07:08:04 2006 +0200
@@ -5,7 +5,7 @@
 Locales -- Isar proof contexts as meta-level predicates, with local
 syntax and implicit structures.
 
-Draws some basic ideas from Florian Kammueller's original version of
+Draws basic ideas from Florian Kammueller's original version of
 locales, but uses the richer infrastructure of Isar instead of the raw
 meta-logic.  Furthermore, we provide structured import of contexts
 (with merge and rename operations), as well as type-inference of the
@@ -20,6 +20,12 @@
 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
     In Stefano Berardi et al., Types for Proofs and Programs: International
     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
+[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
+    Dependencies between Locales. Technical Report TUM-I0607, Technische
+    Universitaet Muenchen, 2006.
+[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
+    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
+    pages 31-43, 2006.
 *)
 
 (* TODO:
@@ -153,7 +159,7 @@
 
 type locale =
  {axiom: Element.witness list,
-    (* For locales that define predicates this is [A [A]], where a is the locale
+    (* For locales that define predicates this is [A [A]], where A is the locale
        specification.  Otherwise []. *)
   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,
@@ -1203,6 +1209,29 @@
 end;
 
 
+(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
+
+fun defs_ord (defs1, defs2) =
+    list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
+      Term.fast_term_ord (d1, d2)) (defs1, defs2);
+structure Defstab =
+    TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
+        val ord = defs_ord);
+
+fun rem_dup_defs es ds =
+    fold_map (fn e as (Defines defs) => (fn ds =>
+                 if Defstab.defined ds defs
+                 then (Defines [], ds)
+                 else (e, Defstab.update (defs, ()) ds))
+               | e => (fn ds => (e, ds))) es ds;
+fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
+  | rem_dup_elemss (Ext e) ds = (Ext e, ds);
+fun rem_dup_defines raw_elemss =
+    fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
+                     apfst (pair id) (rem_dup_elemss es ds))
+               | (id as (_, (Derived _)), es) => (fn ds =>
+                     ((id, es), ds))) raw_elemss Defstab.empty |> #1;
+
 (* CB: type inference and consistency checks for locales.
 
    Works by building a context (through declare_elemss), extracting the
@@ -1221,6 +1250,7 @@
        empty list if there is no target. *)
     (* CB: raw_elemss are list of pairs consisting of identifiers and
        context elements, the latter marked as internal or external. *)
+    val raw_elemss = rem_dup_defines raw_elemss;
     val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
     (* CB: raw_ctxt is context with additional fixed variables derived from
        the fixes elements in raw_elemss,
@@ -1755,21 +1785,21 @@
 
 (* turn Defines into Notes elements, accumulate definition terms *)
 
-fun defines_to_notes true thy (Defines defs) ts =
-    fold_map (fn (a, (def, _)) => fn ts =>
-      ((a, [([assume (cterm_of thy def)], [])]), ts @ [def])) defs ts
-    |> apfst (SOME o Notes)
-  | defines_to_notes false _ (Defines defs) ts =
-    fold (fn (_, (def, _)) => fn ts => ts @ [def]) defs ts |> pair NONE
-  | defines_to_notes _ _ e ts = (SOME e, ts);
+fun defines_to_notes is_ext thy (Defines defs) defns =
+    let
+      val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
+      val notes = map (fn (a, (def, _)) =>
+        (a, [([assume (cterm_of thy def)], [])])) defs
+    in (if is_ext then SOME (Notes notes) else NONE, defns @ [Defines defs']) end
+  | defines_to_notes _ _ e defns = (SOME e, defns);
 
-fun change_defines_elemss thy elemss ts =
+fun change_defines_elemss thy elemss defns =
   let
-    fun change (id as (n, _), es) ts =
+    fun change (id as (n, _), es) defns =
         let
-          val (es', ts') = fold_map (defines_to_notes (n="") thy) es ts
-        in ((id, map_filter I es'), ts') end
-  in fold_map change elemss ts end;
+          val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
+        in ((id, map_filter I es'), defns') end
+  in fold_map change elemss defns end;
 
 fun gen_add_locale prep_ctxt prep_expr
     do_predicate bname raw_import raw_body thy =
@@ -1795,9 +1825,12 @@
           pred_thy), (import, regs)) =
       if do_predicate then
         let
-          val (elemss', defs) = change_defines_elemss thy elemss [];
+          val (elemss', defns) = change_defines_elemss thy elemss [];
           val elemss'' = elemss' @
+(*
               [(("", []), [Defines (map (fn t => (("", []), (t, []))) defs)])];
+*)
+              [(("", []), defns)];
           val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
             define_preds bname text elemss'' thy;
           fun mk_regs elemss wits =