--- a/src/Pure/Isar/expression.ML Sat May 25 13:59:08 2013 +0200
+++ b/src/Pure/Isar/expression.ML Sat May 25 15:44:08 2013 +0200
@@ -810,29 +810,34 @@
local
-fun read_with_extended_syntax parse_prop deps ctxt props =
+(* reading *)
+
+fun read_with_extended_syntax prep_prop deps ctxt props =
let
val deps_ctxt = fold Locale.activate_declarations deps ctxt;
in
- map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
+ map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
|> Variable.export_terms deps_ctxt ctxt
end;
-fun read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt =
+fun read_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 = read_with_extended_syntax parse_prop deps expr_ctxt raw_eqns;
+ val eqns = read_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of 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;
+
+(* generic interpretation machinery *)
+
fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
let
- val facts =
- (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
+ val facts = map2 (fn attrs => fn eqn =>
+ (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
val (eqns', ctxt') = ctxt
|> note Thm.lemmaK facts
|-> meta_rewrite;
@@ -845,24 +850,22 @@
|> fold activate' dep_morphs
end;
-fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
+fun generic_interpretation prep_expr prep_prop prep_attr setup_proof note activate
expression raw_eqns initial_ctxt =
let
val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
- read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
+ read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt;
fun after_qed witss eqns =
- note_eqns_register note add_registration deps witss eqns attrss export export';
+ note_eqns_register note activate deps witss eqns attrss export export';
in setup_proof after_qed propss eqns goal_ctxt end;
-val activate_proof = Context.proof_map ooo Locale.add_registration;
-val activate_local_theory = Local_Theory.surface_target ooo activate_proof;
-val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-fun add_dependency locale dep_morph mixin export =
- (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
- #> activate_local_theory dep_morph mixin export;
-fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
+
+(* various flavours of interpretation *)
-fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
+fun assert_not_theory lthy = if Named_Target.is_theory lthy
+ then error "Not possible on level of global theory" else ();
+
+fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
@@ -870,43 +873,40 @@
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_expr parse_prop prep_attr setup_proof
- Attrib.local_notes activate_proof expression raw_eqns ctxt
+ generic_interpretation prep_expr prep_prop prep_attr setup_proof
+ Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
end;
-fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
+fun gen_interpretation prep_expr prep_prop prep_attr expression raw_eqns lthy =
+ if Named_Target.is_theory lthy
+ then
+ lthy
+ |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
+ else
+ lthy
+ |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.activate expression raw_eqns;
+
+fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
let
- val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
- andalso Local_Theory.level lthy = 1;
- val activate = if is_theory then add_registration else activate_local_theory;
- val mark_brittle = if is_theory then I else Local_Theory.mark_brittle;
+ val _ = assert_not_theory lthy;
+ val locale = Named_Target.the_name lthy;
in
lthy
- |> mark_brittle
- |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind activate expression raw_eqns
- end;
-
-fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
- let
- val locale =
- case Option.map #target (Named_Target.peek lthy) of
- SOME locale => locale
- | _ => error "Not in a locale target";
- in
- lthy
- |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind (add_dependency locale) expression raw_eqns
+ |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+ Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
end;
-fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
+fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
let
val locale = prep_loc thy raw_locale;
+ val add_dependency_global = Proof_Context.background_theory ooo Locale.add_dependency 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 (add_dependency_global locale) expression raw_eqns
+ |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+ Local_Theory.notes_kind add_dependency_global expression raw_eqns
end;
in
@@ -914,27 +914,22 @@
fun permanent_interpretation expression raw_eqns lthy =
let
val _ = Local_Theory.assert_bottom true lthy;
- val target = case Named_Target.peek lthy of
- SOME { target, ... } => target
- | NONE => error "Not in a named target";
- val is_theory = (target = "");
- val activate = if is_theory then add_registration else add_dependency target;
+ val target = Named_Target.the_name lthy;
+ val subscribe = if target = "" then Local_Theory.add_registration
+ else Local_Theory.add_dependency target;
in
lthy
|> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
- Local_Theory.notes_kind activate expression raw_eqns
+ Local_Theory.notes_kind subscribe expression raw_eqns
end;
fun ephemeral_interpretation expression raw_eqns lthy =
let
- val _ = if Option.map #target (Named_Target.peek lthy) = SOME ""
- andalso Local_Theory.level lthy = 1
- then error "Not possible on level of global theory" else ();
+ val _ = assert_not_theory lthy;
in
lthy
- |> Local_Theory.mark_brittle
|> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
- Local_Theory.notes_kind activate_local_theory expression raw_eqns
+ Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
end;
fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
--- a/src/Pure/Isar/local_theory.ML Sat May 25 13:59:08 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML Sat May 25 15:44:08 2013 +0200
@@ -14,7 +14,6 @@
val restore: local_theory -> local_theory
val level: Proof.context -> int
val assert_bottom: bool -> local_theory -> local_theory
- val mark_brittle: local_theory -> local_theory
val assert_nonbrittle: local_theory -> local_theory
val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
local_theory -> local_theory
@@ -36,7 +35,6 @@
val target_of: local_theory -> Proof.context
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val target_morphism: local_theory -> morphism
- val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val propagate_ml_env: generic_theory -> generic_theory
val operations_of: local_theory -> operations
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -58,6 +56,12 @@
val class_alias: binding -> class -> local_theory -> local_theory
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
+ val activate: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
+ val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
+ val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
val init: Name_Space.naming -> operations -> Proof.context -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
@@ -232,10 +236,6 @@
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-fun surface_target f =
- map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
- (naming, operations, after_close, brittle, f target));
-
fun propagate_ml_env (context as Context.Proof lthy) =
let val inherit = ML_Env.inherit context in
lthy
@@ -306,6 +306,22 @@
val const_alias = alias Sign.const_alias Proof_Context.const_alias;
+(* activation of locale fragments *)
+
+fun activate_surface dep_morph mixin export =
+ map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
+ (naming, operations, after_close, brittle,
+ (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
+
+fun activate dep_morph mixin export =
+ mark_brittle #> activate_surface dep_morph mixin export;
+
+val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
+
+fun add_dependency locale dep_morph mixin export =
+ (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+ #> activate_surface dep_morph mixin export;
+
(** init and exit **)
--- a/src/Pure/Isar/named_target.ML Sat May 25 13:59:08 2013 +0200
+++ b/src/Pure/Isar/named_target.ML Sat May 25 15:44:08 2013 +0200
@@ -8,6 +8,8 @@
signature NAMED_TARGET =
sig
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+ val is_theory: local_theory -> bool
+ val the_name: local_theory -> string
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val reinit: local_theory -> local_theory -> local_theory
@@ -43,6 +45,17 @@
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
{target = target, is_locale = is_locale, is_class = is_class});
+fun is_theory lthy = Option.map #target (peek lthy) = SOME ""
+ andalso Local_Theory.level lthy = 1;
+
+fun the_name lthy =
+ let
+ val _ = Local_Theory.assert_bottom true lthy;
+ in case Option.map #target (peek lthy) of
+ SOME target => target
+ | _ => error "Not in a named target"
+ end;
+
(* consts in locale *)
--- a/src/Pure/ROOT.ML Sat May 25 13:59:08 2013 +0200
+++ b/src/Pure/ROOT.ML Sat May 25 15:44:08 2013 +0200
@@ -230,8 +230,8 @@
use "Isar/obtain.ML";
(*local theories and targets*)
+use "Isar/locale.ML";
use "Isar/local_theory.ML";
-use "Isar/locale.ML";
use "Isar/generic_target.ML";
use "Isar/overloading.ML";
use "axclass.ML";