# HG changeset patch
# User wenzelm
# Date 1026120883 -7200
# Node ID 1dbed9ea764b897875aeaa18d7768c8e22a0b5d6
# Parent  cf076cdcfbf33661167bb65772597e5b80d90441
clarified text content of locale body;
tuned;

diff -r cf076cdcfbf3 -r 1dbed9ea764b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jul 08 08:20:21 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Jul 08 11:34:43 2002 +0200
@@ -91,12 +91,10 @@
 type locale =
  {import: expr,                                                         (*dynamic import*)
   elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
-  text: ((string * typ) list * term list) * ((string * typ) list * (term * term) list),
-    (*local predicate specification and definitions*)
   params: (string * typ option) list * string list};                    (*all vs. local params*)
 
-fun make_locale import elems text params =
- {import = import, elems = elems, text = text, params = params}: locale;
+fun make_locale import elems params =
+ {import = import, elems = elems, params = params}: locale;
 
 
 
@@ -112,8 +110,8 @@
   val prep_ext = I;
 
   (*joining of locale elements: only facts may be added later!*)
-  fun join ({import, elems, text, params}: locale, {elems = elems', ...}: locale) =
-    Some (make_locale import (gen_merge_lists eq_snd elems elems') text params);
+  fun join ({import, elems, params}: locale, {elems = elems', ...}: locale) =
+    Some (make_locale import (gen_merge_lists eq_snd elems elems') params);
   fun merge ((space1, locs1), (space2, locs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2));
 
@@ -200,10 +198,6 @@
       (rename_term ren t, map (rename_term ren) ps))) defs)
   | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);
 
-fun rename_text ren ((xs, body), (ys, defs)) =
-  ((map (apfst (rename ren)) xs, map (rename_term ren) body),
-   (map (apfst (rename ren)) ys, map (pairself (rename_term ren)) defs));
-
 fun rename_facts prfx elem =
   let
     fun qualify (arg as ((name, atts), x)) =
@@ -256,10 +250,6 @@
   | inst_elem ctxt env (Notes facts) =
       Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
 
-fun inst_text env ((xs, body), (ys, defs)) =
- ((map (apsnd (inst_type env)) xs, map (inst_term env) body),
-  (map (apsnd (inst_type env)) ys, map (pairself (inst_term env)) defs));
-
 
 
 (** structured contexts: rename + merge + implicit type instantiation **)
@@ -343,9 +333,8 @@
   | unify_elemss ctxt fixed_parms elemss =
       let
         val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss);
-        fun inst (((name, ps), (elems, text)), env) =
-          ((name, map (apsnd (apsome (inst_type env))) ps),
-            (map (inst_elem ctxt env) elems, inst_text env text));
+        fun inst (((name, ps), elems), env) =
+          ((name, map (apsnd (apsome (inst_type env))) ps), (map (inst_elem ctxt env) elems));
       in map inst (elemss ~~ envs) end;
 
 fun flatten_expr ctxt (prev_idents, expr) =
@@ -386,14 +375,14 @@
 
     fun eval (name, xs) =
       let
-        val {params = (ps, qs), elems, text, ...} = the_locale thy name;
+        val {params = (ps, qs), elems, ...} = the_locale thy name;
         val ren = filter_out (op =) (map #1 ps ~~ xs);
-        val (params', elems', text') =
-          if null ren then ((ps, qs), map #1 elems, text)
+        val (params', elems') =
+          if null ren then ((ps, qs), map #1 elems)
           else ((map (apfst (rename ren)) ps, map (rename ren) qs),
-            map (rename_elem ren o #1) elems, rename_text ren text);
+            map (rename_elem ren o #1) elems);
         val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
-      in ((name, params'), (elems'', text')) end;
+      in ((name, params'), elems'') end;
 
     val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
     val raw_elemss = unique_parms ctxt (map eval idents);
@@ -504,7 +493,7 @@
 fun declare_elems prep_fixes (ctxt, ((name, ps), elems)) =
   let val (ctxt', propps) =
     (case elems of
-      Int (es, _) => foldl_map declare_int_elem (ctxt, es)
+      Int es => foldl_map declare_int_elem (ctxt, es)
     | Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
     handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   in (ctxt', propps) end;
@@ -524,11 +513,6 @@
 
 end;
 
-val empty_text = (([], []), ([], []));
-
-fun merge_text (((xs1, spec1), (ys1, env1)), ((xs2, spec2), (ys2, env2))) =
-  ((gen_merge_lists eq_fst xs1 xs2, spec1 @ spec2), (ys1 @ ys2, env1 @ env2));
-
 local
 
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
@@ -541,28 +525,49 @@
     val (f, xs) = Term.strip_comb lhs;
   in (Term.dest_Free f, Term.list_abs_free (map Term.dest_Free xs, rhs)) end;
 
-fun bind_def ctxt (name, ps) ((all_text, text), eq) =
+fun bind_def ctxt (name, ps) ((xs, env), eq) =
   let
-    val ((all_xs, _), (all_ys, all_env)) = all_text;
-    val (y, b) = abstract_def eq;
-    val b' = norm_term all_env b;
-    val txt = ((Term.add_frees ([], b'), []), ([y], [(Free y, b')]));
-    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote (#1 y)) [(name, map fst ps)];
+    val ((y, T), b) = abstract_def eq;
+    val b' = norm_term env b;
+    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   in
-    conditional (y mem all_xs) (fn () => err "Attempt to define previously specified variable");
-    conditional (y mem all_ys) (fn () => err "Attempt to redefine variable");
-    (merge_text (all_text, txt), merge_text (text, txt))
+    conditional (exists (equal y o #1) xs) (fn () =>
+      err "Attempt to define previously specified variable");
+    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
+      err "Attempt to redefine variable");
+    (Term.add_frees (xs, b'), (Free (y, T), b') :: env)
   end;
 
-fun eval_text _ _ (all_text, Fixes _) = (all_text, empty_text)
-  | eval_text _ _ (all_text, Assumes asms) =
+fun eval_text _ _ _ (text, Fixes _) = text
+  | eval_text _ _ do_text ((spec, (xs, env)), Assumes asms) =
+      let
+        val ts = map (norm_term env) (flat (map (map #1 o #2) asms));
+        val spec' = if do_text then spec @ ts else spec;
+        val xs' = foldl Term.add_frees (xs, ts);
+      in (spec', (xs', env)) end
+  | eval_text ctxt id _ ((spec, binds), Defines defs) =
+      (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
+  | eval_text _ _ _ (text, Notes _) = text;
+
+fun closeup _ false elem = elem
+  | closeup ctxt true elem =
       let
-        val ts = map (norm_term (#2 (#2 all_text))) (flat (map (map #1 o #2) asms));
-        val txt = ((foldl Term.add_frees ([], ts), ts), ([], []));
-      in (merge_text (all_text, txt), txt) end
-  | eval_text ctxt id (all_text, Defines defs) =
-      foldl (bind_def ctxt id) ((all_text, empty_text), map (#1 o #2) defs)
-  | eval_text _ _ (all_text, Notes _) = (all_text, empty_text);
+        fun close_frees t =
+          let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
+            (Term.add_frees ([], t)))
+          in Term.list_all_free (frees, t) end;
+
+        fun no_binds [] = []
+          | no_binds _ =
+              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
+      in
+        (case elem of
+          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
+            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
+        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
+            (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))
+        | e => e)
+      end;
 
 
 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
@@ -576,41 +581,25 @@
 fun finish_parms parms ((name, ps), elems) =
   ((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems);
 
-fun finish_elems ctxt parms _ ((all_text, int_text, ext_text), ((id, Int e), _)) =
-      let val [(_, (es, txt))] = unify_elemss ctxt parms [(id, e)]
-      in ((merge_text (all_text, txt), merge_text (int_text, txt), ext_text), (id, map Int es)) end
-  | finish_elems ctxt parms close ((all_text, int_text, ext_text), ((id, Ext e), [propp])) =
+fun finish_elems ctxt parms _ _ (text, ((id, Int e), _)) =
       let
-        val e' = finish_ext_elem parms close (e, propp);
-        val (all_text', txt) = eval_text ctxt id (all_text, e');
-      in ((all_text', int_text, merge_text (ext_text, txt)), (id, [Ext e'])) end;
+        val [(_, es)] = unify_elemss ctxt parms [(id, e)];
+        val text' = foldl (eval_text ctxt id false) (text, es);
+      in (text', (id, map Int es)) end
+  | finish_elems ctxt parms do_close do_text (text, ((id, Ext e), [propp])) =
+      let
+        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
+        val text' = eval_text ctxt id do_text (text, e');
+      in (text', (id, [Ext e'])) end;
 
 in
 
-fun finish_elemss ctxt parms close =
-  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms close);
+fun finish_elemss ctxt parms do_close do_text =
+  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close do_text);
 
 end;
 
-fun closeup ctxt elem =
-  let
-    fun close_frees t =
-      let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t)))
-      in Term.list_all_free (frees, t) end;
-
-    fun no_binds ps =
-      if null ps then ps
-      else raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
-  in
-    (case elem of
-      Assumes asms => Assumes (asms |> map (fn (a, propps) =>
-        (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
-    | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
-        (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))
-    | e => e)
-  end;
-
-fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
+fun prep_elemss prep_fixes prepp do_close do_text context fixed_params raw_elemss raw_concl =
   let
     val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
     val raw_propps = map flat raw_proppss;
@@ -633,10 +622,9 @@
       (map (ProofContext.default_type ctxt) xs);
     val parms = param_types (xs ~~ typing);
 
-    val close = if do_close then closeup ctxt else I;
-    val ((_, int_text, ext_text), elemss) = finish_elemss ctxt parms close
-      ((empty_text, empty_text, empty_text), raw_elemss ~~ proppss);
-  in (parms, elemss, (merge_text (int_text, ext_text), ext_text), concl) end;
+    val (text, elemss) =
+      finish_elemss ctxt parms do_close do_text (([], ([], [])), raw_elemss ~~ proppss);
+  in ((parms, elemss, concl), text) end;
 
 in
 
@@ -675,20 +663,19 @@
 local
 
 fun prep_context_statement prep_expr prep_elemss prep_facts
-    close fixed_params import elements raw_concl context =
+    do_close do_text fixed_params import elements raw_concl context =
   let
     val sign = ProofContext.sign_of context;
     fun flatten (ids, Elem (Fixes fixes)) =
           (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
       | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
       | flatten (ids, Expr expr) =
-          let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr)
-          in (ids', map (apsnd Int) elemss) end
+          apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
 
     val (import_ids, raw_import_elemss) = flatten ([], Expr import);
     val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
-    val (parms, all_elemss, texts, concl) =
-      prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
+    val ((parms, all_elemss, concl), (spec, (xs, _))) = prep_elemss do_close do_text context
+      fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
 
     val n = length raw_import_elemss;
     val (import_ctxt, (import_elemss, import_facts)) =
@@ -697,7 +684,7 @@
       activate_facts prep_facts (import_ctxt, drop (n, all_elemss));
   in
     ((((import_ctxt, (import_elemss, import_facts)),
-      (ctxt, (elemss, facts))), texts), concl)
+      (ctxt, (elemss, facts))), (xs, spec)), concl)
   end;
 
 val gen_context = prep_context_statement intern_expr read_elemss get_facts;
@@ -705,7 +692,7 @@
 
 fun gen_facts prep_locale thy name =
   let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
-    |> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
+    |> gen_context_i false false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
   in flat (map #2 facts) end;
 
 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
@@ -716,13 +703,13 @@
       (case locale of None => ([], empty)
       | Some name => (param_types (#1 (#params (the_locale thy name))), Locale name));
     val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
-      prep_ctxt false fixed_params import elems concl ctxt;
+      prep_ctxt false false fixed_params import elems concl ctxt;
   in (locale, locale_ctxt, elems_ctxt, concl') end;
 
 in
 
-fun read_context x y z = #1 (gen_context true [] x y [] z);
-fun cert_context x y z = #1 (gen_context_i true [] x y [] z);
+fun read_context b x y z = #1 (gen_context true b [] x y [] z);
+fun cert_context b x y z = #1 (gen_context_i true b [] x y [] z);
 val locale_facts = gen_facts intern;
 val locale_facts_i = gen_facts (K I);
 val read_context_statement = gen_statement intern gen_context;
@@ -738,8 +725,8 @@
   let
     val sg = Theory.sign_of thy;
     val thy_ctxt = ProofContext.init thy;
-    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), (((pred_xs, pred_ts), _), _)) =
-      read_context import body thy_ctxt;
+    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), (pred_xs, pred_ts)) =
+      read_context true import body thy_ctxt;
     val all_elems = flat (map #2 (import_elemss @ elemss));
 
     val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
@@ -809,16 +796,16 @@
 
 fun put_facts loc args thy =
   let
-    val {import, elems, text, params} = the_locale thy loc;
+    val {import, elems, params} = the_locale thy loc;
     val note = Notes (map (fn ((a, more_atts), th_atts) =>
       ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
-  in thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) text params) end;
+  in thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) params) end;
 
 fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy =
   let
     val thy_ctxt = ProofContext.init thy;
     val loc = prep_locale (Theory.sign_of thy) raw_loc;
-    val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt)));
+    val loc_ctxt = #1 (#1 (#1 (cert_context false (Locale loc) [] thy_ctxt)));
     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
     val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt;
     val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
@@ -855,16 +842,14 @@
       error ("Duplicate definition of locale " ^ quote name));
 
     val thy_ctxt = ProofContext.init thy;
-    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
-        (int_ext_text, ext_text)) = prep_ctxt raw_import raw_body thy_ctxt;
+    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), (xs, spec)) =
+      prep_ctxt true raw_import raw_body thy_ctxt;
 
     val import_parms = params_of import_elemss;
     val body_parms = params_of body_elemss;
     val all_parms = import_parms @ body_parms;
 
-    (* FIXME *)
-    val ((_, spec), defs) = int_ext_text;
-    val ((xs, _), _) = int_ext_text;
+    (* FIXME define foo xs' == atomized spec *)
     val xs' = all_parms |> mapfilter (fn (p, _) =>
       (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
 
@@ -874,7 +859,7 @@
     thy
     |> declare_locale name
     |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
-        ((xs', spec), defs) (all_parms, map fst body_parms))
+        (all_parms, map fst body_parms))
   end;
 
 in
@@ -892,4 +877,3 @@
  [LocalesData.init];
 
 end;
-