# HG changeset patch
# User haftmann
# Date 1366567693 -7200
# Node ID f27e22880cc3e20e18f49114c05174037155be6d
# Parent  dffc57bfc653dc5838eddcfc98f2ed758afe5dff
more sharing

diff -r dffc57bfc653 -r f27e22880cc3 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 21 16:29:40 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 21 20:08:13 2013 +0200
@@ -804,6 +804,8 @@
 
 (*** Interpretation ***)
 
+local
+
 fun read_with_extended_syntax parse_prop deps ctxt props =
   let
     val deps_ctxt = fold Locale.activate_declarations deps ctxt;
@@ -812,14 +814,18 @@
       |> Variable.export_terms deps_ctxt ctxt
   end;
 
+fun read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt =
+  let
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
+    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) equations;
+    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
+
 fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def);
 
-
-(** Interpretation in theories and proof contexts **)
-
-local
-
-fun note_eqns_register note add_registration deps witss attrss eqns export export' ctxt =
+fun note_eqns_register note add_registration deps witss eqns attrss export export' ctxt =
   let
     val facts = 
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
@@ -835,48 +841,50 @@
         export ctxt'') deps witss
   end;
 
-fun gen_interpretation prep_expr parse_prop prep_attr
-    expression equations thy =
+fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
+    expression equations initial_ctxt = 
   let
-    val initial_ctxt = Named_Target.theory_init thy;
-
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
-    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
+    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
+      read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt;
+    fun after_qed witss eqns =
+      note_eqns_register note add_registration deps witss eqns attrss export export';
+  in setup_proof after_qed propss eqns goal_ctxt end;
 
-    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
-    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
-    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+fun gen_interpretation prep_expr parse_prop prep_attr expression equations thy =
+  thy
+  |> Named_Target.theory_init
+  |> generic_interpretation prep_expr parse_prop prep_attr
+      Element.witness_proof_eqs
+      Local_Theory.notes_kind
+      (Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration)
+      expression equations;
 
-    val note = Local_Theory.notes_kind;
-    val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
-    fun after_qed witss eqns =
-      note_eqns_register note add_registration deps witss attrss eqns export export';
-
-  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
-
-fun gen_interpret prep_expr parse_prop prep_attr
-    expression equations int state =
+fun gen_interpret prep_expr parse_prop prep_attr expression equations int state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
-    val thy = Proof_Context.theory_of ctxt;
-
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
-    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
-
-    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
-    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
-    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
-
-    val note = Attrib.local_notes;
-    val add_registration = Context.proof_map ooo Locale.add_registration;
-    fun after_qed witss eqns =
-      Proof.map_context (note_eqns_register note add_registration deps witss attrss eqns export export')
-      #> Proof.reset_facts;
-
+    fun lift_after_qed after_qed witss eqns = Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
+    fun setup_proof after_qed propss eqns goal_ctxt = 
+      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
   in
-    state
-    |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
+    generic_interpretation prep_expr parse_prop prep_attr
+      setup_proof
+      Attrib.local_notes
+      (Context.proof_map ooo Locale.add_registration)
+      expression equations ctxt
+  end;
+ 
+fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression equations thy =
+  let
+    val locale = prep_loc thy raw_locale;
+  in
+    thy
+    |> Named_Target.init before_exit locale
+    |> generic_interpretation prep_expr parse_prop prep_attr
+        Element.witness_proof_eqs
+        Local_Theory.notes_kind
+        (Proof_Context.background_theory ooo Locale.add_dependency locale)
+        expression equations
   end;
 
 in
@@ -889,48 +897,6 @@
 fun interpret_cmd x = gen_interpret read_goal_expression
   Syntax.parse_prop Attrib.intern_src x;
 
-end;
-
-
-(** Interpretation between locales: declaring sublocale relationships **)
-
-local
-
-fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
-  let
-    val facts =
-      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
-    val (eqns', ctxt') = ctxt
-      |> Local_Theory.notes_kind Thm.lemmaK facts
-      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
-  in
-    ctxt'
-    |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' =>
-      (Proof_Context.background_theory ooo Locale.add_dependency target)
-        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
-        (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true))
-        export ctxt'') deps witss
-  end;
-
-fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
-    before_exit raw_target expression equations thy =
-  let
-    val target = prep_loc thy raw_target;
-    val initial_ctxt = Named_Target.init before_exit target thy;
-
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
-    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
-
-    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
-    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
-    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
-
-    fun after_qed witss eqns =
-      note_eqns_dependency target deps witss attrss eqns export export';
-
-  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
-in
-
 fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
 fun sublocale_cmd x =
   gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;