# HG changeset patch # User wenzelm # Date 1465479709 -7200 # Node ID 7dd3ee7ee422087a282d03b33a359f35ac304daa # Parent 27d51aa2d7119bb019ada7bd62e449c8bf9eeb08 support for bundle definition via target; diff -r 27d51aa2d711 -r 7dd3ee7ee422 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Thu Jun 09 12:21:15 2016 +0200 +++ b/src/Pure/Isar/bundle.ML Thu Jun 09 15:41:49 2016 +0200 @@ -9,10 +9,12 @@ val check: Proof.context -> xstring * Position.T -> string val get_bundle: Proof.context -> string -> Attrib.thms val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms + val print_bundles: bool -> Proof.context -> unit val bundle: binding * Attrib.thms -> (binding * typ option * mixfix) list -> local_theory -> local_theory val bundle_cmd: binding * (Facts.ref * Token.src list) list -> (binding * string option * mixfix) list -> local_theory -> local_theory + val init: binding -> theory -> local_theory val includes: string list -> Proof.context -> Proof.context val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context val include_: string list -> Proof.state -> Proof.state @@ -23,34 +25,82 @@ generic_theory -> Binding.scope * local_theory val context_cmd: (xstring * Position.T) list -> Element.context list -> generic_theory -> Binding.scope * local_theory - val print_bundles: bool -> Proof.context -> unit end; structure Bundle: BUNDLE = struct -(* maintain bundles *) +(** context data **) + +structure Data = Generic_Data +( + type T = Attrib.thms Name_Space.table * Attrib.thms option; + val empty : T = (Name_Space.empty_table "bundle", NONE); + val extend = I; + fun merge ((tab1, target1), (tab2, target2)) = + (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); +); + + +(* bundles *) + +val get_bundles_generic = #1 o Data.get; +val get_bundles = get_bundles_generic o Context.Proof; + +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); + +val get_bundle_generic = Name_Space.get o get_bundles_generic; +val get_bundle = get_bundle_generic o Context.Proof; +fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; + +fun define_bundle def context = + let + val (name, bundles') = Name_Space.define context true def (get_bundles_generic context); + val context' = (Data.map o apfst o K) bundles' context; + in (name, context') end; + + +(* target -- bundle under construction *) + +fun the_target thy = + (case #2 (Data.get (Context.Theory thy)) of + SOME thms => thms + | NONE => error "Missing bundle target"); + +val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; +val set_target = Context.theory_map o Data.map o apsnd o K o SOME; + +fun augment_target thms = + Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); + + +(* print bundles *) + +fun pretty_bundle ctxt (markup_name, bundle) = + let + val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; + + fun prt_thms (ths, []) = map prt_thm ths + | prt_thms (ths, atts) = Pretty.enclose "(" ")" + (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; + in + Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ + (if null bundle then [] else Pretty.breaks (Pretty.str " =" :: maps prt_thms bundle))) + end; + +fun print_bundles verbose ctxt = + Pretty.writeln_chunks + (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt))); + + + +(** define bundle **) fun transform_bundle phi = map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); -structure Data = Generic_Data -( - type T = Attrib.thms Name_Space.table; - val empty : T = Name_Space.empty_table "bundle"; - val extend = I; - val merge = Name_Space.merge_tables; -); -val get_bundles = Data.get o Context.Proof; - -fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); - -val get_bundle = Name_Space.get o get_bundles; -fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; - - -(* define bundle *) +(* command *) local @@ -64,10 +114,7 @@ |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => fn context => - context |> Data.map - (#2 o Name_Space.define context true - (Morphism.binding phi binding, transform_bundle phi bundle))) + (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) end; in @@ -78,7 +125,67 @@ end; -(* include bundles *) +(* target *) + +local + +fun bad_operation _ = error "Not possible in bundle target"; + +fun conclude binding = + Local_Theory.background_theory_result (fn thy => + let + val (name, Context.Theory thy') = + define_bundle (binding, the_target thy) (Context.Theory thy); + in (name, reset_target thy') end); + +fun pretty binding lthy = + let + val bundle = the_target (Proof_Context.theory_of lthy); + val (name, lthy') = conclude binding lthy; + val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy'); + val markup_name = + Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name; + in [pretty_bundle lthy' (markup_name, bundle)] end; + +fun bundle_notes kind facts lthy = + let + val bundle = facts + |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms); + in + lthy + |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle) + |> Generic_Target.standard_notes (K true) kind facts + |> Attrib.local_notes kind facts + end; + +fun bundle_declaration decl lthy = + lthy + |> (augment_target o Attrib.internal_declaration) + (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl) + |> Generic_Target.standard_declaration (K true) decl; + +in + +fun init binding thy = + thy + |> Sign.change_begin + |> set_target [] + |> Proof_Context.init_global + |> Local_Theory.init (Sign.naming_of thy) + {define = bad_operation, + notes = bundle_notes, + abbrev = bad_operation, + declaration = K bundle_declaration, + theory_registration = bad_operation, + locale_dependency = bad_operation, + pretty = pretty binding, + exit = conclude binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local} + +end; + + + +(** include bundles **) local @@ -120,22 +227,4 @@ end; - -(* print_bundles *) - -fun print_bundles verbose ctxt = - let - val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; - - fun prt_fact (ths, []) = map prt_thm ths - | prt_fact (ths, atts) = Pretty.enclose "(" ")" - (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; - - fun prt_bundle (name, bundle) = - Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name :: - Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle)); - in - map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt)) - end |> Pretty.writeln_chunks; - end; diff -r 27d51aa2d711 -r 7dd3ee7ee422 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Jun 09 12:21:15 2016 +0200 +++ b/src/Pure/Isar/local_theory.ML Thu Jun 09 15:41:49 2016 +0200 @@ -31,6 +31,7 @@ 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 @@ -195,6 +196,9 @@ 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); diff -r 27d51aa2d711 -r 7dd3ee7ee422 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Jun 09 12:21:15 2016 +0200 +++ b/src/Pure/Pure.thy Thu Jun 09 15:41:49 2016 +0200 @@ -32,6 +32,7 @@ "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl + and "bundle_target" :: thy_decl_block and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block @@ -496,6 +497,10 @@ >> (uncurry Bundle.bundle_cmd)); val _ = + Outer_Syntax.command @{command_keyword bundle_target} "define bundle of declarations" + (Parse.binding --| Parse.begin >> (Toplevel.begin_local_theory true o Bundle.init)); + +val _ = Outer_Syntax.command @{command_keyword include} "include declarations from bundle in proof body" (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));