# HG changeset patch
# User haftmann
# Date 1447487151 -3600
# Node ID 27ca6147e3b3d1589f3a98bd167bf97c7486aa1d
# Parent  9a51e4dfc5d999fa26230f1dc8a7c5f6507bd420
separate ML module for interpretation

diff -r 9a51e4dfc5d9 -r 27ca6147e3b3 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -127,7 +127,7 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
+   |> Interpretation.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    |> Proof_Context.theory_of
diff -r 9a51e4dfc5d9 -r 27ca6147e3b3 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -36,27 +36,11 @@
   val add_locale_cmd: binding -> binding ->
     expression -> Element.context list -> theory -> string * local_theory
 
-  (* Interpretation *)
+  (* Processing of locale expressions *)
   val cert_goal_expression: expression_i -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context
   val read_goal_expression: expression -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context
-  val permanent_interpretation: expression_i -> (Attrib.binding * term) list ->
-    local_theory -> Proof.state
-  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list ->
-    local_theory -> Proof.state
-  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
-  val interpret_cmd: expression -> (Attrib.binding * string) list ->
-    bool -> Proof.state -> Proof.state
-  val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
-  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
-    local_theory -> Proof.state
-  val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
-  val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
-  val sublocale_global: string -> expression_i ->
-    (Attrib.binding * term) list -> theory -> Proof.state
-  val sublocale_global_cmd: xstring * Position.T -> expression ->
-    (Attrib.binding * string) list -> theory -> Proof.state
 
   (* Diagnostic *)
   val print_dependencies: Proof.context -> bool -> expression -> unit
@@ -848,155 +832,6 @@
 end;
 
 
