diff --git a/src/HOL/Eisbach/method_closure.ML b/src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML +++ b/src/HOL/Eisbach/method_closure.ML @@ -1,251 +1,252 @@ (* Title: HOL/Eisbach/method_closure.ML Author: Daniel Matichuk, NICTA/UNSW Facilities for treating method syntax as a closure, with abstraction over terms, facts and other methods. The 'method' command allows to define new proof methods by combining existing ones with their usual syntax. *) signature METHOD_CLOSURE = sig val apply_method: Proof.context -> string -> term list -> thm list list -> (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic val method: binding -> (binding * typ option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory val method_cmd: binding -> (binding * string option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory end; structure Method_Closure: METHOD_CLOSURE = struct (* auxiliary data for method definition *) structure Method_Definition = Proof_Data ( type T = (Proof.context -> Method.method) Symtab.table * (*dynamic methods*) (term list -> Proof.context -> Method.method) Symtab.table (*recursive methods*); fun init _ : T = (Symtab.empty, Symtab.empty); ); fun lookup_dynamic_method ctxt full_name = (case Symtab.lookup (#1 (Method_Definition.get ctxt)) full_name of SOME m => m ctxt | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); val update_dynamic_method = Method_Definition.map o apfst o Symtab.update; fun get_recursive_method full_name ts ctxt = (case Symtab.lookup (#2 (Method_Definition.get ctxt)) full_name of SOME m => m ts ctxt | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); val put_recursive_method = Method_Definition.map o apsnd o Symtab.update; (* stored method closures *) type closure = {vars: term list, named_thms: string list, methods: string list, body: Method.text}; structure Data = Generic_Data ( type T = closure Symtab.table; val empty: T = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (K true) data; ); fun get_closure ctxt name = (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of SOME closure => closure | NONE => error ("Unknown Eisbach method: " ^ quote name)); fun put_closure binding (closure: closure) lthy = let val name = Local_Theory.full_name lthy binding; in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (name, {vars = map (Morphism.term phi) (#vars closure), named_thms = #named_thms closure, methods = #methods closure, body = (Method.map_source o map) (Token.transform phi) (#body closure)}))) end; (* instantiate and evaluate method text *) fun method_instantiate vars body ts ctxt = let val thy = Proof_Context.theory_of ctxt; val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty); val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst); val body' = (Method.map_source o map) (Token.transform morphism) body; in Method.evaluate_runtime body' ctxt end; (** apply method closure **) fun recursive_method full_name vars body ts = let val m = method_instantiate vars body in put_recursive_method (full_name, m) #> m ts end; fun apply_method ctxt method_name terms facts methods = let fun declare_facts (name :: names) (fact :: facts) = fold (Context.proof_map o Named_Theorems.add_thm name) fact #> declare_facts names facts | declare_facts _ [] = I | declare_facts [] (_ :: _) = error ("Excessive facts for method " ^ quote method_name); val {vars, named_thms, methods = method_args, body} = get_closure ctxt method_name; in declare_facts named_thms facts #> fold update_dynamic_method (method_args ~~ methods) #> recursive_method method_name vars body terms end; (** define method closure **) local fun setup_local_method binding lthy = let val full_name = Local_Theory.full_name lthy binding; fun dynamic_method ctxt = lookup_dynamic_method ctxt full_name; in lthy |> update_dynamic_method (full_name, K Method.fail) |> Method.local_setup binding (Scan.succeed dynamic_method) "(internal)" end; fun check_named_thm ctxt binding = let val bname = Binding.name_of binding; val pos = Binding.pos_of binding; val full_name = Named_Theorems.check ctxt (bname, pos); val parser: Method.modifier parser = Args.$$$ bname -- Args.colon >> K {init = I, attribute = Named_Theorems.add full_name, pos = pos}; in (full_name, parser) end; fun parse_term_args args = Args.context :|-- (fn ctxt => let val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt; fun parse T = (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt') #> Type.constraint (Type_Infer.paramify_vars T); fun do_parse' T = Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T); fun do_parse (Var (_, T)) = do_parse' T | do_parse (Free (_, T)) = do_parse' T | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t); fun rep [] x = Scan.succeed [] x | rep (t :: ts) x = (do_parse t ::: rep ts) x; fun check ts = let val (ts, fs) = split_list ts; val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt'; val _ = ListPair.app (fn (f, t) => f t) (fs, ts'); in ts' end; in Scan.lift (rep args) >> check end); fun parse_method_args method_args = let fun bind_method (name, text) ctxt = let val method = Method.evaluate_runtime text; val inner_update = method o update_dynamic_method (name, K (method ctxt)); in update_dynamic_method (name, inner_update) ctxt end; fun rep [] x = Scan.succeed [] x | rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x; in rep method_args >> fold bind_method end; fun gen_method add_fixes name vars uses declares methods source lthy = let val (uses_internal, lthy1) = lthy |> Proof_Context.concealed - |> Local_Theory.begin_target I |-> Proof_Context.private_scope + |> Local_Theory.begin_target + |-> Proof_Context.private_scope |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |> Config.put Method.old_section_parser true |> fold setup_local_method methods |> fold_map (fn b => Named_Theorems.declare b "") uses; val (term_args, lthy2) = lthy1 |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free; val (named_thms, modifiers) = map (check_named_thm lthy2) (declares @ uses) |> split_list; val method_args = map (Local_Theory.full_name lthy2) methods; fun parser args meth = apfst (Config.put_generic Method.old_section_parser true) #> (parse_term_args args -- parse_method_args method_args --| (Scan.depend (fn context => Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) -- Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl); val full_name = Local_Theory.full_name lthy name; val lthy3 = lthy2 |> Method.local_setup (Binding.make (Binding.name_of name, Position.none)) (parser term_args (get_recursive_method full_name)) "(internal)" |> put_recursive_method (full_name, fn _ => fn _ => Method.fail); val (text, src) = Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source; val morphism = Variable.export_morphism lthy3 (lthy |> Proof_Context.transfer (Proof_Context.theory_of lthy3) |> fold Token.declare_maxidx src |> Variable.declare_maxidx (Variable.maxidx_of lthy3)); val text' = (Method.map_source o map) (Token.transform morphism) text; val term_args' = map (Morphism.term morphism) term_args; in lthy3 |> Local_Theory.close_target |> Proof_Context.restore_naming lthy |> put_closure name {vars = term_args', named_thms = named_thms, methods = method_args, body = text'} |> Method.local_setup name (Args.context :|-- (fn ctxt => let val {body, vars, ...} = get_closure ctxt full_name in parser vars (recursive_method full_name vars body) end)) "" |> pair full_name end; in val method = gen_method Proof_Context.add_fixes; val method_cmd = gen_method Proof_Context.add_fixes_cmd; end; val _ = Outer_Syntax.local_theory \<^command_keyword>\method\ "Eisbach method definition" (Parse.binding -- Parse.for_fixes -- ((Scan.optional (\<^keyword>\methods\ |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- (Scan.optional (\<^keyword>\uses\ |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) -- (Scan.optional (\<^keyword>\declares\ |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- Parse.!!! (\<^keyword>\=\ |-- Parse.args1 (K true)) >> (fn ((((name, vars), (methods, uses)), declares), src) => #2 o method_cmd name vars uses declares methods src)); end; diff --git a/src/Pure/Isar/bundle.ML b/src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML +++ b/src/Pure/Isar/bundle.ML @@ -1,245 +1,242 @@ (* Title: Pure/Isar/bundle.ML Author: Makarius Bundled declarations (notes etc.). *) signature BUNDLE = sig 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 unbundle: string list -> local_theory -> local_theory val unbundle_cmd: (xstring * Position.T) list -> local_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 val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state val including: string list -> Proof.state -> Proof.state val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state val context: string list -> Element.context_i list -> generic_theory -> Binding.scope * local_theory val context_cmd: (xstring * Position.T) list -> Element.context list -> generic_theory -> Binding.scope * local_theory end; structure Bundle: BUNDLE = struct (** 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 (b, bundle) context = let val bundle' = Attrib.trim_context_thms bundle; val (name, bundles') = Name_Space.define context true (b, bundle') (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 o Attrib.trim_context_thms; 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_thm_attribs atts th = Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); fun prt_thms (ths, []) = map prt_thm ths | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; in Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ (if null bundle then [] else Pretty.fbreaks (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)); (* command *) local fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = let val (_, ctxt') = add_fixes raw_fixes lthy; val bundle0 = raw_bundle |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); val bundle = Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) end; in val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; end; (* target *) local fun bad_operation _ = error "Not possible in bundle target"; fun conclude invisible binding = Local_Theory.background_theory_result (fn thy => thy |> invisible ? Context_Position.set_visible_global false |> Context.Theory |> define_bundle (binding, the_target thy) ||> (Context.the_theory #> invisible ? Context_Position.restore_visible_global thy #> reset_target)); fun pretty binding lthy = let val bundle = the_target (Proof_Context.theory_of lthy); val (name, lthy') = lthy |> Local_Theory.raw_theory (Context_Position.set_visible_global false) |> conclude true binding; 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 (op <>) 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 |> Generic_Target.init {background_naming = Sign.naming_of thy, setup = set_target [] #> Proof_Context.init_global, conclude = conclude false binding #> #2} {define = bad_operation, notes = bundle_notes, abbrev = bad_operation, declaration = K bundle_declaration, theory_registration = bad_operation, locale_dependency = bad_operation, pretty = pretty binding} end; (** activate bundles **) local fun gen_activate notes get args ctxt = let val decls = maps (get ctxt) args in ctxt |> Context_Position.set_visible false |> notes [(Binding.empty_atts, decls)] |> #2 |> Context_Position.restore_visible ctxt end; fun gen_includes get = gen_activate (Attrib.local_notes "") get; fun gen_context get prep_decl raw_incls raw_elems gthy = let - val init = Context.cases - (pair Local_Theory.exit o Named_Target.theory_init) - (pair I o Local_Theory.assert); val import = gen_includes get raw_incls #> prep_decl ([], []) I raw_elems #> (#4 o fst); in gthy - |> init - ||> import - |-> (fn after_close => Local_Theory.begin_target after_close) + |> Context.cases Named_Target.theory_init Local_Theory.assert + |> import + |> Local_Theory.begin_target end; in val unbundle = gen_activate Local_Theory.notes get_bundle; val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd; val includes = gen_includes get_bundle; val includes_cmd = gen_includes get_bundle_cmd; fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; fun include_cmd bs = Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts; fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); val context = gen_context get_bundle Expression.cert_declaration; val context_cmd = gen_context get_bundle_cmd Expression.read_declaration; 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,416 +1,412 @@ (* 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 assert_bottom: local_theory -> local_theory val mark_brittle: local_theory -> local_theory val assert_nonbrittle: 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, exit: local_theory -> Proof.context} -> operations -> Proof.context -> local_theory val exit: local_theory -> Proof.context val exit_global: 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_target: (local_theory -> local_theory) -> local_theory -> Binding.scope * local_theory + val begin_target: local_theory -> Binding.scope * local_theory val open_target: local_theory -> local_theory val close_target: local_theory -> local_theory val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 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, after_close: local_theory -> local_theory, exit: local_theory -> Proof.context, brittle: bool, target: Proof.context}; fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy = {background_naming = background_naming, operations = operations, after_close = after_close, exit = exit, brittle = brittle, 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, after_close, exit, brittle, target} :: parents => make_lthy (f (background_naming, operations, after_close, exit, brittle, 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, after_close, exit, brittle, target}) => make_lthy (background_naming, operations, after_close, exit, brittle, target |> Context_Position.set_visible false |> f (n - i - 1) |> Context_Position.restore_visible target)) |> f n end; (* brittle context -- implicit for nested structures *) fun mark_brittle lthy = if level lthy = 1 then map_top (fn (background_naming, operations, after_close, exit, _, target) => (background_naming, operations, after_close, exit, true, target)) lthy else lthy; fun assert_nonbrittle lthy = if #brittle (top_of lthy) then error "Brittle local theory context" else lthy; (* naming for background theory *) val background_naming_of = #background_naming o top_of; fun map_background_naming f = map_top (fn (background_naming, operations, after_close, exit, brittle, target) => (f background_naming, operations, after_close, exit, brittle, 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 {background_naming, exit} operations target = target |> Data.map (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)] | _ => error "Local theory already initialized"); val exit_of = #exit o bottom_of; fun exit lthy = exit_of lthy lthy; val exit_global = Proof_Context.theory_of o exit; 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 init_target {background_naming, after_close} operations lthy = +fun begin_target lthy = let val _ = assert lthy; - val after_close' = Proof_Context.restore_naming lthy #> after_close; val (scope, target) = Proof_Context.new_scope lthy; - val entry = make_lthy (background_naming, operations, after_close', exit_of lthy, true, target); + val entry = make_lthy (background_naming_of lthy, operations_of lthy, + Proof_Context.restore_naming lthy, exit_of lthy, true, target); val lthy' = Data.map (cons entry) target; in (scope, lthy') end; -fun begin_target after_close lthy = - init_target {background_naming = background_naming_of lthy, after_close = after_close} - (operations_of lthy) lthy; - -val open_target = begin_target I #> #2; +val open_target = begin_target #> snd; fun close_target lthy = let val _ = assert_not_bottom lthy; val ({after_close, ...} :: rest) = Data.get lthy; in lthy |> Data.put rest |> reset |> after_close end; fun subtarget body = open_target #> body #> close_target; fun subtarget_result decl body lthy = let val (x, inner_lthy) = lthy |> open_target |> body; val lthy' = inner_lthy |> close_target; val phi = Proof_Context.export_morphism inner_lthy lthy'; in (decl phi x, lthy') end; end; diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML +++ b/src/Pure/Isar/toplevel.ML @@ -1,795 +1,795 @@ (* Title: Pure/Isar/toplevel.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar toplevel transactions. *) signature TOPLEVEL = sig exception UNDEF type state val init_toplevel: unit -> state val theory_toplevel: theory -> state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int val is_end_theory: state -> bool val end_theory: Position.T -> state -> theory val presentation_context: state -> Proof.context val presentation_state: Proof.context -> state val pretty_context: state -> Pretty.T list val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T type transition val empty: transition val name_of: transition -> string val pos_of: transition -> Position.T val timing_of: transition -> Time.time val type_error: transition -> string val name: string -> transition -> transition val position: Position.T -> transition -> transition val markers: Input.source list -> transition -> transition val timing: Time.time -> transition -> transition val init_theory: (unit -> theory) -> transition -> transition val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition val ignored: Position.T -> transition val is_ignored: transition -> bool val malformed: Position.T -> string -> transition val generic_theory: (generic_theory -> generic_theory) -> transition -> transition val theory': (bool -> theory -> theory) -> transition -> transition val theory: (theory -> theory) -> transition -> transition val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition val end_main_target: transition -> transition val begin_nested_target: (generic_theory -> local_theory) -> transition -> transition val end_nested_target: transition -> transition val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> Proof.state) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (unit -> unit) -> transition -> transition val skip_proof_open: transition -> transition val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state val reset_theory: state -> state option val reset_proof: state -> state option val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result val join_results: result -> (transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; structure Toplevel: TOPLEVEL = struct (** toplevel state **) exception UNDEF = Runtime.UNDEF; (* datatype node *) datatype node = Toplevel (*toplevel outside of theory body*) | Theory of generic_theory (*global or local theory*) | Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | Skipped_Proof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) val theory_node = fn Theory gthy => SOME gthy | _ => NONE; val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; fun cases_node f _ _ Toplevel = f () | cases_node _ g _ (Theory gthy) = g gthy | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf) | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy; fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h; val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of); (* datatype state *) type node_presentation = node * Proof.context; fun init_presentation () = Proof_Context.init_global (Theory.get_pure_bootstrap ()); fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); datatype state = State of node_presentation * theory option; (*current node with presentation context, previous theory*) fun node_of (State ((node, _), _)) = node; fun previous_theory_of (State (_, prev_thy)) = prev_thy; fun init_toplevel () = State (node_presentation Toplevel, NONE); fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); fun level state = (case node_of state of Toplevel => 0 | Theory _ => 0 | Proof (prf, _) => Proof.level (Proof_Node.current prf) | Skipped_Proof (d, _) => d + 1); (*different notion of proof depth!*) fun str_of_state state = (case node_of state of Toplevel => (case previous_theory_of state of NONE => "at top level" | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy)) | Theory (Context.Theory _) => "in theory mode" | Theory (Context.Proof _) => "in local theory mode" | Proof _ => "in proof mode" | Skipped_Proof _ => "in skipped proof mode"); (* current node *) fun is_toplevel state = (case node_of state of Toplevel => true | _ => false); fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state; fun proper_node_case f g state = cases_proper_node f g (proper_node_of state); val context_of = proper_node_case Context.proof_of Proof.context_of; val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of); val theory_of = proper_node_case Context.theory_of Proof.theory_of; val proof_of = proper_node_case (fn _ => error "No proof state") I; fun proof_position_of state = (case proper_node_of state of Proof (prf, _) => Proof_Node.position prf | _ => ~1); fun is_end_theory (State ((Toplevel, _), SOME _)) = true | is_end_theory _ = false; fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); (* presentation context *) structure Presentation_State = Proof_Data ( type T = state option; fun init _ = NONE; ); fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt; fun presentation_context (state as State (current, _)) = presentation_context0 state |> Presentation_State.put (SOME (State (current, NONE))); fun presentation_state ctxt = (case Presentation_State.get ctxt of NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) | SOME state => state); (* print state *) fun pretty_context state = if is_toplevel state then [] else let val gthy = (case node_of state of Toplevel => raise Match | Theory gthy => gthy | Proof (_, (_, gthy)) => gthy | Skipped_Proof (_, (_, gthy)) => gthy); val lthy = Context.cases Named_Target.theory_init I gthy; in Local_Theory.pretty lthy end; fun pretty_state state = (case node_of state of Toplevel => [] | Theory _ => [] | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf) | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; fun pretty_abstract state = Pretty.str (""); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); (** toplevel transitions **) (* primitive transitions *) datatype trans = (*init theory*) Init of unit -> theory | (*formal exit of theory*) Exit | (*peek at state*) Keep of bool -> state -> unit | (*node transaction and presentation*) Transaction of (bool -> node -> node_presentation) * (state -> unit); local exception FAILURE of state * exn; fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; fun state_error e node_pr' = (State (node_pr', get_theory node), e); val (result, err) = node |> Runtime.controlled_execution (SOME context) f |> state_error NONE handle exn => state_error (SOME exn) node_pr; in (case err of NONE => tap g result | SOME exn => raise FAILURE (result, exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = node |> apply (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) (K ()); in State ((Toplevel, pr_ctxt), get_theory node') end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g node | _ => raise UNDEF); fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = apply_union int trs state handle Runtime.UNDEF => apply_tr int tr state | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) = let val state' = Runtime.controlled_execution (try generic_theory_of state) (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) (); in (state', NONE) end handle exn => (state, SOME exn); in fun apply_trans int name markers trans state = (apply_union int trans state |> apply_markers name markers) handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); end; (* datatype transition *) datatype transition = Transition of {name: string, (*command name*) pos: Position.T, (*source position*) markers: Input.source list, (*semantic document markers*) timing: Time.time, (*prescient timing information*) trans: trans list}; (*primitive transitions (union)*) fun make_transition (name, pos, markers, timing, trans) = Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans}; fun map_transition f (Transition {name, pos, markers, timing, trans}) = make_transition (f (name, pos, markers, timing, trans)); val empty = make_transition ("", Position.none, [], Time.zeroTime, []); (* diagnostics *) fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; fun timing_of (Transition {timing, ...}) = timing; fun command_msg msg tr = msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ Position.here (pos_of tr); fun at_command tr = command_msg "At " tr; fun type_error tr = command_msg "Bad context for " tr; (* modify transitions *) fun name name = map_transition (fn (_, pos, markers, timing, trans) => (name, pos, markers, timing, trans)); fun position pos = map_transition (fn (name, _, markers, timing, trans) => (name, pos, markers, timing, trans)); fun markers markers = map_transition (fn (name, pos, _, timing, trans) => (name, pos, markers, timing, trans)); fun timing timing = map_transition (fn (name, pos, markers, _, trans) => (name, pos, markers, timing, trans)); fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) => (name, pos, markers, timing, tr :: trans)); val reset_trans = map_transition (fn (name, pos, markers, timing, _) => (name, pos, markers, timing, [])); (* basic transitions *) fun init_theory f = add_trans (Init f); fun is_init (Transition {trans = [Init _], ...}) = true | is_init _ = false; fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; val exit = add_trans Exit; val keep' = add_trans o Keep; fun present_transaction f g = add_trans (Transaction (f, g)); fun transaction f = present_transaction f (K ()); fun transaction0 f = present_transaction (node_presentation oo f) (K ()); fun keep f = add_trans (Keep (fn _ => f)); fun keep_proof f = keep (fn st => if is_proof st then f st else if is_skipped_proof st then () else warning "No proof state"); fun ignored pos = empty |> name "" |> position pos |> keep (fn _ => ()); fun is_ignored tr = name_of tr = ""; fun malformed pos msg = empty |> name "" |> position pos |> keep (fn _ => error msg); (* theory transitions *) fun generic_theory f = transaction (fn _ => (fn Theory gthy => node_presentation (Theory (f gthy)) | _ => raise UNDEF)); fun theory' f = transaction (fn int => (fn Theory (Context.Theory thy) => let val thy' = thy |> Sign.new_group |> f int |> Sign.reset_group; in node_presentation (Theory (Context.Theory thy')) end | _ => raise UNDEF)); fun theory f = theory' (K f); fun begin_main_target begin f = transaction (fn _ => (fn Theory (Context.Theory thy) => let val lthy = f thy; val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy); val _ = (case Local_Theory.pretty lthy of [] => () | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); in (Theory gthy, lthy) end | _ => raise UNDEF)); val end_main_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy) | _ => raise UNDEF)); fun begin_nested_target f = transaction0 (fn _ => (fn Theory gthy => let val lthy = f gthy in Theory (Context.Proof lthy) end | _ => raise UNDEF)); val end_nested_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (case try Local_Theory.close_target lthy of - SOME ctxt' => + SOME lthy' => let val gthy' = - if can Local_Theory.assert ctxt' - then Context.Proof ctxt' - else Context.Theory (Proof_Context.theory_of ctxt'); + if Named_Target.is_theory lthy' + then Context.Theory (Local_Theory.exit_global lthy') + else Context.Proof lthy' in (Theory gthy', lthy) end | NONE => raise UNDEF) | _ => raise UNDEF)); fun restricted_context (SOME (strict, scope)) = Proof_Context.map_naming (Name_Space.restricted strict scope) | restricted_context NONE = I; fun local_theory' restricted target f = present_transaction (fn int => (fn Theory gthy => let val (finish, lthy) = Named_Target.switch target gthy; val lthy' = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int |> Local_Theory.reset_group; in (Theory (finish lthy'), lthy') end | _ => raise UNDEF)) (K ()); fun local_theory restricted target f = local_theory' restricted target (K f); fun present_local_theory target = present_transaction (fn _ => (fn Theory gthy => let val (finish, lthy) = Named_Target.switch target gthy; in (Theory (finish lthy), lthy) end | _ => raise UNDEF)); (* proof transitions *) fun end_proof f = transaction (fn int => (fn Proof (prf, (finish, _)) => let val state = Proof_Node.current prf in if can (Proof.assert_bottom true) state then let val ctxt' = f int state; val gthy' = finish ctxt'; in (Theory gthy', ctxt') end else raise UNDEF end | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy) | _ => raise UNDEF)); local fun begin_proof init_proof = transaction0 (fn int => (fn Theory gthy => let val (finish, prf) = init_proof int gthy; val document = Options.default_string "document"; val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled (); val schematic_goal = try Proof.schematic_goal prf; val _ = if skip andalso schematic_goal = SOME true then warning "Cannot skip proof of schematic goal statement" else (); in if skip andalso schematic_goal = SOME false then Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' restricted target f = begin_proof (fn int => fn gthy => let val (finish, lthy) = Named_Target.switch target gthy; val prf = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int; in (finish o Local_Theory.reset_group, prf) end); fun local_theory_to_proof restricted target f = local_theory_to_proof' restricted target (K f); fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end; val forget_proof = transaction0 (fn _ => (fn Proof (prf, (_, orig_gthy)) => if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF else Theory orig_gthy | Skipped_Proof (_, (_, orig_gthy)) => Theory orig_gthy | _ => raise UNDEF)); fun proofs' f = transaction0 (fn int => (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K; (* skipped proofs *) fun actual_proof f = transaction0 (fn _ => (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); fun skip_proof f = transaction0 (fn _ => (fn skip as Skipped_Proof _ => (f (); skip) | _ => raise UNDEF)); val skip_proof_open = transaction0 (fn _ => (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) | _ => raise UNDEF)); val skip_proof_close = transaction0 (fn _ => (fn Skipped_Proof (0, (gthy, _)) => Theory gthy | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x) | _ => raise UNDEF)); (** toplevel transactions **) (* runtime position *) fun exec_id id (tr as Transition {pos, ...}) = position (Position.put_id (Document_ID.print id) pos) tr; fun setmp_thread_position (Transition {pos, ...}) f x = Position.setmp_thread_data pos f x; (* post-transition hooks *) local val hooks = Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); in fun add_hook hook = Synchronized.change hooks (cons hook); fun get_hooks () = Synchronized.value hooks; end; (* apply transitions *) local fun app int (tr as Transition {name, markers, trans, ...}) = setmp_thread_position tr (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans) ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); in fun transition int tr st = let val (st', opt_err) = Context.setmp_generic_context (try (Context.Proof o presentation_context0) st) (fn () => app int tr st) (); val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ())); in (st', opt_err') end; end; (* managed commands *) fun command_errors int tr st = (case transition int tr st of (st', NONE) => ([], SOME st') | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE)); fun command_exception int tr st = (case transition int tr st of (st', NONE) => st' | (_, SOME (exn, info)) => if Exn.is_interrupt exn then Exn.reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)); val command = command_exception false; (* reset state *) local fun reset_state check trans st = if check st then NONE else #2 (command_errors false (trans empty) st); in val reset_theory = reset_state is_theory forget_proof; val reset_proof = reset_state is_proof (transaction0 (fn _ => (fn Theory gthy => Skipped_Proof (0, (gthy, gthy)) | _ => raise UNDEF))); val reset_notepad = reset_state (fn st => (case try proof_of st of SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state | NONE => true)) (proof Proof.reset_notepad); end; (* scheduled proof result *) datatype result = Result of transition * state | Result_List of result list | Result_Future of result future; fun join_results (Result x) = [x] | join_results (Result_List xs) = maps join_results xs | join_results (Result_Future x) = join_results (Future.join x); local structure Result = Proof_Data ( type T = result; fun init _ = Result_List []; ); val get_result = Result.get o Proof.context_of; val put_result = Proof.map_context o Result.put; fun timing_estimate elem = let val trs = tl (Thy_Element.flat_element elem) in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end; fun future_proofs_enabled estimate st = (case try proof_of st of NONE => false | SOME state => not (Proofterm.proofs_enabled ()) andalso not (Proof.is_relevant state) andalso (if can (Proof.assert_bottom true) state then Future.proofs_enabled 1 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); val empty_markers = markers []; val empty_trans = reset_trans #> keep (K ()); in fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans); fun atom_result keywords tr st = let val st' = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then let val (tr1, tr2) = fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} (fn () => command tr1 st); in command tr2 st end else command tr st; in (Result (tr, st'), st') end; fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st = let val (head_result, st') = atom_result keywords head_tr st; val (body_elems, end_tr) = element_rest; val estimate = timing_estimate elem; in if not (future_proofs_enabled estimate st') then let val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr]; val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; in (Result_List (head_result :: proof_results), st'') end else let val (end_tr1, end_tr2) = fork_presentation end_tr; val finish = Context.Theory o Proof_Context.theory_of; val future_proof = Proof.future_proof (fn state => Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} (fn () => let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy)); val (results, result_state) = State (node_presentation node', prev_thy) |> fold_map (element_result keywords) body_elems ||> command end_tr1; in (Result_List results, presentation_context0 result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); val forked_proof = proof (future_proof #> (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o end_proof (fn _ => future_proof #> (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); val st'' = st' |> command (head_tr |> reset_trans |> forked_proof); val end_st = st'' |> command end_tr2; val end_result = Result (end_tr, end_st); val result = Result_List [head_result, Result.get (presentation_context0 st''), end_result]; in (result, end_st) end end; end; end; structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;