diff --git a/src/Pure/Isar/interpretation.ML b/src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML +++ b/src/Pure/Isar/interpretation.ML @@ -1,237 +1,240 @@ (* Title: Pure/Isar/interpretation.ML Author: Clemens Ballarin, TU Muenchen Author: Florian Haftmann, TU Muenchen Locale interpretation. *) signature INTERPRETATION = sig type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (*interpretation in proofs*) val interpret: Expression.expression_i -> Proof.state -> Proof.state val interpret_cmd: Expression.expression -> Proof.state -> Proof.state (*interpretation in local theories*) val interpretation: Expression.expression_i -> local_theory -> Proof.state val interpretation_cmd: Expression.expression -> local_theory -> Proof.state (*interpretation into global theories*) val global_interpretation: Expression.expression_i -> term defines -> local_theory -> Proof.state val global_interpretation_cmd: Expression.expression -> string defines -> local_theory -> Proof.state (*interpretation between locales*) val sublocale: Expression.expression_i -> term defines -> local_theory -> Proof.state val sublocale_cmd: Expression.expression -> string defines -> local_theory -> Proof.state val global_sublocale: string -> Expression.expression_i -> term defines -> theory -> Proof.state val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> string defines -> theory -> Proof.state (*mixed Isar interface*) val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state end; structure Interpretation : INTERPRETATION = struct (** common interpretation machinery **) type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (* reading of locale expressions with rewrite morphisms *) local fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy = let val rhs = prep_term lthy raw_rhs; val lthy' = Variable.declare_term rhs lthy; val ((_, (_, def)), lthy'') = Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy'; in (Thm.symmetric def, lthy'') end; fun augment_with_defs _ [] _ = pair [] (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) | augment_with_defs prep_term raw_defs deps = Local_Theory.begin_nested #> snd #> fold Locale.activate_declarations deps #> fold_map (augment_with_def prep_term) raw_defs #> Local_Theory.end_nested_result Morphism.fact; fun prep_interpretation prep_expr prep_term expression raw_defs initial_ctxt = let val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; val (def_eqns, def_ctxt) = augment_with_defs prep_term raw_defs deps expr_ctxt; val export' = Proof_Context.export_morphism def_ctxt expr_ctxt; in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; in fun cert_interpretation expression = prep_interpretation Expression.cert_goal_expression Syntax.check_term expression; fun read_interpretation expression = prep_interpretation Expression.read_goal_expression Syntax.read_term expression; end; (* interpretation machinery *) local fun abs_def_rule eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); fun note_eqns_register note add_registration deps eqnss witss def_eqns thms export export' ctxt = let val factss = thms |> unflat ((map o map) #1 eqnss) |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt; val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; val deps' = (deps ~~ witss) |> map (fn ((dep, morph), wits) => (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); fun register (dep, eqns) ctxt = ctxt |> add_registration {inst = dep, mixin = Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), export = export}; in ctxt'' |> fold register (deps' ~~ eqnss') end; in fun generic_interpretation prep_interpretation setup_proof note add_registration expression raw_defs initial_ctxt = let val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = prep_interpretation expression raw_defs initial_ctxt; fun after_qed witss eqns = note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; end; (** interfaces **) (* interpretation in proofs *) local fun setup_proof state after_qed propss eqns goal_ctxt = Element.witness_local_proof_eqs (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) "interpret" propss eqns goal_ctxt state; fun gen_interpret prep_interpretation expression state = Proof.assert_forward_or_chain state |> Proof.context_of |> generic_interpretation prep_interpretation (setup_proof state) Attrib.local_notes Locale.add_registration_proof expression []; in val interpret = gen_interpret cert_interpretation; val interpret_cmd = gen_interpret read_interpretation; end; (* interpretation in local theories *) +val add_registration_local_theory = + Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory; + fun interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs - Local_Theory.notes_kind Locale.add_registration_local_theory expression []; + Local_Theory.notes_kind add_registration_local_theory expression []; fun interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs - Local_Theory.notes_kind Locale.add_registration_local_theory expression []; + Local_Theory.notes_kind add_registration_local_theory expression []; (* interpretation into global theories *) fun global_interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; fun global_interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; (* interpretation between locales *) fun sublocale expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; fun sublocale_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; local fun gen_global_sublocale prep_loc prep_interpretation raw_locale expression raw_defs 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 Local_Theory.locale_dependency expression raw_defs end; in fun global_sublocale expression = gen_global_sublocale (K I) cert_interpretation expression; fun global_sublocale_cmd raw_expression = gen_global_sublocale Locale.check read_interpretation raw_expression; end; (* mixed Isar interface *) local fun register_or_activate lthy = if Named_Target.is_theory lthy then Local_Theory.theory_registration - else Locale.add_registration_local_theory; + else add_registration_local_theory; fun gen_isar_interpretation prep_interpretation expression lthy = generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; in fun isar_interpretation expression = gen_isar_interpretation cert_interpretation expression; fun isar_interpretation_cmd raw_expression = gen_isar_interpretation read_interpretation raw_expression; end; end; diff --git a/src/Pure/Isar/local_theory.ML b/src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML +++ b/src/Pure/Isar/local_theory.ML @@ -1,408 +1,390 @@ (* Title: Pure/Isar/local_theory.ML Author: Makarius Local theory operations, with abstract target context. *) type local_theory = Proof.context; type generic_theory = Context.generic; structure Attrib = struct type binding = binding * Token.src list; type thms = (thm list * Token.src list) list; type fact = binding * thms; end; structure Locale = struct type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}; end; signature LOCAL_THEORY = sig type operations val assert: local_theory -> local_theory val level: Proof.context -> int - val revoke_reinitializability: local_theory -> local_theory val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory val background_naming_of: local_theory -> Name_Space.naming val map_background_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory val restore_background_naming: local_theory -> local_theory -> local_theory val full_name: local_theory -> binding -> string val new_group: local_theory -> local_theory val reset_group: local_theory -> local_theory val standard_morphism: local_theory -> Proof.context -> morphism val standard_morphism_theory: local_theory -> morphism val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val raw_theory: (theory -> theory) -> local_theory -> local_theory val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val background_theory: (theory -> theory) -> local_theory -> local_theory val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism val propagate_ml_env: generic_theory -> generic_theory val operations_of: local_theory -> operations val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory val notes_kind: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory val theory_registration: Locale.registration -> local_theory -> local_theory val locale_dependency: Locale.registration -> local_theory -> local_theory val pretty: local_theory -> Pretty.T list val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory val set_defsort: sort -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context, conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory - val exit_global_reinitializable: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory val begin_nested: local_theory -> Binding.scope * local_theory val end_nested: local_theory -> local_theory val end_nested_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * local_theory end; signature PRIVATE_LOCAL_THEORY = sig include LOCAL_THEORY val reset: local_theory -> local_theory end structure Local_Theory: PRIVATE_LOCAL_THEORY = struct (** local theory data **) (* type lthy *) type operations = {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory, notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory, abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory, declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory, theory_registration: Locale.registration -> local_theory -> local_theory, locale_dependency: Locale.registration -> local_theory -> local_theory, pretty: local_theory -> Pretty.T list}; type lthy = {background_naming: Name_Space.naming, operations: operations, conclude: Proof.context -> Proof.context, - reinitializable: bool, target: Proof.context}; -fun make_lthy (background_naming, operations, conclude, reinitializable, target) : lthy = +fun make_lthy (background_naming, operations, conclude, target) : lthy = {background_naming = background_naming, operations = operations, - conclude = conclude, reinitializable = reinitializable, target = target}; + conclude = conclude, target = target}; (* context data *) structure Data = Proof_Data ( type T = lthy list; fun init _ = []; ); (* nested structure *) val level = length o Data.get; (*1: main target at bottom, >= 2: nested target context*) fun assert lthy = if level lthy = 0 then error "Missing local theory context" else lthy; fun assert_bottom lthy = let val _ = assert lthy; in if level lthy > 1 then error "Not at bottom of local theory nesting" else lthy end; fun assert_not_bottom lthy = let val _ = assert lthy; in if level lthy = 1 then error "Already at bottom of local theory nesting" else lthy end; val bottom_of = List.last o Data.get o assert; val top_of = hd o Data.get o assert; fun map_top f = assert #> - Data.map (fn {background_naming, operations, conclude, reinitializable, target} :: parents => - make_lthy (f (background_naming, operations, conclude, reinitializable, target)) :: parents); + Data.map (fn {background_naming, operations, conclude, target} :: parents => + make_lthy (f (background_naming, operations, conclude, target)) :: parents); fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); fun map_contexts f lthy = let val n = level lthy in lthy |> (Data.map o map_index) - (fn (i, {background_naming, operations, conclude, reinitializable, target}) => - make_lthy (background_naming, operations, conclude, reinitializable, + (fn (i, {background_naming, operations, conclude, target}) => + make_lthy (background_naming, operations, conclude, target |> Context_Position.set_visible false |> f (n - i - 1) |> Context_Position.restore_visible target)) |> f n end; -(* reinitializable context -- implicit for nested structures *) - -fun revoke_reinitializability lthy = - if level lthy = 1 then - map_top (fn (background_naming, operations, conclude, _, target) => - (background_naming, operations, conclude, false, target)) lthy - else lthy; - -fun assert_reinitializable lthy = - if #reinitializable (top_of lthy) then lthy - else error "Non-reinitializable local theory context"; - - (* naming for background theory *) val background_naming_of = #background_naming o top_of; fun map_background_naming f = - map_top (fn (background_naming, operations, conclude, reinitializable, target) => - (f background_naming, operations, conclude, reinitializable, target)); + map_top (fn (background_naming, operations, conclude, target) => + (f background_naming, operations, conclude, target)); val restore_background_naming = map_background_naming o K o background_naming_of; val full_name = Name_Space.full_name o background_naming_of; val new_group = map_background_naming Name_Space.new_group; val reset_group = map_background_naming Name_Space.reset_group; (* standard morphisms *) fun standard_morphism lthy ctxt = Proof_Context.norm_export_morphism lthy ctxt $> Morphism.binding_morphism "Local_Theory.standard_binding" (Name_Space.transform_binding (Proof_Context.naming_of lthy)); fun standard_morphism_theory lthy = standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy)); fun standard_form lthy ctxt x = Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x); (* background theory *) fun raw_theory_result f lthy = let val (res, thy') = f (Proof_Context.theory_of lthy); val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy; in (res, lthy') end; fun raw_theory f = #2 o raw_theory_result (f #> pair ()); fun background_theory_result f lthy = let val naming = background_naming_of lthy |> Name_Space.transform_naming (Proof_Context.naming_of lthy); in lthy |> raw_theory_result (fn thy => thy |> Sign.map_naming (K naming) |> f ||> Sign.restore_naming thy) end; fun background_theory f = #2 o background_theory_result (f #> pair ()); (* target contexts *) val target_of = #target o bottom_of; fun target f lthy = let val ctxt = target_of lthy; val ctxt' = ctxt |> Context_Position.set_visible false |> f |> Context_Position.restore_visible ctxt; val thy' = Proof_Context.theory_of ctxt'; in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end; fun target_morphism lthy = standard_morphism lthy (target_of lthy); fun propagate_ml_env (context as Context.Proof lthy) = let val inherit = ML_Env.inherit [context] in lthy |> background_theory (Context.theory_map inherit) |> map_contexts (K (Context.proof_map inherit)) |> Context.Proof end | propagate_ml_env context = context; (** operations **) val operations_of = #operations o top_of; fun operation f lthy = f (operations_of lthy) lthy; fun operation2 f x y = operation (fn ops => f ops x y); (* primitives *) val pretty = operation #pretty; val abbrev = operation2 #abbrev; val define = operation2 #define false; val define_internal = operation2 #define true; val notes_kind = operation2 #notes; val declaration = operation2 #declaration; fun theory_registration registration = assert_bottom #> operation (fn ops => #theory_registration ops registration); fun locale_dependency registration = assert_bottom #> operation (fn ops => #locale_dependency ops registration); (* theorems *) val notes = notes_kind ""; fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single; fun add_thms_dynamic (binding, f) lthy = lthy |> background_theory_result (fn thy => thy |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f)) |-> (fn name => map_contexts (fn _ => fn ctxt => Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #> declaration {syntax = false, pervasive = false} (fn phi => let val binding' = Morphism.binding phi binding in Context.mapping (Global_Theory.alias_fact binding' name) (Proof_Context.alias_fact binding' name) end)); (* default sort *) fun set_defsort S = declaration {syntax = true, pervasive = false} (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S))); (* notation *) fun type_notation add mode raw_args lthy = let val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args; val args' = map (apsnd Mixfix.reset_pos) args; val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args; in declaration {syntax = true, pervasive = false} (Proof_Context.generic_type_notation add mode args') lthy end; fun notation add mode raw_args lthy = let val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args val args' = map (apsnd Mixfix.reset_pos) args; val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args; in declaration {syntax = true, pervasive = false} (Proof_Context.generic_notation add mode args') lthy end; (* name space aliases *) fun syntax_alias global_alias local_alias b name = declaration {syntax = true, pervasive = false} (fn phi => let val b' = Morphism.binding phi b in Context.mapping (global_alias b' name) (local_alias b' name) end); val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias; val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias; (** manage targets **) (* main target *) fun init_target background_naming conclude operations target = - Data.map (K [make_lthy - (background_naming, operations, conclude, true, target)]) target + Data.map (K [make_lthy (background_naming, operations, conclude, target)]) target fun init {background_naming, setup, conclude} operations thy = thy |> Sign.change_begin |> setup |> init_target background_naming (conclude #> target_of #> Sign.change_end_local) operations; val exit_of = #conclude o bottom_of; fun exit lthy = exit_of lthy (assert_bottom lthy); val exit_global = Proof_Context.theory_of o exit; -val exit_global_reinitializable = exit_global o assert_reinitializable; fun exit_result decl (x, lthy) = let val ctxt = exit lthy; val phi = standard_morphism lthy ctxt; in (decl phi x, ctxt) end; fun exit_result_global decl (x, lthy) = let val thy = exit_global lthy; val thy_ctxt = Proof_Context.init_global thy; val phi = standard_morphism lthy thy_ctxt; in (decl phi x, thy) end; (* nested targets *) fun begin_nested lthy = let val _ = assert lthy; val (scope, target) = Proof_Context.new_scope lthy; val entry = make_lthy (background_naming_of lthy, operations_of lthy, - Proof_Context.restore_naming lthy, true, target); + Proof_Context.restore_naming lthy, target); val lthy' = Data.map (cons entry) target; in (scope, lthy') end; fun end_nested lthy = let val _ = assert_not_bottom lthy; val ({conclude, ...} :: rest) = Data.get lthy; in lthy |> Data.put rest |> reset |> conclude end; fun end_nested_result decl (x, lthy) = let val outer_lthy = end_nested lthy; val phi = Proof_Context.export_morphism lthy outer_lthy; in (decl phi x, outer_lthy) end; end; diff --git a/src/Pure/Isar/locale.ML b/src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML +++ b/src/Pure/Isar/locale.ML @@ -1,810 +1,807 @@ (* Title: Pure/Isar/locale.ML Author: Clemens Ballarin, TU Muenchen Locales -- managed Isar proof contexts, based on Pure predicates. Draws basic ideas from Florian Kammueller's original version of locales, but uses the richer infrastructure of Isar instead of the raw meta-logic. Furthermore, structured composition of contexts (with merge and instantiation) is provided, as well as type-inference of the signature parts and predicate definitions of the specification text. Interpretation enables the transfer of declarations and theorems to other contexts, namely those defined by theories, structured proofs and locales themselves. A comprehensive account of locales is available: [1] Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 52(2):123-153, 2014. See also: [2] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. In Stefano Berardi et al., Types for Proofs and Programs: International Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004. [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing Dependencies between Locales. Technical Report TUM-I0607, Technische Universitaet Muenchen, 2006. [4] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, pages 31-43, 2006. *) signature LOCALE = sig (* Locale specification *) val register_locale: binding -> (string * sort) list * ((string * typ) * mixfix) list -> term option * term list -> thm option * thm option -> thm list -> Element.context_i list -> declaration list -> (string * Attrib.fact list) list -> (string * morphism) list -> theory -> theory val locale_space: theory -> Name_Space.T val intern: theory -> xstring -> string val check: theory -> xstring * Position.T -> string val extern: theory -> string -> xstring val markup_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val defined: theory -> string -> bool val parameters_of: theory -> string -> (string * sort) list * ((string * typ) * mixfix) list val params_of: theory -> string -> ((string * typ) * mixfix) list val intros_of: theory -> string -> thm option * thm option val axioms_of: theory -> string -> thm list val instance_of: theory -> string -> morphism -> term list val specification_of: theory -> string -> term option * term list val hyp_spec_of: theory -> string -> Element.context_i list (* Storing results *) val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context (* Activation *) val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic val activate_declarations: string * morphism -> Proof.context -> Proof.context val init: string -> theory -> Proof.context (* Reasoning about locales *) val get_witnesses: Proof.context -> thm list val get_intros: Proof.context -> thm list val get_unfolds: Proof.context -> thm list val witness_add: attribute val intro_add: attribute val unfold_add: attribute val intro_locales_tac: {strict: bool, eager: bool} -> Proof.context -> thm list -> tactic (* Registrations and dependencies *) type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism} val amend_registration: registration -> Context.generic -> Context.generic val add_registration: registration -> Context.generic -> Context.generic val add_registration_theory': registration -> theory -> theory val add_registration_theory: registration -> local_theory -> local_theory val add_registration_local_theory: registration -> local_theory -> local_theory val add_registration_proof: registration -> Proof.context -> Proof.context val registrations_of: Context.generic -> string -> (string * morphism) list val add_dependency': string -> registration -> theory -> theory val add_dependency: string -> registration -> local_theory -> local_theory (* Diagnostic *) val get_locales: theory -> string list val pretty_locales: theory -> bool -> Pretty.T val pretty_locale: theory -> bool -> string -> Pretty.T val pretty_registrations: Proof.context -> string -> Pretty.T val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list type locale_dependency = {source: string, target: string, prefix: (string * bool) list, morphism: morphism, pos: Position.T, serial: serial} val dest_dependencies: theory list -> theory -> locale_dependency list val tracing : Proof.context -> string -> unit end; structure Locale: LOCALE = struct datatype ctxt = datatype Element.ctxt; (*** Locales ***) type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial}; fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2; fun make_dep (name, morphisms) : dep = {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()}; (*table of mixin lists, per list mixins in reverse order of declaration; lists indexed by registration/dependency serial, entries for empty lists may be omitted*) type mixin = (morphism * bool) * serial; type mixins = mixin list Inttab.table; fun lookup_mixins (mixins: mixins) serial' = Inttab.lookup_list mixins serial'; val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); fun rename_mixin (old, new) (mixins: mixins) = (case Inttab.lookup mixins old of NONE => mixins | SOME mixin => Inttab.delete old mixins |> Inttab.update_new (new, mixin)); fun compose_mixins (mixins: mixin list) = fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; datatype locale = Loc of { (* static part *) (*type and term parameters*) parameters: (string * sort) list * ((string * typ) * mixfix) list, (*assumptions (as a single predicate expression) and defines*) spec: term option * term list, intros: thm option * thm option, axioms: thm list, (*diagnostic device: theorem part of hypothetical body as specified by the user*) hyp_spec: Element.context_i list, (* dynamic part *) (*syntax declarations*) syntax_decls: (declaration * serial) list, (*theorem declarations*) notes: ((string * Attrib.fact list) * serial) list, (*locale dependencies (sublocale relation) in reverse order*) dependencies: dep list, (*mixin part of dependencies*) mixins: mixins }; fun mk_locale ((parameters, spec, intros, axioms, hyp_spec), ((syntax_decls, notes), (dependencies, mixins))) = Loc {parameters = parameters, spec = spec, intros = intros, axioms = axioms, hyp_spec = hyp_spec, syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins}; fun map_locale f (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins}) = mk_locale (f ((parameters, spec, intros, axioms, hyp_spec), ((syntax_decls, notes), (dependencies, mixins)))); fun merge_locale (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins}, Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', mixins = mixins', ...}) = mk_locale ((parameters, spec, intros, axioms, hyp_spec), ((merge (eq_snd op =) (syntax_decls, syntax_decls'), merge (eq_snd op =) (notes, notes')), (merge eq_dep (dependencies, dependencies'), (merge_mixins (mixins, mixins'))))); structure Locales = Theory_Data ( type T = locale Name_Space.table; val empty : T = Name_Space.empty_table "locale"; val extend = I; val merge = Name_Space.join_tables (K merge_locale); ); val locale_space = Name_Space.space_of_table o Locales.get; val intern = Name_Space.intern o locale_space; fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); fun markup_extern ctxt = Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup; fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str; val get_locale = Name_Space.lookup o Locales.get; val defined = is_some oo get_locale; fun the_locale thy name = (case get_locale thy name of SOME (Loc loc) => loc | NONE => error ("Unknown locale " ^ quote name)); fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy = thy |> Locales.map (Name_Space.define (Context.Theory thy) true (binding, mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros, map Thm.trim_context axioms, hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes), (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) fun change_locale name = Locales.map o Name_Space.map_table_entry name o map_locale o apsnd; (** Primitive operations **) fun parameters_of thy = #parameters o the_locale thy; val params_of = #2 oo parameters_of; fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> map (Morphism.term morph o Free o #1); fun specification_of thy = #spec o the_locale thy; fun hyp_spec_of thy = #hyp_spec o the_locale thy; fun dependencies_of thy = #dependencies o the_locale thy; fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; (* Print instance and qualifiers *) fun pretty_reg_inst ctxt qs (name, ts) = let fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?"); fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs)); val prt_term = Pretty.quote o Syntax.pretty_term ctxt; fun prt_term' t = if Config.get ctxt show_types then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] else prt_term t; fun prt_inst ts = Pretty.block (Pretty.breaks (pretty_name ctxt name :: map prt_term' ts)); in (case qs of [] => prt_inst ts | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts]) end; fun pretty_reg ctxt export (name, morph) = let val thy = Proof_Context.theory_of ctxt; val morph' = morph $> export; val qs = Morphism.binding_prefix morph'; val ts = instance_of thy name morph'; in pretty_reg_inst ctxt qs (name, ts) end; (*** Identifiers: activated locales in theory or proof context ***) type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *) val empty_idents : idents = Symtab.empty; val insert_idents = Symtab.insert_list (eq_list (op aconv)); val merge_idents = Symtab.merge_list (eq_list (op aconv)); fun redundant_ident thy idents (name, instance) = exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name); structure Idents = Generic_Data ( type T = idents; val empty = empty_idents; val extend = I; val merge = merge_idents; ); (** Resolve locale dependencies in a depth-first fashion **) local val roundup_bound = 120; fun add thy depth stem export (name, morph) (deps, marked) = if depth > roundup_bound then error "Roundup bound exceeded (sublocale relation probably not terminating)." else let val instance = instance_of thy name (morph $> stem $> export); in if redundant_ident thy marked (name, instance) then (deps, marked) else let (*no inheritance of mixins, regardless of requests by clients*) val dependencies = dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} => (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep)))); val marked' = insert_idents (name, instance) marked; val (deps', marked'') = fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies ([], marked'); in ((name, morph $> stem) :: deps' @ deps, marked'') end end; in (* Note that while identifiers always have the external (exported) view, activate_dep is presented with the internal view. *) fun roundup thy activate_dep export (name, morph) (marked, input) = let (* Find all dependencies including new ones (which are dependencies enriching existing registrations). *) val (dependencies, marked') = add thy 0 Morphism.identity export (name, morph) ([], empty_idents); (* Filter out fragments from marked; these won't be activated. *) val dependencies' = filter_out (fn (name, morph) => redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies; in (merge_idents (marked, marked'), input |> fold_rev activate_dep dependencies') end; end; (*** Registrations: interpretations in theories or proof contexts ***) val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord); structure Idtab = Table(type key = string * term list val ord = total_ident_ord); type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial}; type regs = reg Idtab.table; val join_regs : regs * regs -> regs = Idtab.join (fn id => fn (reg1, reg2) => if #serial reg1 = #serial reg2 then raise Idtab.SAME else raise Idtab.DUP id); (* FIXME consolidate with locale dependencies, consider one data slot only *) structure Global_Registrations = Theory_Data' ( (*registrations, indexed by locale name and instance; unique registration serial points to mixin list*) type T = regs * mixins; val empty: T = (Idtab.empty, Inttab.empty); val extend = I; fun merge old_thys = let fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T = (join_regs (regs1, regs2), merge_mixins (mixins1, mixins2)) handle Idtab.DUP id => (*distinct interpretations with same base: merge their mixins*) let val reg1 = Idtab.lookup regs1 id |> the; val reg2 = Idtab.lookup regs2 id |> the; val reg2' = {morphisms = #morphisms reg2, pos = Position.thread_data (), serial = #serial reg1}; val regs2' = Idtab.update (id, reg2') regs2; val mixins2' = rename_mixin (#serial reg2, #serial reg1) mixins2; val _ = warning ("Removed duplicate interpretation after retrieving its mixins" ^ Position.here_list [#pos reg1, #pos reg2] ^ ":\n " ^ Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id)); in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end; in recursive_merge end; ); structure Local_Registrations = Proof_Data ( type T = Global_Registrations.T; val init = Global_Registrations.get; ); val get_registrations = Context.cases Global_Registrations.get Local_Registrations.get; fun map_registrations f (Context.Theory thy) = Context.Theory (Global_Registrations.map f thy) | map_registrations f (Context.Proof ctxt) = Context.Proof (Local_Registrations.map f ctxt); (* Primitive operations *) fun add_reg thy export (name, morph) = let val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()}; val id = (name, instance_of thy name (morph $> export)); in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end; fun add_mixin serial' mixin = (* registration to be amended identified by its serial id *) (map_registrations o apsnd) (insert_mixin serial' mixin); val get_regs = #1 o get_registrations; fun get_mixins context (name, morph) = let val thy = Context.theory_of context; val (regs, mixins) = get_registrations context; in (case Idtab.lookup regs (name, instance_of thy name morph) of NONE => [] | SOME {serial, ...} => lookup_mixins mixins serial) end; fun collect_mixins context (name, morph) = let val thy = Context.theory_of context; in roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep)) Morphism.identity (name, morph) (insert_idents (name, instance_of thy name morph) empty_idents, []) |> snd |> filter (snd o fst) (* only inheritable mixins *) |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph))) |> compose_mixins end; (*** Activate context elements of locale ***) fun activate_err msg kind (name, morph) context = cat_error msg ("The above error(s) occurred while activating " ^ kind ^ " of locale instance\n" ^ (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of)); fun init_element elem context = context |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really) |> Element.init elem |> Context.mapping I (fn ctxt => let val ctxt0 = Context.proof_of context in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end); (* Potentially lazy notes *) fun make_notes kind = map (fn ((b, atts), facts) => if null atts andalso forall (null o #2) facts then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts))) else Notes (kind, [((b, atts), facts)])); fun lazy_notes thy loc = rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) => make_notes kind notes); fun consolidate_notes elems = elems |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE) |> Lazy.consolidate |> ignore; fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])]) | force_notes elem = elem; (* Declarations, facts and entire locale content *) val trace_locales = Attrib.setup_config_bool (Binding.make ("trace_locales", \<^here>)) (K false); fun tracing context msg = if Config.get context trace_locales then Output.tracing msg else (); fun trace kind (name, morph) context = tracing (Context.proof_of context) ("Activating " ^ kind ^ " of " ^ (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of)); fun activate_syntax_decls (name, morph) context = let val _ = trace "syntax" (name, morph) context; val thy = Context.theory_of context; val {syntax_decls, ...} = the_locale thy name; in context |> fold_rev (fn (decl, _) => decl morph) syntax_decls handle ERROR msg => activate_err msg "syntax" (name, morph) context end; fun activate_notes activ_elem transfer context export' (name, morph) input = let val thy = Context.theory_of context; val mixin = (case export' of NONE => Morphism.identity | SOME export => collect_mixins context (name, morph $> export) $> export); val morph' = transfer input $> morph $> mixin; val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name); in (notes', input) |-> fold (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) end handle ERROR msg => activate_err msg "facts" (name, morph) context; fun activate_notes_trace activ_elem transfer context export' (name, morph) context' = let val _ = trace "facts" (name, morph) context'; in activate_notes activ_elem transfer context export' (name, morph) context' end; fun activate_all name thy activ_elem transfer (marked, input) = let val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name; val input' = input |> (not (null params) ? activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |> (* FIXME type parameters *) (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |> (not (null defs) ? activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs))); val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE; in roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input') end; (** Public activation functions **) fun activate_facts export dep context = context |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) (activate_notes_trace init_element Morphism.transfer_morphism'' context export) (the_default Morphism.identity export) dep |-> Idents.put |> Context_Position.restore_visible_generic context; fun activate_declarations dep = Context.proof_map (fn context => context |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep |-> Idents.put |> Context_Position.restore_visible_generic context); fun init name thy = let val context = Context.Proof (Proof_Context.init_global thy); val marked = Idents.get context; in context |> Context_Position.set_visible_generic false |> pair empty_idents |> activate_all name thy init_element Morphism.transfer_morphism'' |-> (fn marked' => Idents.put (merge_idents (marked, marked'))) |> Context_Position.restore_visible_generic context |> Context.proof_of end; (*** Add and extend registrations ***) type registration = Locale.registration; fun amend_registration {mixin = NONE, ...} context = context | amend_registration {inst = (name, morph), mixin = SOME mixin, export} context = let val thy = Context.theory_of context; val ctxt = Context.proof_of context; val regs = get_regs context; val base = instance_of thy name (morph $> export); val serial' = (case Idtab.lookup regs (name, base) of NONE => error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^ " with\nparameter instantiation " ^ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available") | SOME {serial = serial', ...} => serial'); in add_mixin serial' mixin context end; (* Note that a registration that would be subsumed by an existing one will not be generated, and it will not be possible to amend it. *) fun add_registration {inst = (name, base_morph), mixin, export} context = let val thy = Context.theory_of context; val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix); val inst = instance_of thy name mix_morph; val idents = Idents.get context; in if redundant_ident thy idents (name, inst) then context (* FIXME amend mixins? *) else (idents, context) (* add new registrations with inherited mixins *) |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2 (* add mixin *) |> amend_registration {inst = (name, mix_morph), mixin = mixin, export = export} (* activate import hierarchy as far as not already active *) |> activate_facts (SOME export) (name, mix_morph $> pos_morph) end; val add_registration_theory' = Context.theory_map o add_registration; val add_registration_theory = Local_Theory.raw_theory o add_registration_theory'; -fun add_registration_local_theory' registration lthy = +fun add_registration_local_theory registration lthy = let val n = Local_Theory.level lthy in lthy |> Local_Theory.map_contexts (fn level => level = n - 1 ? Context.proof_map (add_registration registration)) end; -fun add_registration_local_theory registration = - Local_Theory.revoke_reinitializability #> add_registration_local_theory' registration - fun add_registration_proof registration ctxt = ctxt |> Proof_Context.set_stmt false |> Context.proof_map (add_registration registration) |> Proof_Context.restore_stmt ctxt; (*** Dependencies ***) fun registrations_of context loc = Idtab.fold_rev (fn ((name, _), {morphisms, ...}) => name = loc ? cons (name, morphisms)) (get_regs context) [] (*with inherited mixins*) |> map (fn (name, (base, export)) => (name, base $> (collect_mixins context (name, base $> export)) $> export)); fun add_dependency' loc {inst = (name, morph), mixin, export} thy = let val dep = make_dep (name, (morph, export)); val add_dep = apfst (cons dep) #> apsnd (case mixin of NONE => I | SOME mixin => insert_mixin (#serial dep) mixin); val thy' = change_locale loc (apsnd add_dep) thy; val context' = Context.Theory thy'; val (_, regs) = fold_rev (roundup thy' cons export) (registrations_of context' loc) (Idents.get context', []); in fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export}) regs thy' end; fun add_dependency loc registration = Local_Theory.raw_theory (add_dependency' loc registration) - #> add_registration_local_theory' registration; + #> add_registration_local_theory registration; (*** Storing results ***) fun add_facts loc kind facts ctxt = if null facts then ctxt else let val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ()); val applied_notes = make_notes kind facts; fun apply_notes morph = applied_notes |> fold (fn elem => fn context => let val elem' = Element.transform_ctxt (Morphism.transfer_morphism'' context $> morph) elem in Element.init elem' context end); val apply_registrations = Context.theory_map (fn context => fold_rev (apply_notes o #2) (registrations_of context loc) context); in ctxt |> Attrib.local_notes kind facts |> #2 |> Proof_Context.background_theory ((change_locale loc o apfst o apsnd) (cons stored_notes) #> apply_registrations) end; fun add_declaration loc syntax decl = syntax ? Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ()))) #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)]; (*** Reasoning about locales ***) (* Storage for witnesses, intro and unfold rules *) structure Thms = Generic_Data ( type T = thm list * thm list * thm list; val empty = ([], [], []); val extend = I; fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) = (Thm.merge_thms (witnesses1, witnesses2), Thm.merge_thms (intros1, intros2), Thm.merge_thms (unfolds1, unfolds2)); ); fun get_thms which ctxt = map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt))); val get_witnesses = get_thms #1; val get_intros = get_thms #2; val get_unfolds = get_thms #3; val witness_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm (Thm.trim_context th) x, y, z))); val intro_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm (Thm.trim_context th) y, z))); val unfold_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm (Thm.trim_context th) z))); (* Tactics *) fun intro_locales_tac {strict, eager} ctxt = (if strict then Method.intros_tac else Method.try_intros_tac) ctxt (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else [])); val _ = Theory.setup (Method.setup \<^binding>\intro_locales\ (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = false})) "back-chain introduction rules of locales without unfolding predicates" #> Method.setup \<^binding>\unfold_locales\ (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = true})) "back-chain all introduction rules of locales"); (*** diagnostic commands and interfaces ***) fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy)); fun pretty_locales thy verbose = Pretty.block (Pretty.breaks (Pretty.str "locales:" :: map (Pretty.mark_str o #1) (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy)))); fun pretty_locale thy show_facts name = let val locale_ctxt = init name thy; fun cons_elem (elem as Notes _) = show_facts ? cons elem | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, []) |> snd |> rev |> tap consolidate_notes |> map force_notes; in Pretty.block (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems) end; fun pretty_registrations ctxt name = (case registrations_of (Context.Proof ctxt) name of [] => Pretty.str "no interpretations" | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs))); fun pretty_locale_deps thy = let fun make_node name = {name = name, parents = map #name (dependencies_of thy name), body = pretty_locale thy false name}; val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); in map make_node names end; type locale_dependency = {source: string, target: string, prefix: (string * bool) list, morphism: morphism, pos: Position.T, serial: serial}; fun dest_dependencies prev_thys thy = let fun remove_prev loc prev_thy deps = (case get_locale prev_thy loc of NONE => deps | SOME (Loc {dependencies = prev_deps, ...}) => if eq_list eq_dep (prev_deps, deps) then [] else subtract eq_dep prev_deps deps); fun result loc (dep: dep) = let val morphism = op $> (#morphisms dep) in {source = #name dep, target = loc, prefix = Morphism.binding_prefix morphism, morphism = morphism, pos = #pos dep, serial = #serial dep} end; fun add (loc, Loc {dependencies = deps, ...}) = fold (cons o result loc) (fold (remove_prev loc) prev_thys deps); in Name_Space.fold_table add (Locales.get thy) [] |> sort (int_ord o apply2 #serial) end; end; diff --git a/src/Pure/Isar/named_target.ML b/src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML +++ b/src/Pure/Isar/named_target.ML @@ -1,139 +1,152 @@ (* Title: Pure/Isar/named_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Targets for theory, locale, class -- at the bottom of the nested structure. *) signature NAMED_TARGET = sig val is_theory: local_theory -> bool val locale_of: local_theory -> string option val bottom_locale_of: local_theory -> string option val class_of: local_theory -> string option val init: Bundle.name list -> string -> theory -> local_theory val theory_init: theory -> local_theory val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory - val reinit: local_theory -> theory -> local_theory + val revoke_reinitializability: local_theory -> local_theory + val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory end; structure Named_Target: NAMED_TARGET = struct (* context data *) datatype target = Theory | Locale of string | Class of string; fun target_of_ident _ "" = Theory | target_of_ident thy ident = if Locale.defined thy ident then (if Class.is_class thy ident then Class else Locale) ident else error ("No such locale: " ^ quote ident); fun ident_of_target Theory = "" | ident_of_target (Locale locale) = locale | ident_of_target (Class class) = class; fun target_is_theory (SOME Theory) = true | target_is_theory _ = false; fun locale_of_target (SOME (Locale locale)) = SOME locale | locale_of_target (SOME (Class locale)) = SOME locale | locale_of_target _ = NONE; fun class_of_target (SOME (Class class)) = SOME class | class_of_target _ = NONE; structure Data = Proof_Data ( - type T = target option; + type T = (target * bool) option; fun init _ = NONE; ); -val get_bottom_target = Data.get; +val get_bottom_target = Option.map fst o Data.get; fun get_target lthy = if Local_Theory.level lthy = 1 then get_bottom_target lthy else NONE; fun ident_of lthy = case get_target lthy of NONE => error "Not in a named target" | SOME target => ident_of_target target; val is_theory = target_is_theory o get_target; val locale_of = locale_of_target o get_target; val bottom_locale_of = locale_of_target o get_bottom_target; val class_of = class_of_target o get_target; +fun is_reinitializable lthy = + Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy; + (* operations *) fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun class_foundation class (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); fun operations Theory = {define = Generic_Target.define Generic_Target.theory_target_foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.theory_abbrev, declaration = fn _ => Generic_Target.theory_declaration, theory_registration = Locale.add_registration_theory, locale_dependency = fn _ => error "Not possible in theory target", pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} | operations (Locale locale) = {define = Generic_Target.define (locale_foundation locale), notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), abbrev = Generic_Target.locale_abbrev locale, declaration = Generic_Target.locale_declaration locale, theory_registration = fn _ => error "Not possible in locale target", locale_dependency = Locale.add_dependency locale, pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} | operations (Class class) = {define = Generic_Target.define (class_foundation class), notes = Generic_Target.notes (Generic_Target.locale_target_notes class), abbrev = Class.abbrev class, declaration = Generic_Target.locale_declaration class, theory_registration = fn _ => error "Not possible in class target", locale_dependency = Locale.add_dependency class, pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; fun setup_context Theory = Proof_Context.init_global | setup_context (Locale locale) = Locale.init locale | setup_context (Class class) = Class.init class; +fun setup target includes = + setup_context target + #> Data.put (SOME (target, null includes)) + #> Bundle.includes includes; + fun init includes ident thy = let val target = target_of_ident thy ident; in thy |> Local_Theory.init {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), - setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes, + setup = setup target includes, conclude = I} (operations target) - |> not (null includes) ? Local_Theory.revoke_reinitializability end; val theory_init = init [] ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; -fun reinit lthy = init [] (ident_of lthy); +val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); + +fun exit_global_reinitialize lthy = + if is_reinitializable lthy + then (init [] (ident_of lthy), Local_Theory.exit_global lthy) + else error "Non-reinitializable local theory context"; end; diff --git a/src/Pure/Isar/target_context.ML b/src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML +++ b/src/Pure/Isar/target_context.ML @@ -1,65 +1,69 @@ (* Title: Pure/Isar/target_context.ML Author: Florian Haftmann Handling of named and nested targets at the Isar toplevel via context begin / end blocks. *) signature TARGET_CONTEXT = sig val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T -> theory -> local_theory val end_named_cmd: local_theory -> Context.generic val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> (local_theory -> Context.generic) * local_theory val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> Context.generic -> local_theory val end_nested_cmd: local_theory -> Context.generic end; structure Target_Context: TARGET_CONTEXT = struct fun prep_includes thy = map (Bundle.check (Proof_Context.init_global thy)); fun context_begin_named_cmd raw_includes ("-", _) thy = Named_Target.init (prep_includes thy raw_includes) "" thy | context_begin_named_cmd raw_includes name thy = Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy; val end_named_cmd = Context.Theory o Local_Theory.exit_global; fun switch_named_cmd NONE (Context.Theory thy) = (end_named_cmd, Named_Target.theory_init thy) | switch_named_cmd (SOME name) (Context.Theory thy) = (end_named_cmd, context_begin_named_cmd [] name thy) | switch_named_cmd NONE (Context.Proof lthy) = (Context.Proof o Local_Theory.reset, lthy) | switch_named_cmd (SOME name) (Context.Proof lthy) = - (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, - (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy); + let + val (reinit, thy) = Named_Target.exit_global_reinitialize lthy + in + (Context.Proof o reinit o Local_Theory.exit_global, + context_begin_named_cmd [] name thy) + end; fun includes raw_includes lthy = Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; fun context_begin_nested_cmd raw_includes raw_elems gthy = gthy |> Context.cases Named_Target.theory_init Local_Theory.assert |> includes raw_includes |> Expression.read_declaration ([], []) I raw_elems |> (#4 o fst) |> Local_Theory.begin_nested |> snd; fun end_nested_cmd lthy = let val lthy' = Local_Theory.end_nested lthy in if Named_Target.is_theory lthy' then Context.Theory (Local_Theory.exit_global lthy') else Context.Proof lthy' end; end; structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;