# HG changeset patch # User haftmann # Date 1369489448 -7200 # Node ID 88a69da5d3faaeacf66a94b6465b4f1106c1506e # Parent 40fe6b80b481dfa19a9bbe30685c26adab52dfd2 tuned structure diff -r 40fe6b80b481 -r 88a69da5d3fa src/Pure/Isar/expression.ML --- 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; diff -r 40fe6b80b481 -r 88a69da5d3fa src/Pure/Isar/local_theory.ML --- 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 **) diff -r 40fe6b80b481 -r 88a69da5d3fa src/Pure/Isar/named_target.ML --- 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 *) diff -r 40fe6b80b481 -r 88a69da5d3fa src/Pure/ROOT.ML --- 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";