--- 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). **)