# HG changeset patch
# User ballarin
# Date 1229626331 -3600
# Node ID 918687637307cdedf9b9c5ae9fc4f416b2c95cc6
# Parent  db37b657a326828e43694a3cf3842e6c5e7d8047
Refactored: evaluate specification text only in locale declarations.

diff -r db37b657a326 -r 918687637307 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Dec 17 15:21:23 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Dec 18 19:52:11 2008 +0100
@@ -271,38 +271,7 @@
   | declare_elem _ (Defines _) ctxt = ctxt
   | declare_elem _ (Notes _) ctxt = ctxt;
 
-(** Finish locale elements, extract specification text **)
-
-val norm_term = Envir.beta_norm oo Term.subst_atomic;
-
-fun bind_def ctxt eq (xs, env, eqs) =
-  let
-    val _ = LocalDefs.cert_def ctxt eq;
-    val ((y, T), b) = LocalDefs.abs_def eq;
-    val b' = norm_term env b;
-    fun err msg = error (msg ^ ": " ^ quote y);
-  in
-    exists (fn (x, _) => x = y) xs andalso
-      err "Attempt to define previously specified variable";
-    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
-      err "Attempt to redefine variable";
-    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
-  end;
-
-fun eval_text _ _ (Fixes _) text = text
-  | eval_text _ _ (Constrains _) text = text
-  | eval_text _ is_ext (Assumes asms)
-        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
-      let
-        val ts = maps (map #1 o #2) asms;
-        val ts' = map (norm_term env) ts;
-        val spec' =
-          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
-          else ((exts, exts'), (ints @ ts, ints' @ ts'));
-      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
-  | eval_text ctxt _ (Defines defs) (spec, binds) =
-      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
-  | eval_text _ _ (Notes _) text = text;
+(** Finish locale elements **)
 
 fun closeup _ _ false elem = elem
   | closeup ctxt parms true elem =
@@ -337,36 +306,24 @@
   | finish_primitive _ close (Defines defs) = close (Defines defs)
   | finish_primitive _ _ (Notes facts) = Notes facts;
 
-fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text =
+fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = NewLocale.params_of thy loc |>
       map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
-    val (asm, defs) = NewLocale.specification_of thy loc;
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
-    val asm' = Option.map (Morphism.term morph) asm;
-    val defs' = map (Morphism.term morph) defs;
-    val text' = text |>
-      (if is_some asm
-        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
-        else I) |>
-      (if not (null defs)
-        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
-        else I)
-(* FIXME clone from new_locale.ML *)
-  in ((loc, morph), text') end;
+  in (loc, morph) end;
 
-fun finish_elem ctxt parms do_close elem text =
+fun finish_elem ctxt parms do_close elem =
   let
     val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
-    val text' = eval_text ctxt true elem' text;
-  in (elem', text') end
+  in elem' end
   
-fun finish ctxt parms do_close insts elems text =
+fun finish ctxt parms do_close insts elems =
   let
-    val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text;
-    val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text';
-  in (deps, elems', text'') end;
+    val deps = map (finish_inst ctxt parms do_close) insts;
+    val elems' = map (finish_elem ctxt parms do_close) elems;
+  in (deps, elems') end;
 
 
 (** Process full context statement: instantiations + elements + conclusion **)
@@ -422,28 +379,9 @@
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
-    val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
-    (* text has the following structure:
-           (((exts, exts'), (ints, ints')), (xs, env, defs))
-       where
-         exts: external assumptions (terms in assumes elements)
-         exts': dito, normalised wrt. env
-         ints: internal assumptions (terms in assumptions from insts)
-         ints': dito, normalised wrt. env
-         xs: the free variables in exts' and ints' and rhss of definitions,
-           this includes parameters except defined parameters
-         env: list of term pairs encoding substitutions, where the first term
-           is a free variable; substitutions represent defines elements and
-           the rhs is normalised wrt. the previous env
-         defs: the equations from the defines elements
-       elems is an updated version of raw_elems:
-         - type info added to Fixes and modified in Constrains
-         - axiom and definition statement replaced by corresponding one
-           from proppss in Assumes and Defines
-         - Facts unchanged
-       *)
+    val (deps, elems') = finish ctxt' parms do_close insts elems;
 
-  in ((fors', deps, elems', concl), (parms, text)) end
+  in ((fors', deps, elems', concl), (parms, ctxt')) end
 
 in
 
@@ -480,14 +418,13 @@
 
 fun prep_declaration prep activate raw_import raw_elems context =
   let
-    val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
-      prep false true context raw_import raw_elems [];
+    val ((fixed, deps, elems, _), (parms, ctxt')) = prep false true context raw_import raw_elems [];
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
       fold NewLocale.activate_local_facts deps;
     val (elems', _) = activate elems (ProofContext.set_stmt true context');
-  in ((fixed, deps, elems'), (parms, spec, defs)) end;
+  in ((fixed, deps, elems'), (parms, ctxt')) end;
 
 in
 
@@ -538,6 +475,81 @@
 
 (*** Locale declarations ***)
 
+(* extract specification text *)
+
+val norm_term = Envir.beta_norm oo Term.subst_atomic;
+
+fun bind_def ctxt eq (xs, env, eqs) =
+  let
+    val _ = LocalDefs.cert_def ctxt eq;
+    val ((y, T), b) = LocalDefs.abs_def eq;
+    val b' = norm_term env b;
+    fun err msg = error (msg ^ ": " ^ quote y);
+  in
+    exists (fn (x, _) => x = y) xs andalso
+      err "Attempt to define previously specified variable";
+    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
+      err "Attempt to redefine variable";
+    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
+  end;
+
+(* text has the following structure:
+       (((exts, exts'), (ints, ints')), (xs, env, defs))
+   where
+     exts: external assumptions (terms in assumes elements)
+     exts': dito, normalised wrt. env
+     ints: internal assumptions (terms in assumptions from insts)
+     ints': dito, normalised wrt. env
+     xs: the free variables in exts' and ints' and rhss of definitions,
+       this includes parameters except defined parameters
+     env: list of term pairs encoding substitutions, where the first term
+       is a free variable; substitutions represent defines elements and
+       the rhs is normalised wrt. the previous env
+     defs: the equations from the defines elements
+   *)
+
+fun eval_text _ _ (Fixes _) text = text
+  | eval_text _ _ (Constrains _) text = text
+  | eval_text _ is_ext (Assumes asms)
+        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
+      let
+        val ts = maps (map #1 o #2) asms;
+        val ts' = map (norm_term env) ts;
+        val spec' =
+          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
+          else ((exts, exts'), (ints @ ts, ints' @ ts'));
+      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
+  | eval_text ctxt _ (Defines defs) (spec, binds) =
+      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
+  | eval_text _ _ (Notes _) text = text;
+
+fun eval_inst ctxt (loc, morph) text =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val (asm, defs) = NewLocale.specification_of thy loc;
+    val asm' = Option.map (Morphism.term morph) asm;
+    val defs' = map (Morphism.term morph) defs;
+    val text' = text |>
+      (if is_some asm
+        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
+        else I) |>
+      (if not (null defs)
+        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
+        else I)
+(* FIXME clone from new_locale.ML *)
+  in text' end;
+
+fun eval_elem ctxt elem text =
+  let
+    val text' = eval_text ctxt true elem text;
+  in text' end;
+
+fun eval ctxt deps elems =
+  let
+    val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], []));
+    val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text';
+  in (spec, defs) end;
+
 (* axiomsN: name of theorem set with destruct rules for locale predicates,
      also name suffix of delta predicates and assumptions. *)
 
@@ -623,7 +635,7 @@
 
 (* CB: main predicate definition function *)
 
-fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
+fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   let
     val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
 
@@ -686,10 +698,12 @@
     val _ = NewLocale.test_locale thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
-    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
+    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 ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
-      define_preds predicate_name text thy;
+      define_preds predicate_name parms text thy;
 
     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
     val _ = if null extraTs then ()