-(*** Interpretation ***)
-
-local
-
-(* reading *)
-
-fun prep_with_extended_syntax prep_prop deps ctxt props =
-  let
-    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
-  in
-    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
-      |> Variable.export_terms deps_ctxt ctxt
-  end;
-
-fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
-  let
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
-    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
-    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
-    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;
-
-val cert_interpretation =
-  prep_interpretation cert_goal_expression (K I) (K I);
-
-val read_interpretation =
-  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
-
-
-(* generic interpretation machinery *)
-
-fun meta_rewrite ctxt eqns =
-  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
-
-fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
-  let
-    val facts = map2 (fn attrs => fn eqn =>
-      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
-    val (eqns', ctxt') = ctxt
-      |> note Thm.theoremK facts
-      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
-    val dep_morphs =
-      map2 (fn (dep, morph) => fn wits =>
-          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
-        deps witss;
-    fun activate' dep_morph ctxt =
-      activate dep_morph
-        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
-        export ctxt;
-  in
-    ctxt'
-    |> fold activate' dep_morphs
-  end;
-
-fun generic_interpretation prep_interpretation setup_proof note activate
-    expression raw_eqns initial_ctxt =
-  let
-    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
-      prep_interpretation expression raw_eqns initial_ctxt;
-    fun after_qed witss eqns =
-      note_eqns_register note activate deps witss eqns attrss export export';
-  in setup_proof after_qed propss eqns goal_ctxt end;
-
-
-(* first dimension: proof vs. local theory *)
-
-fun gen_interpret prep_interpretation expression raw_eqns int state =
-  let
-    val _ = Proof.assert_forward_or_chain state;
-    val ctxt = Proof.context_of state;
-    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
-    generic_interpretation prep_interpretation setup_proof
-      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
-  end;
-
-fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
-  generic_interpretation prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
-
-
-(* second dimension: relation to underlying target *)
-
-fun subscribe_or_activate lthy =
-  if Named_Target.is_theory lthy
-  then Local_Theory.subscription
-  else Locale.activate_fragment;
-
-fun subscribe_locale_only lthy =
-  let
-    val _ =
-      if Named_Target.is_theory lthy
-      then error "Not possible on level of global theory"
-      else ();
-  in Local_Theory.subscription end;
-
-
-(* special case: global sublocale command *)
-
-fun gen_sublocale_global prep_loc prep_interpretation
-    raw_locale expression raw_eqns thy =
-  let
-    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
-    fun setup_proof after_qed =
-      Element.witness_proof_eqs
-        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
-  in
-    lthy |>
-      generic_interpretation prep_interpretation setup_proof
-        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
-  end;
-
-in
-
-
-(* interfaces *)
-
-fun interpret x = gen_interpret cert_interpretation x;
-fun interpret_cmd x = gen_interpret read_interpretation x;
-
-fun permanent_interpretation expression raw_eqns =
-  Local_Theory.assert_bottom true
-  #> gen_local_theory_interpretation cert_interpretation
-    (K Local_Theory.subscription) expression raw_eqns;
-
-fun ephemeral_interpretation x =
-  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
-
-fun interpretation x =
-  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
-fun interpretation_cmd x =
-  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
-
-fun sublocale x =
-  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
-fun sublocale_cmd x =
-  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
-
-fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
-fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
-
-end;
-
-
 (** Print the instances that would be activated by an interpretation
   of the expression in the current context (clean = false) or in an
   empty context (clean = true). **)
diff -r 9a51e4dfc5d9 -r 27ca6147e3b3 src/Pure/Isar/interpretation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/interpretation.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -0,0 +1,176 @@
+(*  Title:      Pure/Isar/interpretation.ML
+    Author:     Clemens Ballarin, TU Muenchen
+
+Locale interpretation.
+*)
+
+signature INTERPRETATION =
+sig
+  val permanent_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
+    local_theory -> Proof.state
+  val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
+    local_theory -> Proof.state
+  val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
+  val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
+    bool -> Proof.state -> Proof.state
+  val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
+  val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
+    local_theory -> Proof.state
+  val sublocale: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
+  val sublocale_cmd: Expression.expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
+  val sublocale_global: string -> Expression.expression_i ->
+    (Attrib.binding * term) list -> theory -> Proof.state
+  val sublocale_global_cmd: xstring * Position.T -> Expression.expression ->
+    (Attrib.binding * string) list -> theory -> Proof.state
+end;
+
+structure Interpretation : INTERPRETATION =
+struct
+
+local
+
+(* reading *)
+
+fun prep_with_extended_syntax prep_prop deps ctxt props =
+  let
+    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
+  in
+    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
+      |> Variable.export_terms deps_ctxt ctxt
+  end;
+
+fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
+  let
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
+    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
+    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
+    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;
+
+val cert_interpretation =
+  prep_interpretation Expression.cert_goal_expression (K I) (K I);
+
+val read_interpretation =
+  prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
+
+
+(* generic interpretation machinery *)
+
+fun meta_rewrite ctxt eqns =
+  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
+
+fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
+  let
+    val facts = map2 (fn attrs => fn eqn =>
+      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
+    val (eqns', ctxt') = ctxt
+      |> note Thm.theoremK facts
+      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
+    val dep_morphs =
+      map2 (fn (dep, morph) => fn wits =>
+          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
+        deps witss;
+    fun activate' dep_morph ctxt =
+      activate dep_morph
+        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
+        export ctxt;
+  in
+    ctxt'
+    |> fold activate' dep_morphs
+  end;
+
+fun generic_interpretation prep_interpretation setup_proof note activate
+    expression raw_eqns initial_ctxt =
+  let
+    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
+      prep_interpretation expression raw_eqns initial_ctxt;
+    fun after_qed witss eqns =
+      note_eqns_register note activate deps witss eqns attrss export export';
+  in setup_proof after_qed propss eqns goal_ctxt end;
+
+
+(* first dimension: proof vs. local theory *)
+
+fun gen_interpret prep_interpretation expression raw_eqns int state =
+  let
+    val _ = Proof.assert_forward_or_chain state;
+    val ctxt = Proof.context_of state;
+    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
+    generic_interpretation prep_interpretation setup_proof
+      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
+  end;
+
+fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
+  generic_interpretation prep_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
+
+
+(* second dimension: relation to underlying target *)
+
+fun subscribe_or_activate lthy =
+  if Named_Target.is_theory lthy
+  then Local_Theory.subscription
+  else Locale.activate_fragment;
+
+fun subscribe_locale_only lthy =
+  let
+    val _ =
+      if Named_Target.is_theory lthy
+      then error "Not possible on level of global theory"
+      else ();
+  in Local_Theory.subscription end;
+
+
+(* special case: global sublocale command *)
+
+fun gen_sublocale_global prep_loc prep_interpretation
+    raw_locale expression raw_eqns thy =
+  let
+    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
+    fun setup_proof after_qed =
+      Element.witness_proof_eqs
+        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
+  in
+    lthy |>
+      generic_interpretation prep_interpretation setup_proof
+        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
+  end;
+
+in
+
+
+(* interfaces *)
+
+fun interpret x = gen_interpret cert_interpretation x;
+fun interpret_cmd x = gen_interpret read_interpretation x;
+
+fun permanent_interpretation expression raw_eqns =
+  Local_Theory.assert_bottom true
+  #> gen_local_theory_interpretation cert_interpretation
+    (K Local_Theory.subscription) expression raw_eqns;
+
+fun ephemeral_interpretation x =
+  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
+
+fun interpretation x =
+  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
+fun interpretation_cmd x =
+  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
+
+fun sublocale x =
+  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
+fun sublocale_cmd x =
+  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
+
+fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
+fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
+
+end;
+
+end;
diff -r 9a51e4dfc5d9 -r 27ca6147e3b3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -412,21 +412,21 @@
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args >> (fn (loc, (expr, equations)) =>
-        Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
+        Toplevel.theory_to_proof (Interpretation.sublocale_global_cmd loc expr equations)))
     || interpretation_args >> (fn (expr, equations) =>
-        Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
+        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_keyword interpretation}
     "prove interpretation of locale expression in local theory"
     (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
+      Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_keyword interpret}
     "prove interpretation of locale expression in proof context"
     (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.proof' (Expression.interpret_cmd expr equations)));
+      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
 
 
 (* classes *)
diff -r 9a51e4dfc5d9 -r 27ca6147e3b3 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/ROOT.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -271,6 +271,7 @@
 use "Isar/class.ML";
 use "Isar/named_target.ML";
 use "Isar/expression.ML";
+use "Isar/interpretation.ML";
 use "Isar/class_declaration.ML";
 use "Isar/bundle.ML";
 use "Isar/experiment.ML";