diff --git a/src/Pure/Isar/attrib.ML b/src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML +++ b/src/Pure/Isar/attrib.ML @@ -1,646 +1,653 @@ (* Title: Pure/Isar/attrib.ML Author: Markus Wenzel, TU Muenchen Symbolic representation of attributes -- with name and syntax. *) signature ATTRIB = sig type thms = Attrib.thms type fact = Attrib.fact val print_attributes: bool -> Proof.context -> unit val attribute_space: Context.generic -> Name_Space.T val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory val check_name_generic: Context.generic -> xstring * Position.T -> string val check_name: Proof.context -> xstring * Position.T -> string val check_src: Proof.context -> Token.src -> Token.src val attribs: Token.src list context_parser val opt_attribs: Token.src list context_parser val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list val pretty_binding: Proof.context -> Attrib.binding -> string -> Pretty.T list val attribute: Proof.context -> Token.src -> attribute val attribute_global: theory -> Token.src -> attribute val attribute_cmd: Proof.context -> Token.src -> attribute val attribute_cmd_global: theory -> Token.src -> attribute val map_specs: ('a list -> 'att list) -> (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list val map_facts: ('a list -> 'att list) -> (('c * 'a list) * ('d * 'a list) list) list -> (('c * 'att list) * ('d * 'att list) list) list val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) -> (('c * 'a list) * ('b * 'a list) list) list -> (('c * 'att list) * ('fact * 'att list) list) list val trim_context_binding: Attrib.binding -> Attrib.binding val trim_context_thms: thms -> thms val trim_context_fact: fact -> fact val global_notes: string -> fact list -> theory -> (string * thm list) list * theory val local_notes: string -> fact list -> Proof.context -> (string * thm list) list * Proof.context val generic_notes: string -> fact list -> Context.generic -> (string * thm list) list * Context.generic val lazy_notes: string -> binding * thm list lazy -> Context.generic -> Context.generic val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list val attribute_syntax: attribute context_parser -> Token.src -> attribute val setup: binding -> attribute context_parser -> string -> theory -> theory val local_setup: binding -> attribute context_parser -> string -> local_theory -> local_theory val attribute_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory val internal: (morphism -> attribute) -> Token.src val internal_declaration: declaration -> thms val add_del: attribute -> attribute -> attribute context_parser val thm: thm context_parser val thms: thm list context_parser val multi_thm: thm list context_parser val transform_facts: morphism -> fact list -> fact list val partial_evaluation: Proof.context -> fact list -> fact list val print_options: bool -> Proof.context -> unit val config_bool: binding -> (Context.generic -> bool) -> bool Config.T * (theory -> theory) val config_int: binding -> (Context.generic -> int) -> int Config.T * (theory -> theory) val config_real: binding -> (Context.generic -> real) -> real Config.T * (theory -> theory) val config_string: binding -> (Context.generic -> string) -> string Config.T * (theory -> theory) val setup_config_bool: binding -> (Context.generic -> bool) -> bool Config.T val setup_config_int: binding -> (Context.generic -> int) -> int Config.T val setup_config_real: binding -> (Context.generic -> real) -> real Config.T val setup_config_string: binding -> (Context.generic -> string) -> string Config.T val option_bool: string * Position.T -> bool Config.T * (theory -> theory) val option_int: string * Position.T -> int Config.T * (theory -> theory) val option_real: string * Position.T -> real Config.T * (theory -> theory) val option_string: string * Position.T -> string Config.T * (theory -> theory) val setup_option_bool: string * Position.T -> bool Config.T val setup_option_int: string * Position.T -> int Config.T val setup_option_real: string * Position.T -> real Config.T val setup_option_string: string * Position.T -> string Config.T val consumes: int -> Token.src val constraints: int -> Token.src val cases_open: Token.src val case_names: string list -> Token.src val case_conclusion: string * string list -> Token.src end; structure Attrib: sig type binding = Attrib.binding include ATTRIB end = struct open Attrib; (** named attributes **) (* theory data *) structure Attributes = Generic_Data ( type T = ((Token.src -> attribute) * string) Name_Space.table; val empty : T = Name_Space.empty_table Markup.attributeN; fun merge data : T = Name_Space.merge_tables data; ); val ops_attributes = {get_data = Attributes.get, put_data = Attributes.put}; val get_attributes = Attributes.get o Context.Proof; fun print_attributes verbose ctxt = let val attribs = get_attributes ctxt; fun prt_attr (name, (_, "")) = Pretty.mark_str name | prt_attr (name, (_, comment)) = Pretty.block (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); in [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))] |> Pretty.writeln_chunks end; val attribute_space = Name_Space.space_of_table o Attributes.get; (* define *) fun define_global binding att comment = Entity.define_global ops_attributes binding (att, comment); fun define binding att comment = Entity.define ops_attributes binding (att, comment); (* check *) fun check_name_generic context = #1 o Name_Space.check context (Attributes.get context); val check_name = check_name_generic o Context.Proof; fun check_src ctxt src = let val _ = if Token.checked_src src then () else Context_Position.report ctxt (#1 (Token.range_of src)) Markup.language_attribute; in #1 (Token.check_src ctxt get_attributes src) end; val attribs = Args.context -- Scan.lift Parse.attribs >> (fn (ctxt, srcs) => map (check_src ctxt) srcs); val opt_attribs = Scan.optional attribs []; (* pretty printing *) fun pretty_attribs _ [] = [] | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)]; fun pretty_binding ctxt (b, atts) sep = (case (Binding.is_empty b, null atts) of (true, true) => [] | (false, true) => [Pretty.block [Binding.pretty b, Pretty.str sep]] | (true, false) => [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])] | (false, false) => [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])]); (* get attributes *) fun attribute_generic context = let val table = Attributes.get context in fn src => let val name = #1 (Token.name_of_src src); val label = Long_Name.qualify Markup.attributeN name; val att = #1 (Name_Space.get table name) src; in Position.setmp_thread_data_label label att end end; val attribute = attribute_generic o Context.Proof; val attribute_global = attribute_generic o Context.Theory; fun attribute_cmd ctxt = attribute ctxt o check_src ctxt; fun attribute_cmd_global thy = attribute_global thy o check_src (Proof_Context.init_global thy); (* attributed declarations *) fun map_specs f = map (apfst (apsnd f)); fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f))); fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g))); -(* fact expressions *) +(* implicit context *) -val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src); -val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context; +val trim_context_binding: Attrib.binding -> Attrib.binding = + apsnd ((map o map) Token.trim_context); + +val trim_context_thms: thms -> thms = + map (fn (thms, atts) => (map Thm.trim_context thms, (map o map) Token.trim_context atts)); + fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms); + +(* fact expressions *) + fun global_notes kind facts thy = thy |> Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts); fun local_notes kind facts ctxt = ctxt |> Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts); fun generic_notes kind facts context = context |> Context.mapping_result (global_notes kind facts) (local_notes kind facts); fun lazy_notes kind arg = Context.mapping (Global_Theory.add_thms_lazy kind arg) (Proof_Context.add_thms_lazy kind arg); fun eval_thms ctxt srcs = ctxt |> Proof_Context.note_thmss "" (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) [(Binding.empty_atts, srcs)]) |> fst |> maps snd; (* attribute setup *) fun attribute_syntax scan src (context, th) = let val (a, context') = Token.syntax_generic scan src context in a (context', th) end; fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; fun attribute_setup binding source comment = ML_Context.expression (Input.pos_of source) (ML_Lex.read ("Theory.local_setup (Attrib.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @ ML_Lex.read_source source @ ML_Lex.read (") " ^ ML_Syntax.print_string comment ^ ")")) |> Context.proof_map; (* internal attribute *) val _ = Theory.setup (setup (Binding.make ("attribute", \<^here>)) (Scan.lift Args.internal_attribute >> Morphism.form) "internal attribute"); fun internal_name ctxt name = Token.make_src (name, Position.none) [] |> check_src ctxt |> hd; val internal_attribute_name = internal_name (Context.the_local_context ()) "attribute"; fun internal att = internal_attribute_name :: [Token.make_string ("", Position.none) |> Token.assign (SOME (Token.Attribute att))]; fun internal_declaration decl = [([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])]; (* add/del syntax *) fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add); (** parsing attributed theorems **) local val fact_name = Parse.position Args.internal_fact >> (fn (_, pos) => ("", pos)) || Args.name_position; fun gen_thm pick = Scan.depend (fn context => let val get = Proof_Context.get_fact_generic context; val get_fact = get o Facts.Fact; fun get_named is_sel pos name = let val (a, ths) = get (Facts.Named ((name, pos), NONE)) in (if is_sel then NONE else a, ths) end; in Parse.$$$ "[" |-- Scan.pass context attribs --| Parse.$$$ "]" >> (fn srcs => let val atts = map (attribute_generic context) srcs; val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context); in (context', pick ("", Position.none) [th']) end) || (Scan.ahead Args.alt_name -- Args.named_fact get_fact >> (fn (s, fact) => ("", Facts.Fact s, fact)) || Scan.ahead (fact_name -- Scan.option Parse.thm_sel) :|-- (fn ((name, pos), sel) => Args.named_fact (get_named (is_some sel) pos) --| Scan.option Parse.thm_sel >> (fn fact => (name, Facts.Named ((name, pos), sel), fact)))) -- Scan.pass context opt_attribs >> (fn ((name, thmref, fact), srcs) => let val ths = Facts.select thmref fact; val atts = map (attribute_generic context) srcs; val (ths', context') = fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; in (context', pick (name, Facts.ref_pos thmref) ths') end) end); in val thm = gen_thm Facts.the_single; val multi_thm = gen_thm (K I); val thms = Scan.repeats multi_thm; end; (* transform fact expressions *) fun transform_facts phi = map (fn ((a, atts), bs) => ((Morphism.binding phi a, (map o map) (Token.transform phi) atts), bs |> map (fn (ths, btts) => (Morphism.fact phi ths, (map o map) (Token.transform phi) btts)))); (** partial evaluation -- observing rule/declaration/mixed attributes **) (*NB: result length may change due to rearrangement of symbolic expression*) local fun apply_att src (context, th) = let val src1 = map Token.init_assignable src; val result = attribute_generic context src1 (context, th); val src2 = map Token.closure src1; in (src2, result) end; fun err msg src = let val (name, pos) = Token.name_of_src src in error (msg ^ " " ^ quote name ^ Position.here pos) end; fun eval src ((th, dyn), (decls, context)) = (case (apply_att src (context, th), dyn) of ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context)) | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src | ((src', (SOME context', NONE)), NONE) => let val decls' = (case decls of [] => [(th, [src'])] | (th2, srcs2) :: rest => if Thm.eq_thm_strict (th, th2) then ((th2, src' :: srcs2) :: rest) else (th, [src']) :: (th2, srcs2) :: rest); in ((th, NONE), (decls', context')) end | ((src', (opt_context', opt_th')), _) => let val context' = the_default context opt_context'; val th' = the_default th opt_th'; val dyn' = (case dyn of NONE => SOME (th, [src']) | SOME (dyn_th, srcs) => SOME (dyn_th, src' :: srcs)); in ((th', dyn'), (decls, context')) end); in fun partial_evaluation ctxt facts = (facts, Context.Proof (Context_Position.not_really ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn context => let val (fact', (decls, context')) = (fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 => (ths, res1) |-> fold_map (fn th => fn res2 => let val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2); val th_atts' = (case dyn' of NONE => (th', []) | SOME (dyn_th', atts') => (dyn_th', rev atts')); in (th_atts', res3) end)) |>> flat; val decls' = rev (map (apsnd rev) decls); val facts' = if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')] else if null decls' then [((b, []), fact')] else [(Binding.empty_atts, decls'), ((b, []), fact')]; in (facts', context') end) |> fst |> flat |> map (apsnd (map (apfst single))) |> filter_out (fn (b, fact) => Binding.is_empty_atts b andalso forall (null o #2) fact); end; (** configuration options **) (* naming *) structure Configs = Theory_Data ( type T = Config.value Config.T Symtab.table; val empty = Symtab.empty; fun merge data = Symtab.merge (K true) data; ); fun print_options verbose ctxt = let fun prt (name, config) = let val value = Config.get ctxt config in Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="), Pretty.brk 1, Pretty.str (Config.print_value value)] end; val space = attribute_space (Context.Proof ctxt); val configs = Name_Space.markup_entries verbose ctxt space (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt))); in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; (* concrete syntax *) local val equals = Parse.$$$ "="; fun scan_value (Config.Bool _) = equals -- Args.$$$ "false" >> K (Config.Bool false) || equals -- Args.$$$ "true" >> K (Config.Bool true) || Scan.succeed (Config.Bool true) | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real | scan_value (Config.String _) = equals |-- Args.name >> Config.String; fun scan_config thy config = let val config_type = Config.get_global thy config in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end; fun register binding config thy = let val name = Sign.full_name thy binding in thy |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option" |> Configs.map (Symtab.update (name, config)) end; fun declare make coerce binding default = let val name = Binding.name_of binding; val pos = Binding.pos_of binding; val config_value = Config.declare (name, pos) (make o default); val config = coerce config_value; in (config, register binding config_value) end; in fun register_config config = register (Binding.make (Config.name_of config, Config.pos_of config)) config; val register_config_bool = register_config o Config.bool_value; val register_config_int = register_config o Config.int_value; val register_config_real = register_config o Config.real_value; val register_config_string = register_config o Config.string_value; val config_bool = declare Config.Bool Config.bool; val config_int = declare Config.Int Config.int; val config_real = declare Config.Real Config.real; val config_string = declare Config.String Config.string; end; (* implicit setup *) local fun setup_config declare_config binding default = let val (config, setup) = declare_config binding default; val _ = Theory.setup setup; in config end; in val setup_config_bool = setup_config config_bool; val setup_config_int = setup_config config_int; val setup_config_string = setup_config config_string; val setup_config_real = setup_config config_real; end; (* system options *) local fun declare_option coerce (name, pos) = let val config = Config.declare_option (name, pos); in (coerce config, register_config config) end; fun setup_option coerce (name, pos) = let val config = Config.declare_option (name, pos); val _ = Theory.setup (register_config config); in coerce config end; in val option_bool = declare_option Config.bool; val option_int = declare_option Config.int; val option_real = declare_option Config.real; val option_string = declare_option Config.string; val setup_option_bool = setup_option Config.bool; val setup_option_int = setup_option Config.int; val setup_option_real = setup_option Config.real; val setup_option_string = setup_option Config.string; end; (* theory setup *) val _ = Theory.setup (setup \<^binding>\tagged\ (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #> setup \<^binding>\untagged\ (Scan.lift Args.name >> Thm.untag) "untagged theorem" #> setup \<^binding>\kind\ (Scan.lift Args.name >> Thm.kind) "theorem kind" #> setup \<^binding>\THEN\ (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))) "resolution with rule" #> setup \<^binding>\OF\ (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))) "rule resolved with facts" #> setup \<^binding>\rename_abs\ (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))) "rename bound variables in abstractions" #> setup \<^binding>\unfolded\ (thms >> (fn ths => Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))) "unfolded definitions" #> setup \<^binding>\folded\ (thms >> (fn ths => Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))) "folded definitions" #> setup \<^binding>\consumes\ (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes) "number of consumed facts" #> setup \<^binding>\constraints\ (Scan.lift Parse.nat >> Rule_Cases.constraints) "number of equality constraints" #> setup \<^binding>\cases_open\ (Scan.succeed Rule_Cases.cases_open) "rule with open parameters" #> setup \<^binding>\case_names\ (Scan.lift (Scan.repeat (Args.name -- Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [])) >> (fn cs => Rule_Cases.cases_hyp_names (map #1 cs) (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))) "named rule cases" #> setup \<^binding>\case_conclusion\ (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion) "named conclusion of rule cases" #> setup \<^binding>\params\ (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params) "named rule parameters" #> setup \<^binding>\rule_format\ (Scan.lift (Args.mode "no_asm") >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)) "result put into canonical rule format" #> setup \<^binding>\elim_format\ (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))) "destruct rule turned into elimination rule format" #> setup \<^binding>\no_vars\ (Scan.succeed (Thm.rule_attribute [] (Variable.import_vars o Context.proof_of))) "imported schematic variables" #> setup \<^binding>\atomize\ (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #> setup \<^binding>\rulify\ (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #> setup \<^binding>\rotated\ (Scan.lift (Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #> setup \<^binding>\defn\ (add_del Local_Defs.defn_add Local_Defs.defn_del) "declaration of definitional transformations" #> setup \<^binding>\abs_def\ (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of))) "abstract over free variables of definitional theorem" #> register_config_bool Goal.quick_and_dirty #> register_config_bool Ast.trace #> register_config_bool Ast.stats #> register_config_bool Printer.show_brackets #> register_config_bool Printer.show_sorts #> register_config_bool Printer.show_types #> register_config_bool Printer.show_markup #> register_config_bool Printer.show_structs #> register_config_bool Printer.show_question_marks #> register_config_bool Syntax.ambiguity_warning #> register_config_int Syntax.ambiguity_limit #> register_config_bool Syntax_Trans.eta_contract #> register_config_bool Name_Space.names_long #> register_config_bool Name_Space.names_short #> register_config_bool Name_Space.names_unique #> register_config_int ML_Print_Depth.print_depth #> register_config_string ML_Env.ML_environment #> register_config_bool ML_Env.ML_read_global #> register_config_bool ML_Env.ML_write_global #> register_config_bool ML_Options.source_trace #> register_config_bool ML_Options.exception_trace #> register_config_bool ML_Options.exception_debugger #> register_config_bool ML_Options.debugger #> register_config_bool Proof_Context.show_abbrevs #> register_config_int Goal_Display.goals_limit #> register_config_bool Goal_Display.show_main_goal #> register_config_bool Thm.show_consts #> register_config_bool Thm.show_hyps #> register_config_bool Thm.show_tags #> register_config_bool Pattern.unify_trace_failure #> register_config_int Unify.trace_bound #> register_config_int Unify.search_bound #> register_config_bool Unify.trace_simp #> register_config_bool Unify.trace_types #> register_config_int Raw_Simplifier.simp_depth_limit #> register_config_int Raw_Simplifier.simp_trace_depth_limit #> register_config_bool Raw_Simplifier.simp_debug #> register_config_bool Raw_Simplifier.simp_trace #> register_config_bool Local_Defs.unfold_abs_def); (* internal source *) local val internal = internal_name (Context.the_local_context ()); val consumes_name = internal "consumes"; val constraints_name = internal "constraints"; val cases_open_name = internal "cases_open"; val case_names_name = internal "case_names"; val case_conclusion_name = internal "case_conclusion"; fun make_string s = Token.make_string (s, Position.none); in fun consumes i = consumes_name :: Token.make_int i; fun constraints i = constraints_name :: Token.make_int i; val cases_open = [cases_open_name]; fun case_names names = case_names_name :: map make_string names; fun case_conclusion (name, names) = case_conclusion_name :: map make_string (name :: names); end; end; \ No newline at end of file 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,236 +1,247 @@ (* Title: Pure/Isar/bundle.ML Author: Makarius Bundled declarations (notes etc.). *) signature BUNDLE = sig type name = string val bundle_space: Context.generic -> Name_Space.T val check: Proof.context -> xstring * Position.T -> string val get: Proof.context -> name -> Attrib.thms val read: Proof.context -> xstring * Position.T -> Attrib.thms val extern: Proof.context -> string -> xstring 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: name list -> local_theory -> local_theory val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory val includes: name list -> Proof.context -> Proof.context val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context val include_: name list -> Proof.state -> Proof.state val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state val including: name list -> Proof.state -> Proof.state val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state 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 Markup.bundleN, NONE); fun merge ((tab1, target1), (tab2, target2)) = (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); ); (* bundles *) type name = string val get_all_generic = #1 o Data.get; val get_all = get_all_generic o Context.Proof; val bundle_space = Name_Space.space_of_table o #1 o Data.get; fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt); val get = Name_Space.get o get_all_generic o Context.Proof; fun read ctxt = get ctxt o check ctxt; fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all 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_all_generic context); - val context' = (Data.map o apfst o K) bundles' context; - in (name, context') end; - (* target -- bundle under construction *) fun the_target thy = #2 (Data.get (Context.Theory thy)) |> \<^if_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_all ctxt))); (** define bundle **) +(* context and morphisms *) + +val trim_context_bundle = + map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts)); + +fun transfer_bundle thy = + map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts)); + fun transform_bundle phi = map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); +fun define_bundle (b, bundle) context = + let + val (name, bundles') = get_all_generic context + |> Name_Space.define context true (b, trim_context_bundle bundle); + val context' = (Data.map o apfst o K) bundles' context; + in (name, context') end; + (* 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_all 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 |> Local_Theory.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 prep_bundle args ctxt = - let val decls = maps (prep_bundle ctxt) args in + let + val thy = Proof_Context.theory_of ctxt; + val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy; + in ctxt |> Context_Position.set_visible false - |> notes [(Binding.empty_atts, transform_bundle (Morphism.transfer_morphism' ctxt) decls)] |> #2 + |> notes [(Binding.empty_atts, decls)] |> #2 |> Context_Position.restore_visible ctxt end; fun gen_unbundle prep_bundle = gen_activate Local_Theory.notes prep_bundle; fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle; fun gen_include prep_bundle bs = Proof.assert_forward #> Proof.map_context (gen_includes prep_bundle bs) #> Proof.reset_facts; fun gen_including prep_bundle bs = Proof.assert_backward #> Proof.map_context (gen_includes prep_bundle bs) in val unbundle = gen_unbundle get; val unbundle_cmd = gen_unbundle read; val includes = gen_includes get; val includes_cmd = gen_includes read; val include_ = gen_include get; val include_cmd = gen_include read; val including = gen_including get; val including_cmd = gen_including read; end; end; diff --git a/src/Pure/Isar/class.ML b/src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML +++ b/src/Pure/Isar/class.ML @@ -1,841 +1,844 @@ (* Title: Pure/Isar/class.ML Author: Florian Haftmann, TU Muenchen Type classes derived from primitive axclasses and locales. *) signature CLASS = sig (*classes*) val is_class: theory -> class -> bool val these_params: theory -> sort -> (string * (class * (string * typ))) list val base_sort: theory -> class -> sort val rules: theory -> class -> thm option * thm val these_defs: theory -> sort -> thm list val these_operations: theory -> sort -> (string * (class * ((typ * term) * bool))) list val print_classes: Proof.context -> unit val init: class -> theory -> Proof.context val begin: class list -> sort -> Proof.context -> Proof.context val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val redeclare_operations: theory -> sort -> Proof.context -> Proof.context val class_prefix: string -> string val register: class -> class list -> ((string * typ) * (string * typ)) list -> sort -> morphism -> morphism -> thm option -> thm option -> thm -> theory -> theory (*instances*) val instantiation: string list * (string * sort) list * sort -> theory -> local_theory val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory val prove_instantiation_exit: (Proof.context -> tactic) -> local_theory -> theory val prove_instantiation_exit_result: (morphism -> 'a -> 'b) -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory val read_multi_arity: theory -> xstring list * xstring list * xstring -> string list * (string * sort) list * sort val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state val theory_map_result: string list * (string * sort) list * sort -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> (Proof.context -> 'b -> tactic) -> theory -> 'b * theory (*subclasses*) val classrel: class * class -> theory -> Proof.state val classrel_cmd: xstring * xstring -> theory -> Proof.state val register_subclass: class * class -> morphism option -> Element.witness option -> morphism -> local_theory -> local_theory (*tactics*) val intro_classes_tac: Proof.context -> thm list -> tactic val standard_intro_classes_tac: Proof.context -> thm list -> tactic (*diagnostics*) val pretty_specification: theory -> class -> Pretty.T list end; structure Class: CLASS = struct (** class data **) datatype class_data = Class_Data of { (* static part *) consts: (string * string) list (*locale parameter ~> constant name*), base_sort: sort, base_morph: morphism (*static part of canonical morphism*), export_morph: morphism, assm_intro: thm option, of_class: thm, axiom: thm option, (* dynamic part *) defs: thm Item_Net.T, operations: (string * (class * ((typ * term) * bool))) list (* n.b. params = logical parameters of class operations = operations participating in user-space type system *) }; fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), (defs, operations)) = Class_Data {consts = consts, base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom, defs = defs, operations = operations}; fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom, defs, operations}) = make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), (defs, operations))); fun merge_class_data _ (Class_Data {consts = consts, base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom, defs = defs1, operations = operations1}, Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, of_class = _, axiom = _, defs = defs2, operations = operations2}) = make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), (Item_Net.merge (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2))); structure Class_Data = Theory_Data ( type T = class_data Graph.T val empty = Graph.empty; val merge = Graph.join merge_class_data; ); (* queries *) fun lookup_class_data thy class = (case try (Graph.get_node (Class_Data.get thy)) class of SOME (Class_Data data) => SOME data | NONE => NONE); fun the_class_data thy class = lookup_class_data thy class |> \<^if_none>\error ("Undeclared class " ^ quote class)\; val is_class = is_some oo lookup_class_data; val ancestry = Graph.all_succs o Class_Data.get; val heritage = Graph.all_preds o Class_Data.get; fun these_params thy = let fun params class = let val const_typs = (#params o Axclass.get_info thy) class; val const_names = (#consts o the_class_data thy) class; in (map o apsnd) (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names end; in maps params o ancestry thy end; val base_sort = #base_sort oo the_class_data; fun rules thy class = let val {axiom, of_class, ...} = the_class_data thy class in (axiom, of_class) end; fun all_assm_intros thy = Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm) (the_list assm_intro)) (Class_Data.get thy) []; fun these_defs thy = maps (Item_Net.content o #defs o the_class_data thy) o ancestry thy; fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; val base_morphism = #base_morph oo the_class_data; fun morphism thy class = base_morphism thy class $> Morphism.default (Element.eq_morphism thy (these_defs thy [class])); val export_morphism = #export_morph oo the_class_data; fun pretty_param ctxt (c, ty) = Pretty.block [Name_Space.pretty ctxt (Proof_Context.const_space ctxt) c, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt ty]; fun print_classes ctxt = let val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val class_space = Proof_Context.class_space ctxt; val type_space = Proof_Context.type_space ctxt; val arities = Symtab.build (Sorts.arities_of algebra |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => Symtab.map_default (class, []) (insert (op =) tyco)) arities)); fun prt_supersort class = Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class)); fun prt_arity class tyco = let val Ss = Sorts.mg_domain algebra tyco [class]; in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty); fun prt_entry class = Pretty.block ([Pretty.keyword1 "class", Pretty.brk 1, Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ (case (these o Option.map #params o try (Axclass.get_info thy)) class of [] => [] | params => [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ (case (these o Symtab.lookup arities) class of [] => [] | ars => [Pretty.fbrk, Pretty.big_list "instances:" (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))])); in Sorts.all_classes algebra |> sort (Name_Space.extern_ord ctxt class_space) |> map prt_entry |> Pretty.writeln_chunks2 end; (* updaters *) fun register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class thy = let val operations = map (fn (v_ty as (_, ty), (c, _)) => (c, (class, ((ty, Free v_ty), false)))) params; val add_class = Graph.new_node (class, make_class_data (((map o apply2) fst params, base_sort, - base_morph, export_morph, Option.map Thm.trim_context some_assm_intro, - Thm.trim_context of_class, Option.map Thm.trim_context some_axiom), + Morphism.reset_context base_morph, + Morphism.reset_context export_morph, + Option.map Thm.trim_context some_assm_intro, + Thm.trim_context of_class, + Option.map Thm.trim_context some_axiom), (Thm.item_net, operations))) #> fold (curry Graph.add_edge class) sups; in Class_Data.map add_class thy end; fun activate_defs class thms thy = (case Element.eq_morphism thy thms of SOME eq_morph => fold (fn cls => fn thy' => (Context.theory_map o Locale.amend_registration) {inst = (cls, base_morphism thy' cls), mixin = SOME (eq_morph, true), export = export_morphism thy' cls} thy') (heritage thy [class]) thy | NONE => thy); fun register_operation class (c, t) input_only thy = let val base_sort = base_sort thy class; val prep_typ = map_type_tfree (fn (v, sort) => if Name.aT = v then TFree (v, base_sort) else TVar ((v, 0), sort)); val t' = map_types prep_typ t; val ty' = Term.fastype_of t'; in thy |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apsnd) (cons (c, (class, ((ty', t'), input_only)))) end; fun register_def class def_thm thy = let val sym_thm = Thm.trim_context (Thm.symmetric def_thm) in thy |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst) (Item_Net.update sym_thm) |> activate_defs class [sym_thm] end; (** classes and class target **) (* class context syntax *) fun make_rewrite t c_ty = let val vs = strip_abs_vars t; val vts = map snd vs |> Name.invent_names Name.context Name.uu |> map (fn (v, T) => Var ((v, 0), T)); in (betapplys (t, vts), betapplys (Const c_ty, vts)) end; fun these_unchecks thy = these_operations thy #> map_filter (fn (c, (_, ((ty, t), input_only))) => if input_only then NONE else SOME (make_rewrite t (c, ty))); fun these_unchecks_reversed thy = these_operations thy #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t)); fun redeclare_const thy c = let val b = Long_Name.base_name c in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; fun synchronize_class_syntax sort base_sort ctxt = let val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val operations = these_operations thy sort; fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); val primary_constraints = (map o apsnd) (subst_class_typ base_sort o fst o fst o snd) operations; val secondary_constraints = (map o apsnd) (fn (class, ((ty, _), _)) => subst_class_typ [class] ty) operations; fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) of SOME (_, ty' as TVar (vi, sort)) => if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort) then SOME (ty', Term.aT base_sort) else NONE | _ => NONE) | NONE => NONE) | NONE => NONE); fun subst (c, _) = Option.map (fst o snd) (AList.lookup (op =) operations c); val unchecks = these_unchecks thy sort; in ctxt |> fold (redeclare_const thy o fst) primary_constraints |> Overloading.map_improvable_syntax (K {primary_constraints = primary_constraints, secondary_constraints = secondary_constraints, improve = improve, subst = subst, no_subst_in_abbrev_mode = true, unchecks = unchecks}) |> Overloading.set_primary_constraints end; fun synchronize_class_syntax_target class lthy = lthy |> Local_Theory.map_contexts (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class))); fun redeclare_operations thy sort = fold (redeclare_const thy o fst) (these_operations thy sort); fun begin sort base_sort ctxt = ctxt |> Variable.declare_term (Logic.mk_type (Term.aT base_sort)) |> synchronize_class_syntax sort base_sort |> Overloading.activate_improvable_syntax; fun init class thy = thy |> Locale.init class |> begin [class] (base_sort thy class); (* class target *) val class_prefix = Logic.const_of_class o Long_Name.base_name; fun guess_morphism_identity (b, rhs) phi1 phi2 = let (*FIXME proper concept to identify morphism instead of educated guess*) val name_of_binding = Name_Space.full_name Name_Space.global_naming; val n1 = (name_of_binding o Morphism.binding phi1) b; val n2 = (name_of_binding o Morphism.binding phi2) b; val rhs1 = Morphism.term phi1 rhs; val rhs2 = Morphism.term phi2 rhs; in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end; fun target_const class phi0 prmode (b, rhs) lthy = let val export = Variable.export_morphism lthy (Local_Theory.target_of lthy); val guess_identity = guess_morphism_identity (b, rhs) export; val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0); in lthy |> Generic_Target.locale_target_const class (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs) end; local fun dangling_params_for lthy class (type_params, term_params) = let val class_param_names = map fst (these_params (Proof_Context.theory_of lthy) [class]); val dangling_term_params = subtract (fn (v, Free (w, _)) => v = w | _ => false) class_param_names term_params; in (type_params, dangling_term_params) end; fun global_def (b, eq) thy = let val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq); val def_thm' = def_thm |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 |> Thm.varifyT_global; val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm'); in (def_thm', thy'') end; fun canonical_const class phi dangling_params ((b, mx), rhs) thy = let val b_def = Binding.suffix_name "_dict" b; val c = Sign.full_name thy b; val ty = map Term.fastype_of dangling_params ---> Term.fastype_of rhs; val def_eq = Logic.mk_equals (list_comb (Const (c, ty), dangling_params), rhs) |> map_types Type.strip_sorts; in thy |> Sign.declare_const_global ((b, Type.strip_sorts ty), mx) |> snd |> global_def (b_def, def_eq) |-> (fn def_thm => register_def class def_thm) |> null dangling_params ? register_operation class (c, rhs) false |> Sign.add_const_constraint (c, SOME ty) end; in fun const class ((b, mx), lhs) params lthy = let val phi = morphism (Proof_Context.theory_of lthy) class; val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params)); in lthy |> target_const class phi Syntax.mode_default (b, lhs) |> Local_Theory.raw_theory (canonical_const class phi dangling_params ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs)) |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs) |> synchronize_class_syntax_target class end; end; local fun canonical_abbrev class phi prmode with_syntax ((b, mx), rhs) thy = let val c = Sign.full_name thy b; val constrain = map_atyps (fn T as TFree (v, _) => if v = Name.aT then TFree (v, [class]) else T | T => T); val rhs' = map_types constrain rhs; in thy |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs') |> snd |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)] |> with_syntax ? register_operation class (c, rhs) (#1 prmode = Print_Mode.input) |> Sign.add_const_constraint (c, SOME (fastype_of rhs')) end; fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy = let val thy = Proof_Context.theory_of lthy; val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) [])); val (global_rhs, (_, (_, term_params))) = Generic_Target.export_abbrev lthy preprocess rhs; val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx; in lthy |> Local_Theory.raw_theory (canonical_abbrev class phi prmode (null term_params) ((Morphism.binding phi b, mx'), Logic.unvarify_types_global global_rhs)) end; fun further_abbrev_target class phi prmode (b, mx) rhs params = Generic_Target.background_abbrev (b, rhs) (snd params) #-> (fn (lhs, _) => target_const class phi prmode (b, lhs) #> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), lhs)) in fun abbrev class prmode ((b, mx), rhs) lthy = let val thy = Proof_Context.theory_of lthy; val phi = morphism thy class; val rhs_generic = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs; in lthy |> canonical_abbrev_target class phi prmode ((b, mx), rhs) |> Generic_Target.abbrev (further_abbrev_target class phi) prmode ((b, mx), rhs_generic) ||> synchronize_class_syntax_target class end; end; (* subclasses *) fun register_subclass (sub, sup) some_dep_morph some_witn export lthy = let val thy = Proof_Context.theory_of lthy; val conclude_witness = Thm.trim_context o Drule.export_without_context_open o Element.conclude_witness lthy; val intros = (snd o rules thy) sup :: map_filter I [Option.map conclude_witness some_witn, (fst o rules thy) sub]; val classrel = Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup)) (fn {context = ctxt, ...} => EVERY (map (TRYALL o resolve_tac ctxt o single) intros)); val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]) |> filter (is_class thy); val add_dependency = (case some_dep_morph of SOME dep_morph => Generic_Target.locale_dependency sub {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)), mixin = NONE, export = export} | NONE => I); in lthy |> Local_Theory.raw_theory (Axclass.add_classrel classrel #> Class_Data.map (Graph.add_edge (sub, sup)) #> activate_defs sub (these_defs thy diff_sort)) |> add_dependency |> synchronize_class_syntax_target sub end; local fun gen_classrel mk_prop classrel thy = let fun after_qed results = Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results); in thy |> Proof_Context.init_global |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] end; in val classrel = gen_classrel (Logic.mk_classrel oo Axclass.cert_classrel); val classrel_cmd = gen_classrel (Logic.mk_classrel oo Axclass.read_classrel); end; (*local*) (** instantiation target **) (* bookkeeping *) datatype instantiation = Instantiation of { arities: string list * (string * sort) list * sort, params: ((string * string) * (string * typ)) list (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) } fun make_instantiation (arities, params) = Instantiation {arities = arities, params = params}; val empty_instantiation = make_instantiation (([], [], []), []); structure Instantiation = Proof_Data ( type T = instantiation; fun init _ = empty_instantiation; ); val get_instantiation = (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of; fun map_instantiation f = (Local_Theory.target o Instantiation.map) (fn Instantiation {arities, params} => make_instantiation (f (arities, params))); fun the_instantiation lthy = (case get_instantiation lthy of {arities = ([], [], []), ...} => error "No instantiation target" | data => data); val instantiation_params = #params o get_instantiation; fun instantiation_param lthy b = instantiation_params lthy |> find_first (fn (_, (v, _)) => Binding.name_of b = v) |> Option.map (fst o fst); fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = let val ctxt = Proof_Context.init_global thy; val all_arities = map (fn raw_tyco => Proof_Context.read_arity ctxt (raw_tyco, raw_sorts, raw_sort)) raw_tycos; val tycos = map #1 all_arities; val (_, sorts, sort) = hd all_arities; val vs = Name.invent_names Name.context Name.aT sorts; in (tycos, vs, sort) end; (* syntax *) fun synchronize_inst_syntax ctxt = let val Instantiation {params, ...} = Instantiation.get ctxt; val lookup_inst_param = Axclass.lookup_inst_param (Sign.consts_of (Proof_Context.theory_of ctxt)) params; fun subst (c, ty) = (case lookup_inst_param (c, ty) of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) | NONE => NONE); val unchecks = map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; in ctxt |> Overloading.map_improvable_syntax (fn {primary_constraints, improve, ...} => {primary_constraints = primary_constraints, secondary_constraints = [], improve = improve, subst = subst, no_subst_in_abbrev_mode = false, unchecks = unchecks}) end; fun resort_terms ctxt algebra consts constraints ts = let fun matchings (Const (c_ty as (c, _))) = (case constraints c of NONE => I | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts) | matchings _ = I; val tvartab = Vartab.build ((fold o fold_aterms) matchings ts) handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e); val inst = map_type_tvar (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end; (* target *) fun define_overloaded (c, U) b (b_def, rhs) lthy = let val name = Binding.name_of b; val pos = Binding.pos_of b; val _ = if Context_Position.is_reported lthy pos then Position.report_text pos Markup.class_parameter (Pretty.string_of (Pretty.block [Pretty.keyword1 "class", Pretty.brk 1, Pretty.str "parameter", Pretty.brk 1, pretty_param lthy (c, U)])) else (); in lthy |> Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U) ##>> Axclass.define_overloaded b_def (c, rhs)) ||> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = name)) ||> Local_Theory.map_contexts (K synchronize_inst_syntax) end; fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case instantiation_param lthy b of SOME c => if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) b (b_def, rhs) else error ("Illegal mixfix syntax for overloaded constant " ^ quote c) | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let val {arities = (tycos, vs, sort), params} = the_instantiation lthy; fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); fun pr_param ((c, _), (v, ty)) = Pretty.block (Pretty.breaks [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c, Pretty.str "::", Syntax.pretty_typ lthy ty]); in [Pretty.block (Pretty.fbreaks (Pretty.keyword1 "instantiation" :: map pr_arity tycos @ map pr_param params))] end; fun conclude lthy = let val (tycos, vs, sort) = #arities (the_instantiation lthy); val thy = Proof_Context.theory_of lthy; val _ = tycos |> List.app (fn tyco => if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then () else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco))); in lthy end; fun registration thy_ctxt {inst, mixin, export} lthy = lthy |> Generic_Target.theory_registration {inst = inst, mixin = mixin, export = export $> Proof_Context.export_morphism lthy thy_ctxt} (*handle fixed types variables on target context properly*); fun instantiation (tycos, vs, sort) thy = let val _ = if null tycos then error "At least one arity must be given" else (); val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort); fun get_param tyco (param, (_, (c, ty))) = if can (Axclass.param_of_inst thy) (c, tyco) then NONE else SOME ((c, tyco), (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); val params = map_product get_param tycos class_params |> map_filter I; val _ = if null params andalso forall (fn tyco => can (Sign.arity_sorts thy tyco) sort) tycos then error "No parameters and no pending instance proof obligations in instantiation." else (); val primary_constraints = map (apsnd (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; val algebra = Sign.classes_of thy |> fold (fn tyco => Sorts.add_arities (Context.Theory thy) (tyco, map (fn class => (class, map snd vs)) sort)) tycos; val consts = Sign.consts_of thy; val improve_constraints = AList.lookup (op =) (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts; val lookup_inst_param = Axclass.lookup_inst_param consts params; fun improve (c, ty) = (case lookup_inst_param (c, ty) of SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE | NONE => NONE); in thy |> Local_Theory.init {background_naming = Sign.naming_of thy, setup = Proof_Context.init_global #> Instantiation.put (make_instantiation ((tycos, vs, sort), params)) #> fold (Variable.declare_typ o TFree) vs #> fold (Variable.declare_names o Free o snd) params #> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints, secondary_constraints = [], improve = improve, subst = K NONE, no_subst_in_abbrev_mode = false, unchecks = []}) #> Overloading.activate_improvable_syntax #> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check) #> synchronize_inst_syntax, conclude = conclude} {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, declaration = K Generic_Target.theory_declaration, theory_registration = registration (Proof_Context.init_global thy), locale_dependency = fn _ => error "Not possible in instantiation target", pretty = pretty} end; fun instantiation_cmd arities thy = instantiation (read_multi_arity thy arities) thy; fun gen_instantiation_instance do_proof after_qed lthy = let val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = Local_Theory.background_theory (fold (Axclass.add_arity o Thm.varifyT_global) results) #> after_qed; in lthy |> do_proof after_qed' arities_proof end; val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t (fn {context, ...} => tac context)) ts) lthy) I; fun prove_instantiation_exit tac = prove_instantiation_instance tac #> Local_Theory.exit_global; fun prove_instantiation_exit_result f tac x lthy = let val morph = Proof_Context.export_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy)); val y = f morph x; in lthy |> prove_instantiation_exit (fn ctxt => tac ctxt y) |> pair y end; fun theory_map_result arities f g tac = instantiation arities #> g #-> prove_instantiation_exit_result f tac; (* simplified instantiation interface with no class parameter *) fun instance_arity_cmd raw_arities thy = let val (tycos, vs, sort) = read_multi_arity thy raw_arities; val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed results = Proof_Context.background_theory ((fold o fold) Axclass.add_arity results); in thy |> Proof_Context.init_global |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) end; (** tactics and methods **) fun intro_classes_tac ctxt facts st = let val thy = Proof_Context.theory_of ctxt; val classes = Sign.all_classes thy; val class_trivs = map (Thm.class_triv thy) classes; val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes; val assm_intros = all_assm_intros thy; in Method.intros_tac ctxt (class_trivs @ class_intros @ assm_intros) facts st end; fun standard_intro_classes_tac ctxt facts st = if null facts andalso not (Thm.no_prems st) then (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac {strict = true, eager = true} ctxt []) st else no_tac st; fun standard_tac ctxt facts = HEADGOAL (Method.some_rule_tac ctxt [] facts) ORELSE standard_intro_classes_tac ctxt facts; val _ = Theory.setup (Method.setup \<^binding>\intro_classes\ (Scan.succeed (METHOD o intro_classes_tac)) "back-chain introduction rules of classes" #> Method.setup \<^binding>\standard\ (Scan.succeed (METHOD o standard_tac)) "standard proof step: Pure intro/elim rule or class introduction"); (** diagnostics **) fun pretty_specification thy class = if is_class thy class then let val class_ctxt = init class thy; val prt_class = Name_Space.pretty class_ctxt (Proof_Context.class_space class_ctxt); val super_classes = Sign.minimize_sort thy (Sign.super_classes thy class); val fix_args = #params (Axclass.get_info thy class) |> map (fn (c, T) => (Binding.name (Long_Name.base_name c), SOME T, NoSyn)); val fixes = if null fix_args then [] else [Element.Fixes fix_args]; val assumes = Locale.hyp_spec_of thy class; val header = [Pretty.keyword1 "class", Pretty.brk 1, prt_class class, Pretty.str " =", Pretty.brk 1] @ Pretty.separate " +" (map prt_class super_classes) @ (if null super_classes then [] else [Pretty.str " +"]); val body = if null fixes andalso null assumes then [] else maps (Element.pretty_ctxt_no_attribs class_ctxt) (fixes @ assumes) |> maps (fn prt => [Pretty.fbrk, prt]); in if null body then [] else [Pretty.block (header @ body)] end else []; end; diff --git a/src/Pure/Isar/element.ML b/src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML +++ b/src/Pure/Isar/element.ML @@ -1,477 +1,489 @@ (* Title: Pure/Isar/element.ML Author: Makarius Explicit data structures for some Isar language elements, with derived logical operations. *) signature ELEMENT = sig type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list) type obtains = (string, string) obtain list type obtains_i = (typ, term) obtain list datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | Obtains of ('typ, 'term) obtain list type statement = (string, string) stmt type statement_i = (typ, term) stmt datatype ('typ, 'term, 'fact) ctxt = Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | Notes of string * (Attrib.binding * ('fact * Token.src list) list) list | Lazy_Notes of string * (binding * 'fact lazy) type context = (string, string, Facts.ref) ctxt type context_i = (typ, term, thm list) ctxt val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b, pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Token.src -> Token.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt val map_ctxt_attrib: (Token.src -> Token.src) -> ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt + val trim_context_ctxt: context_i -> context_i + val transfer_ctxt: theory -> context_i -> context_i val transform_ctxt: morphism -> context_i -> context_i val pretty_stmt: Proof.context -> statement_i -> Pretty.T list val pretty_ctxt: Proof.context -> context_i -> Pretty.T list val pretty_ctxt_no_attribs: Proof.context -> context_i -> Pretty.T list val pretty_statement: Proof.context -> string -> thm -> Pretty.T type witness val prove_witness: Proof.context -> term -> tactic -> witness val witness_proof: (witness list list -> Proof.context -> Proof.context) -> term list list -> Proof.context -> Proof.state val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) -> term list list -> term list -> Proof.context -> Proof.state val witness_local_proof: (witness list list -> Proof.state -> Proof.state) -> string -> term list list -> Proof.context -> Proof.state -> Proof.state val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) -> string -> term list list -> term list -> Proof.context -> Proof.state -> Proof.state val transform_witness: morphism -> witness -> witness val conclude_witness: Proof.context -> witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism val satisfy_morphism: witness list -> morphism val eq_term_morphism: theory -> term list -> morphism option val eq_morphism: theory -> thm list -> morphism option val init: context_i -> Context.generic -> Context.generic val activate_i: context_i -> Proof.context -> context_i * Proof.context val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context end; structure Element: ELEMENT = struct (** language elements **) (* statement *) type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list); type obtains = (string, string) obtain list; type obtains_i = (typ, term) obtain list; datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | Obtains of ('typ, 'term) obtain list; type statement = (string, string) stmt; type statement_i = (typ, term) stmt; (* context *) datatype ('typ, 'term, 'fact) ctxt = Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | Notes of string * (Attrib.binding * ('fact * Token.src list) list) list | Lazy_Notes of string * (binding * 'fact lazy); type context = (string, string, Facts.ref) ctxt; type context_i = (typ, term, thm list) ctxt; fun map_ctxt {binding, typ, term, pattern, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => (Variable.check_name (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => ((binding a, map attrib atts), (term t, map pattern ps)))) | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))) | Lazy_Notes (kind, (a, ths)) => Lazy_Notes (kind, (binding a, Lazy.map fact ths)); fun map_ctxt_attrib attrib = map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib}; +val trim_context_ctxt: context_i -> context_i = map_ctxt + {binding = I, typ = I, term = I, pattern = I, + fact = map Thm.trim_context, + attrib = map Token.trim_context}; + +fun transfer_ctxt thy: context_i -> context_i = map_ctxt + {binding = I, typ = I, term = I, pattern = I, + fact = map (Thm.transfer thy), + attrib = map (Token.transfer thy)}; + fun transform_ctxt phi = map_ctxt {binding = Morphism.binding phi, typ = Morphism.typ phi, term = Morphism.term phi, pattern = Morphism.term phi, fact = Morphism.fact phi, attrib = map (Token.transform phi)}; (** pretty printing **) fun pretty_items _ _ [] = [] | pretty_items keyword sep (x :: ys) = Pretty.block [Pretty.keyword2 keyword, Pretty.brk 1, x] :: map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword2 sep, Pretty.brk 1, y]) ys; (* pretty_stmt *) fun pretty_stmt ctxt = let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; val prt_terms = separate (Pretty.keyword2 "and") o map prt_term; val prt_binding = Attrib.pretty_binding ctxt; val prt_name = Proof_Context.pretty_name ctxt; fun prt_show (a, ts) = Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts))); fun prt_var (x, SOME T, _) = Pretty.block [prt_name (Binding.name_of x), Pretty.str " ::", Pretty.brk 1, prt_typ T] | prt_var (x, NONE, _) = prt_name (Binding.name_of x); val prt_vars = separate (Pretty.keyword2 "and") o map prt_var; fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props)) | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props)); in fn Shows shows => pretty_items "shows" "and" (map prt_show shows) | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains) end; (* pretty_ctxt *) fun gen_pretty_ctxt show_attribs ctxt = let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; val prt_name = Proof_Context.pretty_name ctxt; fun prt_binding (b, atts) = Attrib.pretty_binding ctxt (b, if show_attribs then atts else []); fun prt_fact (ths, atts) = if not show_attribs orelse null atts then map prt_thm ths else Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; fun prt_mixfix NoSyn = [] | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx]; fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" :: Pretty.brk 1 :: prt_typ T :: prt_mixfix mx) | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx); fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); fun prt_asm (a, ts) = Pretty.block (Pretty.breaks (prt_binding a ":" @ map (prt_term o fst) ts)); fun prt_def (a, (t, _)) = Pretty.block (Pretty.breaks (prt_binding a ":" @ [prt_term t])); fun prt_note (a, ths) = Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths))); fun notes_kind "" = "notes" | notes_kind kind = "notes " ^ kind; in fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) | Defines defs => pretty_items "defines" "and" (map prt_def defs) | Notes (kind, facts) => pretty_items (notes_kind kind) "and" (map prt_note facts) | Lazy_Notes (kind, (a, ths)) => pretty_items (notes_kind kind) "and" [prt_note ((a, []), [(Lazy.force ths, [])])] end; val pretty_ctxt = gen_pretty_ctxt true; val pretty_ctxt_no_attribs = gen_pretty_ctxt false; (* pretty_statement *) local fun standard_elim ctxt th = (case Object_Logic.elim_concl ctxt th of SOME C => let val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); val insts = (TVars.empty, Vars.make1 (Term.dest_Var C, Thm.cterm_of ctxt thesis)); val th' = Thm.instantiate insts th; in (th', true) end | NONE => (th, false)); fun thm_name ctxt kind th prts = let val head = if Thm.has_name_hint th then Pretty.block [Pretty.keyword1 kind, Pretty.brk 1, Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"] else Pretty.keyword1 kind in Pretty.block (Pretty.fbreaks (head :: prts)) end; fun obtain prop ctxt = let val ((ps, prop'), ctxt') = Variable.focus NONE prop ctxt; fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn); val xs = map (fix o #2) ps; val As = Logic.strip_imp_prems prop'; in ((Binding.empty, (xs, As)), ctxt') end; in fun pretty_statement ctxt kind raw_th = let val (th, is_elim) = standard_elim ctxt (Raw_Simplifier.norm_hhf ctxt raw_th); val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt); val prop = Thm.prop_of th'; val (prems, concl) = Logic.strip_horn prop; val concl_term = Object_Logic.drop_judgment ctxt concl; val (assumes, cases) = chop_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems; val is_thesis = if null cases then K false else fn v => v aconv concl_term; val fixes = rev (fold_aterms (fn v as Free (x, T) => if Variable.is_newly_fixed ctxt' ctxt x andalso not (is_thesis v) then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop []); in pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @ pretty_ctxt ctxt' (Assumes (map (fn t => (Binding.empty_atts, [(t, [])])) assumes)) @ (if null cases then pretty_stmt ctxt' (Shows [(Binding.empty_atts, [(concl, [])])]) else let val (clauses, ctxt'') = fold_map obtain cases ctxt' in pretty_stmt ctxt'' (Obtains clauses) end) end |> thm_name ctxt kind raw_th; end; (** logical operations **) (* witnesses -- hypotheses as protected facts *) datatype witness = Witness of term * thm; val mark_witness = Logic.protect; fun witness_prop (Witness (t, _)) = t; fun witness_hyps (Witness (_, th)) = Thm.hyps_of th; fun map_witness f (Witness witn) = Witness (f witn); fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); fun prove_witness ctxt t tac = Witness (t, Goal.prove ctxt [] [] (mark_witness t) (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac) |> Thm.close_derivation \<^here> |> Thm.trim_context); local val refine_witness = Proof.refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI])))))))); fun gen_witness_proof proof after_qed wit_propss eq_props = let val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss @ [map (rpair []) eq_props]; fun after_qed' thmss = let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here> #> Thm.trim_context) thmss); in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness end; fun proof_local cmd goal_ctxt after_qed propp = let fun after_qed' (result_ctxt, results) state' = after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state'; in Proof.map_context (K goal_ctxt) #> Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd NONE after_qed' [] [] (map (pair Binding.empty_atts) propp) #> snd end; in fun witness_proof after_qed wit_propss = gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits) wit_propss []; val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE); fun witness_local_proof after_qed cmd wit_propss goal_ctxt = gen_witness_proof (proof_local cmd goal_ctxt) (fn wits => fn _ => after_qed wits) wit_propss []; fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt = gen_witness_proof (proof_local cmd goal_ctxt) after_qed wit_propss eq_props; end; fun conclude_witness ctxt (Witness (_, th)) = Goal.conclude (Thm.transfer' ctxt th) |> Raw_Simplifier.norm_hhf_protect ctxt |> Thm.close_derivation \<^here>; fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in Pretty.block (prt_term (witness_prop witn) :: (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]" (map prt_term (witness_hyps witn))] else [])) end; (* instantiate frees, with beta normalization *) fun instantiate_normalize_morphism insts = Morphism.instantiate_frees_morphism insts $> Morphism.term_morphism "beta_norm" Envir.beta_norm $> Morphism.thm_morphism "beta_conversion" (Conv.fconv_rule (Thm.beta_conversion true)); (* satisfy hypotheses *) local val norm_term = Envir.beta_eta_contract; val norm_conv = Drule.beta_eta_conversion; val norm_cterm = Thm.rhs_of o norm_conv; fun find_witness witns hyp = (case find_first (fn Witness (t, _) => hyp aconv t) witns of NONE => let val hyp' = norm_term hyp in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end | some => some); fun compose_witness (Witness (_, th)) r = let val th' = Goal.conclude (Thm.transfer (Thm.theory_of_thm r) th); val A = Thm.cprem_of r 1; in Thm.implies_elim (Conv.gconv_rule norm_conv 1 r) (Conv.fconv_rule norm_conv (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th')) end; in fun satisfy_thm witns thm = (Thm.chyps_of thm, thm) |-> fold (fn hyp => (case find_witness witns (Thm.term_of hyp) of NONE => I | SOME w => Thm.implies_intr hyp #> compose_witness w)); val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm; end; (* rewriting with equalities *) (* for activating declarations only *) fun eq_term_morphism _ [] = NONE | eq_term_morphism thy props = let (* FIXME proper morphism context *) fun decomp_simp prop = let val ctxt = Proof_Context.init_global thy; val _ = Logic.no_prems prop orelse error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop); val lhsrhs = Logic.dest_equals prop handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop); in lhsrhs end; val phi = Morphism.morphism "Element.eq_term_morphism" {binding = [], typ = [], term = [K (Pattern.rewrite_term thy (map decomp_simp props) [])], fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]}; in SOME phi end; fun eq_morphism _ [] = NONE | eq_morphism thy thms = let (* FIXME proper morphism context *) fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th; val phi = Morphism.morphism "Element.eq_morphism" {binding = [], typ = [], term = [K (Raw_Simplifier.rewrite_term thy thms [])], fact = [K (map rewrite)]}; in SOME phi end; (** activate in context **) (* init *) fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2) | init (Constrains _) = I | init (Assumes asms) = Context.map_proof (fn ctxt => let val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms; val (_, ctxt') = ctxt |> fold Proof_Context.augment (maps (map #1 o #2) asms') |> Proof_Context.add_assms Assumption.assume_export asms'; in ctxt' end) | init (Defines defs) = Context.map_proof (fn ctxt => let val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; val asms = defs' |> map (fn (b, (t, ps)) => let val (_, t') = Local_Defs.cert_def ctxt (K []) t (* FIXME adapt ps? *) in (t', (b, [(t', ps)])) end); val (_, ctxt') = ctxt |> fold Proof_Context.augment (map #1 asms) |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms); in ctxt' end) | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2 | init (Lazy_Notes (kind, ths)) = Attrib.lazy_notes kind ths; (* activate *) fun activate_i elem ctxt = let val elem' = (case (map_ctxt_attrib o map) Token.init_assignable elem of Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), (t, ps)))) | e => e); val ctxt' = Context.proof_map (init elem') ctxt; in ((map_ctxt_attrib o map) Token.closure elem', ctxt') end; fun activate raw_elem ctxt = let val elem = raw_elem |> map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = Proof_Context.get_fact ctxt, attrib = Attrib.check_src ctxt} in activate_i elem ctxt end; end; diff --git a/src/Pure/Isar/expression.ML b/src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML +++ b/src/Pure/Isar/expression.ML @@ -1,881 +1,881 @@ (* Title: Pure/Isar/expression.ML Author: Clemens Ballarin, TU Muenchen Locale expressions and user interface layer of locales. *) signature EXPRESSION = sig (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list type 'term rewrites = (Attrib.binding * 'term) list type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list type expression_i = (string, term) expr * (binding * typ option * mixfix) list type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list (* Processing of context statements *) val cert_statement: Element.context_i list -> Element.statement_i -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context val read_statement: Element.context list -> Element.statement -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context (* Declaring locales *) val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val add_locale: binding -> binding -> Bundle.name list -> expression_i -> Element.context_i list -> theory -> string * local_theory val add_locale_cmd: binding -> binding -> (xstring * Position.T) list -> expression -> Element.context list -> theory -> string * local_theory (* Processing of locale expressions *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context end; structure Expression : EXPRESSION = struct datatype ctxt = datatype Element.ctxt; (*** Expressions ***) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list; type 'term rewrites = (Attrib.binding * 'term) list; type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list; type expression_i = (string, term) expr * (binding * typ option * mixfix) list; type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list; (** Internalise locale names in expr **) fun check_expr thy instances = map (apfst (Locale.check thy)) instances; (** Parameters of expression **) (*Sanity check of instantiations and extraction of implicit parameters. The latter only occurs iff strict = false. Positional instantiations are extended to match full length of parameter list of instantiated locale.*) fun parameters_of thy strict (expr, fixed) = let val ctxt = Proof_Context.init_global thy; fun reject_dups message xs = (case duplicates (op =) xs of [] => () | dups => error (message ^ commas dups)); fun parm_eq ((p1, mx1), (p2, mx2)) = p1 = p2 andalso (Mixfix.equal (mx1, mx2) orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); fun params_inst (loc, (prfx, (Positional insts, eqns))) = let val ps = params_loc loc; val d = length ps - length insts; val insts' = if d < 0 then error ("More arguments than parameters in instantiation of locale " ^ quote (Locale.markup_name ctxt loc)) else insts @ replicate d NONE; val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); in (ps', (loc, (prfx, (Positional insts', eqns)))) end | params_inst (loc, (prfx, (Named insts, eqns))) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " (map fst insts); val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps else error (quote p ^ " not a parameter of instantiated expression")); in (ps', (loc, (prfx, (Named insts, eqns)))) end; fun params_expr is = let val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; val fixed' = map (Variable.check_name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] else let val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed'); in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; in (expr', implicit'' @ fixed) end; (** Read instantiation **) (* Parse positional or named instantiation *) local fun prep_inst prep_term ctxt parms (Positional insts) = (insts ~~ parms) |> map (fn (NONE, p) => Free (p, dummyT) | (SOME t, _) => prep_term ctxt t) | prep_inst prep_term ctxt parms (Named insts) = parms |> map (fn p => (case AList.lookup (op =) insts p of SOME t => prep_term ctxt t | NONE => Free (p, dummyT))); in fun parse_inst x = prep_inst Syntax.parse_term x; fun make_inst x = prep_inst (K I) x; end; (* Instantiation morphism *) fun inst_morphism params ((prfx, mandatory), insts') ctxt = let (* parameters *) val parm_types = map #2 params; val type_parms = fold Term.add_tfreesT parm_types []; (* type inference *) val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; val type_parms' = fold Term.add_tvarsT parm_types' []; val checked = (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) val (type_parms'', insts'') = chop (length type_parms') checked; (* context *) val ctxt' = fold Proof_Context.augment checked ctxt; val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; (* instantiation *) val instT = TFrees.build (fold2 (fn v => fn T => not (TFree v = T) ? TFrees.add (v, T)) type_parms (map Logic.dest_type type_parms'')); val cert_inst = Frees.build (fold2 (fn v => fn t => not (Free v = t) ? Frees.add (v, cert t)) (map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) insts''); in (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; (*** Locale processing ***) (** Parsing **) fun parse_elem prep_typ prep_term ctxt = Element.map_ctxt {binding = I, typ = prep_typ ctxt, term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), fact = I, attrib = I}; fun prepare_stmt prep_prop prep_obtains ctxt stmt = (case stmt of Element.Shows raw_shows => raw_shows |> (map o apsnd o map) (fn (t, ps) => (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) | Element.Obtains raw_obtains => let val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; val obtains = prep_obtains thesis_ctxt thesis raw_obtains; in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); (** Simultaneous type inference: instantiations + elements + statement **) local fun mk_type T = (Logic.mk_type T, []); fun mk_term t = (t, []); fun mk_propp (p, pats) = (Type.constraint propT p, pats); fun dest_type (T, []) = Logic.dest_type T; fun dest_term (t, []) = t; fun dest_propp (p, pats) = (p, pats); fun extract_inst (_, (_, ts)) = map mk_term ts; fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)); fun extract_eqns es = map (mk_term o snd) es; fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs; fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs | extract_elem (Notes _) = [] | extract_elem (Lazy_Notes _) = []; fun restore_elem (Fixes fixes, css) = (fixes ~~ css) |> map (fn ((x, _, mx), cs) => (x, cs |> map dest_type |> try hd, mx)) |> Fixes | restore_elem (Constrains csts, css) = (csts ~~ css) |> map (fn ((x, _), cs) => (x, cs |> map dest_type |> hd)) |> Constrains | restore_elem (Assumes asms, css) = (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes | restore_elem (Defines defs, css) = (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines | restore_elem (elem as Notes _, _) = elem | restore_elem (elem as Lazy_Notes _, _) = elem; fun prep (_, pats) (ctxt, t :: ts) = let val ctxt' = Proof_Context.augment t ctxt in ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), (ctxt', ts)) end; fun check cs ctxt = let val (cs', (ctxt', _)) = fold_map prep cs (ctxt, Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)); in (cs', ctxt') end; in fun check_autofix insts eqnss elems concl ctxt = let val inst_cs = map extract_inst insts; val eqns_cs = map extract_eqns eqnss; val elem_css = map extract_elem elems; val concl_cs = (map o map) mk_propp (map snd concl); (* Type inference *) val (inst_cs' :: eqns_cs' :: css', ctxt') = (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in ((map restore_inst (insts ~~ inst_cs'), map restore_eqns (eqnss ~~ eqns_cs'), map restore_elem (elems ~~ elem_css'), map fst concl ~~ concl_cs'), ctxt') end; end; (** Prepare locale elements **) fun declare_elem prep_var (Fixes fixes) ctxt = let val (vars, _) = fold_map prep_var fixes ctxt in ctxt |> Proof_Context.add_fixes vars |> snd end | declare_elem prep_var (Constrains csts) ctxt = ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd | declare_elem _ (Assumes _) ctxt = ctxt | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt | declare_elem _ (Lazy_Notes _) ctxt = ctxt; (** Finish locale elements **) fun finish_inst ctxt (loc, (prfx, inst)) = let val thy = Proof_Context.theory_of ctxt; val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; in (loc, morph) end; fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => let val x = Binding.name_of binding in (binding, AList.lookup (op =) parms x, mx) end); local fun closeup _ _ false elem = elem | closeup (outer_ctxt, ctxt) parms true elem = let (* FIXME consider closing in syntactic phase -- before type checking *) fun close_frees t = let val rev_frees = Term.fold_aterms (fn Free (x, T) => if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t []; in fold (Logic.all o Free) rev_frees t end; fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in context element"; in (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) | e => e) end; in fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes) | finish_elem _ _ _ (Constrains _) = Constrains [] | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms) | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs) | finish_elem _ _ _ (elem as Notes _) = elem | finish_elem _ _ _ (elem as Lazy_Notes _) = elem; end; (** Process full context statement: instantiations + elements + statement **) (* Interleave incremental parsing and type inference over entire parsed stretch. *) local fun abs_def ctxt = Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; fun prep_full_context_statement parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 = let val thy = Proof_Context.theory_of ctxt1; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let val params = map #1 (Locale.params_of thy loc); val inst' = prep_inst ctxt (map #1 params) inst; val parm_types' = params |> map (#2 #> Logic.varifyT_global #> Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> Type_Infer.paramify_vars); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt; val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 handle ERROR msg => if null eqns then error msg else (Locale.tracing ctxt1 (msg ^ "\nFalling back to reading rewrites clause before activation."); ctxt2); val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns; val eqns' = (prep_eqns ctxt' o map snd) eqns; val eqnss' = [attrss ~~ eqns']; val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt'; val rewrite_morph = eqns' |> map (abs_def ctxt') |> Variable.export_terms ctxt' ctxt |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) |> Morphism.default; val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']; in (i + 1, insts', eqnss', ctxt'') end; fun prep_elem raw_elem ctxt = let val ctxt' = ctxt |> Context_Position.set_visible false |> declare_elem prep_var_elem raw_elem |> Context_Position.restore_visible ctxt; val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem; in (elems', ctxt') end; val fors = fold_map prep_var_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd; val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2); fun prep_stmt elems ctxt = check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; val _ = if fixed_frees then () else (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of [] => () | frees => error ("Illegal free variables in expression: " ^ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); val ((insts, _, elems', concl), ctxt4) = ctxt3 |> init_body |> fold_map prep_elem raw_elems |-> prep_stmt; (* parameters from expression and elements *) val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) (Fixes fors :: elems'); val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4; val fors' = finish_fixes parms fors; val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors'; val deps = map (finish_inst ctxt5) insts; val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'; in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end; in fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) Obtain.cert_obtains Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x; end; (* Context statement: elements + statement *) local fun prep_statement prep activate raw_elems raw_stmt ctxt = let val ((_, _, _, elems, concl), _) = prep {strict = true, do_close = false, fixed_frees = true} ([], []) I raw_elems raw_stmt ctxt; val ctxt' = ctxt |> Proof_Context.set_stmt true |> fold_map activate elems |> #2 |> Proof_Context.restore_stmt ctxt; in (concl, ctxt') end; in fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x; fun read_statement x = prep_statement read_full_context_statement Element.activate x; end; (* Locale declaration: import + elements *) fun fix_params params = Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; local fun prep_declaration prep activate raw_import init_body raw_elems ctxt = let val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) = prep {strict = false, do_close = true, fixed_frees = false} raw_import init_body raw_elems (Element.Shows []) ctxt; val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale"; (* Declare parameters and imported facts *) val ctxt' = ctxt |> fix_params fixed |> fold (Context.proof_map o Locale.activate_facts NONE) deps; val (elems', ctxt'') = ctxt' |> Proof_Context.set_stmt true |> fold_map activate elems ||> Proof_Context.restore_stmt ctxt'; in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end; in fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; fun read_declaration x = prep_declaration read_full_context_statement Element.activate x; end; (* Locale expression to set up a goal *) local fun props_of thy (name, morph) = let val (asm, defs) = Locale.specification_of thy name in map (Morphism.term morph) (the_list asm @ defs) end; fun prep_goal_expression prep expression ctxt = let val thy = Proof_Context.theory_of ctxt; val ((fixed, deps, eqnss, _, _), _) = prep {strict = true, do_close = true, fixed_frees = true} expression I [] (Element.Shows []) ctxt; (* proof obligations *) val propss = map (props_of thy) deps; val eq_propss = (map o map) snd eqnss; val goal_ctxt = ctxt |> fix_params fixed |> (fold o fold) Proof_Context.augment (propss @ eq_propss); val export = Proof_Context.export_morphism goal_ctxt ctxt; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism "Expression.prep_goal" {binding = [], typ = [K exp_typ], term = [K exp_term], fact = [K exp_fact]}; in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end; in fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; fun read_goal_expression x = prep_goal_expression read_full_context_statement x; end; (*** Locale declarations ***) (* extract specification text *) val norm_term = Envir.beta_norm oo Term.subst_atomic; fun bind_def ctxt eq (env, eqs) = let val _ = Local_Defs.cert_def ctxt (K []) eq; val ((y, T), b) = Local_Defs.abs_def eq; val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of [] => ((Free (y, T), b') :: env, eq :: eqs) | dups => if forall (fn (_, b'') => b' aconv b'') dups then (env, eqs) else err "Attempt to redefine variable") end; (* text has the following structure: (((exts, exts'), (ints, ints')), (xs, env, defs)) where exts: external assumptions (terms in assumes elements) exts': dito, normalised wrt. env ints: internal assumptions (terms in assumptions from insts) ints': dito, normalised wrt. env xs: the free variables in exts' and ints' and rhss of definitions, this includes parameters except defined parameters env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env defs: the equations from the defines elements *) fun eval_text _ _ (Fixes _) text = text | eval_text _ _ (Constrains _) text = text | eval_text _ is_ext (Assumes asms) (((exts, exts'), (ints, ints')), (env, defs)) = let val ts = maps (map #1 o #2) asms; val ts' = map (norm_term env) ts; val spec' = if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) else ((exts, exts'), (ints @ ts, ints' @ ts')); in (spec', (env, defs)) end | eval_text ctxt _ (Defines defs) (spec, binds) = (spec, fold (bind_def ctxt o #1 o #2) defs binds) | eval_text _ _ (Notes _) text = text | eval_text _ _ (Lazy_Notes _) text = text; fun eval_inst ctxt (loc, morph) text = let val thy = Proof_Context.theory_of ctxt; val (asm, defs) = Locale.specification_of thy loc; val asm' = Option.map (Morphism.term morph) asm; val defs' = map (Morphism.term morph) defs; val text' = text |> (if is_some asm then eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])]) else I) |> (if not (null defs) then eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs')) else I) (* FIXME clone from locale.ML *) in text' end; fun eval_elem ctxt elem text = eval_text ctxt true elem text; fun eval ctxt deps elems = let val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [])); val ((spec, (_, defs))) = fold (eval_elem ctxt) elems text'; in (spec, defs) end; (* axiomsN: name of theorem set with destruct rules for locale predicates, also name suffix of delta predicates and assumptions. *) val axiomsN = "axioms"; local (* introN: name of theorems for introduction rules of locale and delta predicates *) val introN = "intro"; fun atomize_spec ctxt ts = let val t = Logic.mk_conjunction_balanced ts; val body = Object_Logic.atomize_term ctxt t; val bodyT = Term.fastype_of body; in if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t)) else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t)) end; (* achieve plain syntax for locale predicates (without "PROP") *) fun aprop_tr' n c = let val c' = Lexicon.mark_const c; fun tr' (_: Proof.context) T args = if T <> dummyT andalso length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args) else raise Match; in (c', tr') end; (* define one predicate including its intro rule and axioms - binding: predicate name - parms: locale parameters - defs: thms representing substitutions from defines elements - ts: terms representing locale assumptions (not normalised wrt. defs) - norm_ts: terms representing locale assumptions (normalised wrt. defs) - thy: the theory *) fun def_pred binding parms defs ts norm_ts thy = let val name = Sign.full_name thy binding; val thy_ctxt = Proof_Context.init_global thy; val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts; val env = Names.build (Names.add_free_names body); val xs = filter (Names.defined env o #1) parms; val Ts = map #2 xs; val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts); val extra_tfrees = TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body) |> TFrees.keys |> map TFree; val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT; val args = map Logic.mk_type extra_tfrees @ map Free xs; val head = Term.list_comb (Const (name, predT), args); val statement = Object_Logic.ensure_propT thy_ctxt head; val ([pred_def], defs_thy) = thy |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name] |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])]; val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head; val intro = Goal.prove_global defs_thy [] norm_ts statement (fn {context = ctxt, ...} => rewrite_goals_tac ctxt [pred_def] THEN compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts)); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness axioms_ctxt t (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1)); in ((statement, intro, axioms), defs_thy) end; in (* main predicate definition function *) fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy = let val ctxt = Proof_Context.init_global thy; val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs; val (a_pred, a_intro, a_axioms, thy2) = if null exts then (NONE, NONE, [], thy) else let val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding; val ((statement, intro, axioms), thy1) = thy |> def_pred abinding parms defs' exts exts'; val ((_, [intro']), thy2) = thy1 |> Sign.qualified_path true abinding |> Global_Theory.note_thms "" ((Binding.name introN, []), [([intro], [Locale.unfold_add])]) ||> Sign.restore_naming thy1; in (SOME statement, SOME intro', axioms, thy2) end; val (b_pred, b_intro, b_axioms, thy4) = if null ints then (NONE, NONE, [], thy2) else let val ((statement, intro, axioms), thy3) = thy2 |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val conclude_witness = Drule.export_without_context o Element.conclude_witness (Proof_Context.init_global thy3); val ([(_, [intro']), _], thy4) = thy3 |> Sign.qualified_path true binding |> Global_Theory.note_thmss "" [((Binding.name introN, []), [([intro], [Locale.intro_add])]), ((Binding.name axiomsN, []), [(map conclude_witness axioms, [])])] ||> Sign.restore_naming thy3; in (SOME statement, SOME intro', axioms, thy4) end; in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy4) end; end; local fun assumes_to_notes (Assumes asms) axms = fold_map (fn (a, spec) => fn axs => let val (ps, qs) = chop (length spec) axs in ((a, [(ps, [])]), qs) end) asms axms |> apfst (curry Notes "") | assumes_to_notes e axms = (e, axms); fun defines_to_notes ctxt (Defines defs) = Notes ("", map (fn (a, (def, _)) => (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)], [(Attrib.internal o K) Locale.witness_add])])) defs) | defines_to_notes _ e = e; val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false; fun gen_add_locale prep_include prep_decl binding raw_predicate_binding raw_includes raw_import raw_body thy = let val name = Sign.full_name thy binding; val _ = Locale.defined thy name andalso error ("Duplicate definition of locale " ^ quote name); val ctxt = Proof_Context.init_global thy; val includes = map (prep_include ctxt) raw_includes; val ((fixed, deps, body_elems, _), (parms, ctxt')) = ctxt |> Bundle.includes includes |> prep_decl raw_import I raw_body; val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms); val extra_tfrees = TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts') |> TFrees.keys; val _ = if null extra_tfrees then () else warning ("Additional type variable(s) in locale specification " ^ Binding.print binding ^ ": " ^ commas (map (Syntax.string_of_typ ctxt' o TFree) extra_tfrees)); val predicate_binding = if Binding.is_empty raw_predicate_binding then binding else raw_predicate_binding; val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_binding parms text thy; val pred_ctxt = Proof_Context.init_global thy'; val a_satisfy = Element.satisfy_morphism a_axioms; val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ maps (fn Fixes fixes => map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems; val asm = if is_some b_statement then b_statement else a_statement; val hyp_spec = filter is_hyp body_elems; val notes = if is_some asm then [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []), [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))], [(Attrib.internal o K) Locale.witness_add])])])] else []; val notes' = body_elems - |> map (Element.transform_ctxt (Morphism.transfer_morphism thy')) + |> map (Element.transfer_ctxt thy') |> map (defines_to_notes pred_ctxt) |> map (Element.transform_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |> fst |> map (Element.transform_ctxt b_satisfy) |> map_filter (fn Notes notes => SOME notes | _ => NONE); val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val axioms = map (Element.conclude_witness pred_ctxt) b_axioms; val loc_ctxt = thy' |> Locale.register_locale binding (extra_tfrees, params) (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps') |> Named_Target.init includes name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; in val add_locale = gen_add_locale (K I) cert_declaration; val add_locale_cmd = gen_add_locale Bundle.check read_declaration; end; end; 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,249 +1,247 @@ (* 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 (Thm.transfer' ctxt 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 transform_witness = - Element.transform_witness - (Morphism.transfer_morphism' ctxt' $> export' $> Morphism.trim_context_morphism); + val transform_witness = Element.transform_witness (Morphism.set_trim_context' ctxt' export'); val deps' = (deps ~~ witss) |> map (fn ((dep, morph), wits) => (dep, morph $> Element.satisfy_morphism (map transform_witness 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 add_registration_proof registration ctxt = ctxt |> Proof_Context.set_stmt false |> Context.proof_map (Locale.add_registration registration) |> Proof_Context.restore_stmt ctxt; 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 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 Generic_Target.local_interpretation; fun interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs 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 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 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,436 +1,437 @@ (* 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 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 touch_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 syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> local_theory -> local_theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val notation_cmd: bool -> Syntax.mode -> (string * 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_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, target: Proof.context}; fun make_lthy (background_naming, operations, conclude, target) : lthy = {background_naming = background_naming, operations = operations, 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, 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, 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; (* 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, 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)); + Morphism.set_context' lthy + (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; fun touch_ml_env context = if Context.enabled_tracing () then (case context of Context.Theory _ => ML_Env.touch context | Context.Proof _ => context) else context; (** operations **) val operations_of = #operations o top_of; fun operation f lthy = f (operations_of lthy) lthy; fun operation1 f x = operation (fn ops => f ops x); 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; val theory_registration = operation1 #theory_registration; fun locale_dependency registration = assert_bottom #> operation1 #locale_dependency 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))); (* syntax *) fun gen_syntax prep_type add mode raw_args lthy = let val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args; val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args; val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args; in declaration {syntax = true, pervasive = false} (fn _ => Proof_Context.generic_syntax add mode args') lthy end; val syntax = gen_syntax (K I); val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax; (* notation *) local fun gen_type_notation prep_type add mode raw_args lthy = let val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy)); val args = map (apfst prepare) 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 gen_notation prep_const add mode raw_args lthy = let val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy); val args = map (apfst prepare) 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; in val type_notation = gen_type_notation (K I); val type_notation_cmd = gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false}); val notation = gen_notation (K I); val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false}); 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, 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; 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, 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,788 +1,789 @@ (* 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 registrations_of: Context.generic -> string -> (string * morphism) list val add_dependency: string -> registration -> theory -> theory (* Diagnostic *) val get_locales: theory -> string list val locale_notes: theory -> string -> (string * Attrib.fact list) 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 Markup.localeN; 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); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\locale\ (Args.theory -- Scan.lift Parse.embedded_position >> (ML_Syntax.print_string o uncurry check))); 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, - map (Element.transform_ctxt Morphism.trim_context_morphism) hyp_spec), + map Element.trim_context_ctxt hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes), - (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, + (map (fn (name, morph) => + make_dep (name, (Morphism.reset_context 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 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}; val eq_reg: reg * reg -> bool = op = o apply2 #serial; (* 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 = reg Idtab.table * mixins; val empty: T = (Idtab.empty, Inttab.empty); fun merge args = let val ctxt0 = Syntax.init_pretty_global (#1 (hd args)); fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T = (Idtab.merge eq_reg (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 ctxt0 [] id)); in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end; in Library.foldl1 recursive_merge (map #2 args) 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 locale_notes thy loc = fold (cons o #1) (#notes (the_locale thy loc)) []; fun lazy_notes thy loc = locale_notes 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) (Morphism.default 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; (*** 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 => Context.theory_map (add_registration {inst = inst, mixin = NONE, export = export})) regs thy' end; (*** 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 + let val elem' = Element.transform_ctxt (Morphism.set_context'' 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 Item_Net.T * thm Item_Net.T * thm Item_Net.T; val empty = (Thm.item_net, Thm.item_net, Thm.item_net); fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) = (Item_Net.merge (witnesses1, witnesses2), Item_Net.merge (intros1, intros2), Item_Net.merge (unfolds1, unfolds2)); ); fun get_thms which ctxt = map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt))); val get_witnesses = get_thms (Item_Net.content o #1); val get_intros = get_thms (Item_Net.content o #2); val get_unfolds = get_thms (Item_Net.content o #3); val witness_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Item_Net.update (Thm.trim_context th) x, y, z))); val intro_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Item_Net.update (Thm.trim_context th) y, z))); val unfold_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Item_Net.update (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/spec_rules.ML b/src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML +++ b/src/Pure/Isar/spec_rules.ML @@ -1,188 +1,187 @@ (* Title: Pure/Isar/spec_rules.ML Author: Makarius Rules that characterize specifications, with optional name and rough classification. NB: In the face of arbitrary morphisms, the original shape of specifications may get lost. *) signature SPEC_RULES = sig datatype recursion = Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion val recursion_ord: recursion ord val encode_recursion: recursion XML.Encode.T datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown val rough_classification_ord: rough_classification ord val equational_primrec: string list -> rough_classification val equational_recdef: rough_classification val equational_primcorec: string list -> rough_classification val equational_corec: rough_classification val equational: rough_classification val is_equational: rough_classification -> bool val is_inductive: rough_classification -> bool val is_co_inductive: rough_classification -> bool val is_relational: rough_classification -> bool val is_unknown: rough_classification -> bool val encode_rough_classification: rough_classification XML.Encode.T type spec_rule = {pos: Position.T, name: string, rough_classification: rough_classification, terms: term list, rules: thm list} val get: Proof.context -> spec_rule list val get_global: theory -> spec_rule list val dest_theory: theory -> spec_rule list val retrieve: Proof.context -> term -> spec_rule list val retrieve_global: theory -> term -> spec_rule list val add: binding -> rough_classification -> term list -> thm list -> local_theory -> local_theory val add_global: binding -> rough_classification -> term list -> thm list -> theory -> theory end; structure Spec_Rules: SPEC_RULES = struct (* recursion *) datatype recursion = Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion; val recursion_index = fn Primrec _ => 0 | Recdef => 1 | Primcorec _ => 2 | Corec => 3 | Unknown_Recursion => 4; fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2) | recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2) | recursion_ord rs = int_ord (apply2 recursion_index rs); val encode_recursion = let open XML.Encode in variant [fn Primrec a => ([], list string a), fn Recdef => ([], []), fn Primcorec a => ([], list string a), fn Corec => ([], []), fn Unknown_Recursion => ([], [])] end; (* rough classification *) datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown; fun rough_classification_ord (Equational r1, Equational r2) = recursion_ord (r1, r2) | rough_classification_ord cs = int_ord (apply2 (fn Equational _ => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3) cs); val equational_primrec = Equational o Primrec; val equational_recdef = Equational Recdef; val equational_primcorec = Equational o Primcorec; val equational_corec = Equational Corec; val equational = Equational Unknown_Recursion; val is_equational = fn Equational _ => true | _ => false; val is_inductive = fn Inductive => true | _ => false; val is_co_inductive = fn Co_Inductive => true | _ => false; val is_relational = is_inductive orf is_co_inductive; val is_unknown = fn Unknown => true | _ => false; val encode_rough_classification = let open XML.Encode in variant [fn Equational r => ([], encode_recursion r), fn Inductive => ([], []), fn Co_Inductive => ([], []), fn Unknown => ([], [])] end; (* rules *) type spec_rule = {pos: Position.T, name: string, rough_classification: rough_classification, terms: term list, rules: thm list}; fun eq_spec (specs: spec_rule * spec_rule) = (op =) (apply2 #name specs) andalso is_equal (rough_classification_ord (apply2 #rough_classification specs)) andalso eq_list (op aconv) (apply2 #terms specs) andalso eq_list Thm.eq_thm_prop (apply2 #rules specs); fun map_spec_rules f ({pos, name, rough_classification, terms, rules}: spec_rule) : spec_rule = {pos = pos, name = name, rough_classification = rough_classification, terms = terms, rules = map f rules}; structure Data = Generic_Data ( type T = spec_rule Item_Net.T; val empty : T = Item_Net.init eq_spec #terms; val merge = Item_Net.merge; ); (* get *) fun get_generic imports context = let val thy = Context.theory_of context; val transfer = Global_Theory.transfer_theories thy; fun imported spec = imports |> exists (fn thy => Item_Net.member (Data.get (Context.Theory thy)) spec); in Item_Net.content (Data.get context) |> filter_out imported |> (map o map_spec_rules) transfer end; val get = get_generic [] o Context.Proof; val get_global = get_generic [] o Context.Theory; fun dest_theory thy = rev (get_generic (Theory.parents_of thy) (Context.Theory thy)); (* retrieve *) fun retrieve_generic context = Item_Net.retrieve (Data.get context) #> (map o map_spec_rules) (Thm.transfer'' context); val retrieve = retrieve_generic o Context.Proof; val retrieve_global = retrieve_generic o Context.Theory; (* add *) fun add b rough_classification terms rules lthy = let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => let + val psi = Morphism.set_trim_context'' context phi; val pos = Position.thread_data (); - val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b); + val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding psi b); val (terms', rules') = - map (Thm.transfer (Context.theory_of context)) thms0 - |> Morphism.fact phi + Morphism.fact psi thms0 |> chop (length terms) - |>> map (Thm.term_of o Drule.dest_term) - ||> map Thm.trim_context; + |>> map (Thm.term_of o Drule.dest_term); in context |> (Data.map o Item_Net.update) {pos = pos, name = name, rough_classification = rough_classification, terms = terms', rules = rules'} end) end; fun add_global b rough_classification terms rules thy = thy |> (Context.theory_map o Data.map o Item_Net.update) {pos = Position.thread_data (), name = Sign.full_name thy b, rough_classification = rough_classification, terms = terms, rules = map Thm.trim_context rules}; end; diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,802 +1,822 @@ (* Title: Pure/Isar/token.ML Author: Markus Wenzel, TU Muenchen Outer token syntax for Isabelle/Isar. *) signature TOKEN = sig datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Cartouche | Control of Antiquote.control | Comment of Comment.kind option | (*special content*) Error of string | EOF val control_kind: kind val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T type src = T list type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} datatype value = Source of src | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list | Output of XML.body option val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T val is_eof: T -> bool val not_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool val get_control: T -> Antiquote.control option val is_command: T -> bool val keyword_with: (string -> bool) -> T -> bool val is_command_modifier: T -> bool val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_comment: T -> bool val is_informal_comment: T -> bool val is_formal_comment: T -> bool val is_document_marker: T -> bool val is_ignored: T -> bool val is_begin_ignore: T -> bool val is_end_ignore: T -> bool val is_error: T -> bool val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool val range_of: T list -> Position.range val core_range_of: T list -> Position.range val content_of: T -> string val source_of: T -> string val input_of: T -> Input.source val inner_syntax_of: T -> string val keyword_markup: bool * Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val reports: Keyword.keywords -> T -> Position.report_text list val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val print: T -> string val text_of: T -> string * string val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_output: T -> XML.body option val put_output: XML.body -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value val get_name: T -> name_value option val declare_maxidx: T -> Proof.context -> Proof.context val map_facts: (string option -> thm list -> thm list) -> T -> T - val trim_context_src: src -> src + val trim_context: T -> T + val transfer: theory -> T -> T val transform: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> T val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a val closure: T -> T val pretty_value: Proof.context -> T -> Pretty.T val name_of_src: src -> string * Position.T val args_of_src: src -> T list val checked_src: src -> bool val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a val pretty_src: Proof.context -> src -> Pretty.T val ident_or_symbolic: string -> bool val read_cartouche: Symbol_Pos.T list -> T val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Token: TOKEN = struct (** tokens **) (* token kind *) datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Cartouche | Control of Antiquote.control | Comment of Comment.kind option | (*special content*) Error of string | EOF; val control_kind = Control Antiquote.no_control; fun equiv_kind kind kind' = (case (kind, kind') of (Control _, Control _) => true | (Error _, Error _) => true | _ => kind = kind'); val str_of_kind = fn Command => "command" | Keyword => "keyword" | Ident => "identifier" | Long_Ident => "long identifier" | Sym_Ident => "symbolic identifier" | Var => "schematic variable" | Type_Ident => "type variable" | Type_Var => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" | Space => "white space" | String => "quoted string" | Alt_String => "back-quoted string" | Cartouche => "text cartouche" | Control _ => "control cartouche" | Comment NONE => "informal comment" | Comment (SOME _) => "formal comment" | Error _ => "bad input" | EOF => "end-of-input"; val immediate_kinds = Vector.fromList [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; val delimited_kind = (fn String => true | Alt_String => true | Cartouche => true | Control _ => true | Comment _ => true | _ => false); (* datatype token *) (*The value slot assigns an (optional) internal value to a token, usually as a side-effect of special scanner setup (see also args.ML). Note that an assignable ref designates an intermediate state of internalization -- it is NOT meant to persist.*) type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot and slot = Slot | Value of value option | Assignable of value option Unsynchronized.ref and value = Source of T list | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list | Output of XML.body option; type src = T list; (* position *) fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; fun adjust_offsets adjust (Token ((x, range), y, z)) = Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); (* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _), _)) = true | is_eof _ = false; val not_eof = not o is_eof; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* kind of token *) fun kind_of (Token (_, (k, _), _)) = k; fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k'; fun get_control tok = (case kind_of tok of Control control => SOME control | _ => NONE); val is_command = is_kind Command; fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; fun is_ignored (Token (_, (Space, _), _)) = true | is_ignored (Token (_, (Comment NONE, _), _)) = true | is_ignored _ = false; fun is_proper (Token (_, (Space, _), _)) = false | is_proper (Token (_, (Comment _, _), _)) = false | is_proper _ = true; fun is_comment (Token (_, (Comment _, _), _)) = true | is_comment _ = false; fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true | is_informal_comment _ = false; fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true | is_formal_comment _ = false; fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true | is_document_marker _ = false; fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true | is_begin_ignore _ = false; fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true | is_end_ignore _ = false; fun is_error (Token (_, (Error _, _), _)) = true | is_error _ = false; (* blanks and newlines -- space tokens obey lines *) fun is_space (Token (_, (Space, _), _)) = true | is_space _ = false; fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) | is_blank _ = false; fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x | is_newline _ = false; (* range of tokens *) fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; val core_range_of = drop_prefix is_ignored #> drop_suffix is_ignored #> range_of; (* token content *) fun content_of (Token (_, (_, x), _)) = x; fun source_of (Token ((source, _), _, _)) = source; fun input_of (Token ((source, range), (kind, _), _)) = Input.source (delimited_kind kind) source range; fun inner_syntax_of tok = let val x = content_of tok in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; (* markup reports *) local val token_kind_markup = fn Var => (Markup.var, "") | Type_Ident => (Markup.tfree, "") | Type_Var => (Markup.tvar, "") | String => (Markup.string, "") | Alt_String => (Markup.alt_string, "") | Cartouche => (Markup.cartouche, "") | Control _ => (Markup.cartouche, "") | Comment _ => (Markup.comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties] else (if Keyword.is_proof_asm keywords x then [Markup.keyword3] else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] else [Markup.keyword1]) |> map Markup.command_properties; in fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; fun reports keywords tok = if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then keyword_reports tok [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)] else let val pos = pos_of tok; val (m, text) = token_kind_markup (kind_of tok); val deleted = Symbol_Pos.explode_deleted (source_of tok, pos); in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end; fun markups keywords = map (#2 o #1) o reports keywords; end; (* unparse *) fun unparse (Token (_, (kind, x), _)) = (case kind of String => Symbol_Pos.quote_string_qq x | Alt_String => Symbol_Pos.quote_string_bq x | Cartouche => cartouche x | Control control => Symbol_Pos.content (Antiquote.control_symbols control) | Comment NONE => enclose "(*" "*)" x | EOF => "" | _ => x); fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ Markup.markups ms s, "") else (k, Markup.markups ms s) end; (** associated values **) (* inlined file content *) fun file_source (file: file) = let val text = cat_lines (#lines file); val end_pos = Position.symbol_explode text (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files | get_files _ = []; fun put_files [] tok = tok | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); (* document output *) fun get_output (Token (_, _, Value (SOME (Output output)))) = output | get_output _ = NONE; fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output)))) | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok)); (* access values *) fun get_value (Token (_, _, Value v)) = v | get_value _ = NONE; fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) | map_value _ tok = tok; (* reports of value *) fun get_assignable_value (Token (_, _, Assignable r)) = ! r | get_assignable_value (Token (_, _, Value v)) = v | get_assignable_value _ = NONE; fun reports_of_value tok = (case get_assignable_value tok of SOME (Literal markup) => let val pos = pos_of tok; val x = content_of tok; in if Position.is_reported pos then map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) else [] end | _ => []); (* name value *) fun name_value a = Name (a, Morphism.identity); fun get_name tok = (case get_assignable_value tok of SOME (Name (a, _)) => SOME a | _ => NONE); (* maxidx *) fun declare_maxidx tok = (case get_value tok of SOME (Source src) => fold declare_maxidx src | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths | SOME (Attribute _) => I (* FIXME !? *) | SOME (Declaration decl) => (fn ctxt => let val ctxt' = Context.proof_map (Morphism.form decl) ctxt in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) | _ => I); (* fact values *) fun map_facts f = map_value (fn v => (case v of Source src => Source (map (map_facts f) src) | Fact (a, ths) => Fact (a, f a ths) | _ => v)); -val trim_context_src = (map o map_facts) (K (map Thm.trim_context)); + +(* implicit context *) + +local + +fun context thm_context morphism_context = + let + fun token_context tok = map_value + (fn Source src => Source (map token_context src) + | Fact (a, ths) => Fact (a, map thm_context ths) + | Name (a, phi) => Name (a, morphism_context phi) + | v => v) tok; + in token_context end; + +in + +val trim_context = context Thm.trim_context Morphism.reset_context; +fun transfer thy = context (Thm.transfer thy) (Morphism.set_context thy); + +end; (* transform *) fun transform phi = map_value (fn v => (case v of Source src => Source (map (transform phi) src) | Literal _ => v | Name (a, psi) => Name (a, psi $> phi) | Typ T => Typ (Morphism.typ phi T) | Term t => Term (Morphism.term phi t) | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) | Files _ => v | Output _ => v)); (* static binding *) (*1st stage: initialize assignable slots*) fun init_assignable tok = (case tok of Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := NONE; tok)); (*2nd stage: assign values as side-effect of scanning*) fun assign v tok = (case tok of Token (x, y, Slot) => Token (x, y, Value v) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := v; tok)); fun evaluate mk eval arg = let val x = eval arg in (assign (SOME (mk x)) arg; x) end; (*3rd stage: static closure of final values*) fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) | closure tok = tok; (* pretty *) fun pretty_value ctxt tok = (case get_value tok of SOME (Literal markup) => let val x = content_of tok in Pretty.mark_str (keyword_markup markup x, x) end | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); (* src *) fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src = let val head = #1 (dest_src src); val name = (case get_name head of SOME {name, ...} => name | NONE => content_of head); in (name, pos_of head) end; val args_of_src = #2 o dest_src; fun pretty_src ctxt src = let val (head, args) = dest_src src; val prt_name = (case get_name head of SOME {print, ...} => Pretty.mark_str (print ctxt) | NONE => Pretty.str (content_of head)); in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; fun checked_src (head :: _) = is_some (get_name head) | checked_src [] = true; fun check_src ctxt get_table src = let val (head, args) = dest_src src; val table = get_table ctxt; in (case get_name head of SOME {name, ...} => (src, Name_Space.get table name) | NONE => let val pos = pos_of head; val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); val _ = Context_Position.report ctxt pos Markup.operator; val kind = Name_Space.kind_of (Name_Space.space_of_table table); fun print ctxt' = Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; val value = name_value {name = name, kind = kind, print = print}; val head' = closure (assign (SOME value) head); in (head' :: args, x) end) end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "Outer lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* scan symbolic idents *) val scan_symid = Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; fun is_symid str = (case try Symbol.explode str of SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan cartouche *) val scan_cartouche = Symbol_Pos.scan_pos -- ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; val scan_space = Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || Scan.many space_symbol @@@ $$$ "\n"; (* scan comment *) val scan_comment = Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); (** token sources **) local fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; fun token k ss = Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || scan_comment >> token_range (Comment NONE) || Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_cartouche >> token_range Cartouche || Antiquote.scan_control err_prefix >> (fn control => token (Control control) (Antiquote.control_symbols control)) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq (Scan.literal (Keyword.major_keywords keywords) >> pair Command) (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) (Lexicon.scan_longid >> pair Long_Ident || Lexicon.scan_id >> pair Ident || Lexicon.scan_var >> pair Var || Lexicon.scan_tid >> pair Type_Ident || Lexicon.scan_tvar >> pair Type_Var || Symbol_Pos.scan_float >> pair Float || Symbol_Pos.scan_nat >> pair Nat || scan_symid >> pair Sym_Ident) >> uncurry token)); fun recover msg = (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in fun make_source keywords {strict} = let val scan_strict = Scan.bulk (scan_token keywords); val scan = if strict then scan_strict else Scan.recover scan_strict recover; in Source.source Symbol_Pos.stopper scan end; fun read_cartouche syms = (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of SOME tok => tok | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); end; (* explode *) fun tokenize keywords strict syms = Source.of_list syms |> make_source keywords strict |> Source.exhaust; fun explode keywords pos text = Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false}; fun explode0 keywords = explode keywords Position.none; (* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; fun print_properties keywords = map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; (* make *) fun make ((k, n), s) pos = let val pos' = Position.shift_offsets {remove_id = false} n pos; val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.nth immediate_kinds k, s), Slot) else (case explode Keyword.empty_keywords pos s of [tok] => tok | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) in (tok, pos') end; fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; fun make_src a args = make_string a :: args; (** parsers **) type 'a parser = T list -> 'a * T list; type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); (* wrapped syntax *) fun syntax_generic scan src context = let val (name, pos) = name_of_src src; val old_reports = maps reports_of_value src; val args1 = map init_assignable (args_of_src src); fun reported_text () = if Context_Position.reports_enabled_generic context then let val new_reports = maps (reports_of_value o closure) args1 in if old_reports <> new_reports then map (fn (p, m) => Position.reported_text p m "") new_reports else [] end else []; in (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => let val _ = Output.report (reported_text ()) in (x, context') end | (_, (context', args2)) => let val print_name = (case get_name (hd src) of NONE => quote name | SOME {kind, print, ...} => let val ctxt' = Context.proof_of context'; val (markup, xname) = print ctxt'; in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); val print_args = if null args2 then "" else ":\n " ^ space_implode " " (map print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ Markup.markup_report (implode (reported_text ()))) end) end; fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; end; type 'a parser = 'a Token.parser; type 'a context_parser = 'a Token.context_parser; diff --git a/src/Pure/ex/Def.thy b/src/Pure/ex/Def.thy --- a/src/Pure/ex/Def.thy +++ b/src/Pure/ex/Def.thy @@ -1,114 +1,114 @@ (* Title: Pure/ex/Def.thy Author: Makarius Primitive constant definition, without fact definition; automatic expansion via Simplifier (simproc). *) theory Def imports Pure keywords "def" :: thy_defn begin ML \ signature DEF = sig val get_def: Proof.context -> cterm -> thm option val def: (binding * typ option * mixfix) option -> (binding * typ option * mixfix) list -> term -> local_theory -> term * local_theory val def_cmd: (binding * string option * mixfix) option -> (binding * string option * mixfix) list -> string -> local_theory -> term * local_theory end; structure Def: DEF = struct (* context data *) type def = {lhs: term, mk_eq: morphism -> thm}; val eq_def : def * def -> bool = op aconv o apply2 #lhs; fun transform_def phi ({lhs, mk_eq}: def) = {lhs = Morphism.term phi lhs, mk_eq = Morphism.transform phi mk_eq}; structure Data = Generic_Data ( type T = def Item_Net.T; val empty : T = Item_Net.init eq_def (single o #lhs); val merge = Item_Net.merge; ); fun declare_def lhs eq lthy = let val eq0 = Thm.trim_context eq; val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0}; in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => - let val psi = Morphism.transfer_morphism'' context $> phi $> Morphism.trim_context_morphism + let val psi = Morphism.set_trim_context'' context phi in (Data.map o Item_Net.update) (transform_def psi def) context end) end; fun get_def ctxt ct = let val thy = Proof_Context.theory_of ctxt; val data = Data.get (Context.Proof ctxt); val t = Thm.term_of ct; fun match_def {lhs, mk_eq} = if Pattern.matches thy (lhs, t) then let val inst = Thm.match (Thm.cterm_of ctxt lhs, ct); val eq = Morphism.form mk_eq |> Thm.transfer thy |> Thm.instantiate inst; in SOME eq end else NONE; in Item_Net.retrieve_matching data t |> get_first match_def end; (* simproc setup *) val _ = (Theory.setup o Named_Target.theory_map) (Simplifier.define_simproc \<^binding>\expand_def\ {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def}); (* Isar command *) fun gen_def prep_spec raw_var raw_params raw_spec lthy = let val ((vars, xs, get_pos, spec), _) = lthy |> prep_spec (the_list raw_var) raw_params [] raw_spec; val (((x, _), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = false} spec; val _ = Name.reject_internal (x, []); val (b, mx) = (case (vars, xs) of ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn) | ([(b, _, mx)], [y]) => if x = y then (b, mx) else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.here (Binding.pos_of b))); val ((lhs, (_, eq)), lthy') = lthy |> Local_Theory.define_internal ((b, mx), (Binding.empty_atts, rhs)); (*sanity check for original specification*) val _: thm = prove lthy' eq; in (lhs, declare_def lhs eq lthy') end; val def = gen_def Specification.check_spec_open; val def_cmd = gen_def Specification.read_spec_open; val _ = Outer_Syntax.local_theory \<^command_keyword>\def\ "primitive constant definition, without fact definition" (Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn ((decl, spec), params) => #2 o def_cmd decl params spec)); end; \ end diff --git a/src/Pure/morphism.ML b/src/Pure/morphism.ML --- a/src/Pure/morphism.ML +++ b/src/Pure/morphism.ML @@ -1,224 +1,231 @@ (* Title: Pure/morphism.ML Author: Makarius Abstract morphisms on formal entities. *) infix 1 $> signature BASIC_MORPHISM = sig type morphism type declaration = morphism -> Context.generic -> Context.generic val $> : morphism * morphism -> morphism end signature MORPHISM = sig include BASIC_MORPHISM exception MORPHISM of string * exn val the_theory: theory option -> theory val set_context: theory -> morphism -> morphism val set_context': Proof.context -> morphism -> morphism val set_context'': Context.generic -> morphism -> morphism val reset_context: morphism -> morphism val morphism: string -> {binding: (theory option -> binding -> binding) list, typ: (theory option -> typ -> typ) list, term: (theory option -> term -> term) list, fact: (theory option -> thm list -> thm list) list} -> morphism val is_identity: morphism -> bool val is_empty: morphism -> bool val pretty: morphism -> Pretty.T val binding: morphism -> binding -> binding val binding_prefix: morphism -> (string * bool) list val typ: morphism -> typ -> typ val term: morphism -> term -> term val fact: morphism -> thm list -> thm list val thm: morphism -> thm -> thm val cterm: morphism -> cterm -> cterm val identity: morphism val default: morphism option -> morphism val compose: morphism -> morphism -> morphism val transform: morphism -> (morphism -> 'a) -> morphism -> 'a val form: (morphism -> 'a) -> 'a val binding_morphism: string -> (binding -> binding) -> morphism val typ_morphism': string -> (theory -> typ -> typ) -> morphism val typ_morphism: string -> (typ -> typ) -> morphism val term_morphism': string -> (theory -> term -> term) -> morphism val term_morphism: string -> (term -> term) -> morphism val fact_morphism: string -> (thm list -> thm list) -> morphism val thm_morphism: string -> (thm -> thm) -> morphism val transfer_morphism: theory -> morphism val transfer_morphism': Proof.context -> morphism val transfer_morphism'': Context.generic -> morphism val trim_context_morphism: morphism + val set_trim_context: theory -> morphism -> morphism + val set_trim_context': Proof.context -> morphism -> morphism + val set_trim_context'': Context.generic -> morphism -> morphism val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism end; structure Morphism: MORPHISM = struct (* named functions *) type 'a funs = (string * (theory option -> 'a -> 'a)) list; exception MORPHISM of string * exn; fun app context (name, f) x = f context x handle exn => if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn); (* optional context *) fun the_theory (SOME thy) = thy | the_theory NONE = raise Fail "Morphism lacks theory context"; fun join_transfer (SOME thy) = Thm.join_transfer thy | join_transfer NONE = I; val join_context = join_options Context.join_certificate_theory; (* type morphism *) datatype morphism = Morphism of {context: theory option, names: string list, binding: binding funs, typ: typ funs, term: term funs, fact: thm list funs}; type declaration = morphism -> Context.generic -> Context.generic; fun rep (Morphism args) = args; fun apply which phi = let val args = rep phi in fold_rev (app (#context args)) (which args) end; fun put_context context (Morphism {context = _, names, binding, typ, term, fact}) = Morphism {context = context, names = names, binding = binding, typ = typ, term = term, fact = fact}; val set_context = put_context o SOME; val set_context' = set_context o Proof_Context.theory_of; val set_context'' = set_context o Context.theory_of; val reset_context = put_context NONE; fun morphism a {binding, typ, term, fact} = Morphism { context = NONE, names = if a = "" then [] else [a], binding = map (pair a) binding, typ = map (pair a) typ, term = map (pair a) term, fact = map (pair a) fact}; (*syntactic test only!*) fun is_identity (Morphism {context = _, names, binding, typ, term, fact}) = null names andalso null binding andalso null typ andalso null term andalso null fact; fun is_empty phi = is_none (#context (rep phi)) andalso is_identity phi; fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi)))); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); val binding = apply #binding; fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of; val typ = apply #typ; val term = apply #term; fun fact phi = map (join_transfer (#context (rep phi))) #> apply #fact phi; val thm = singleton o fact; val cterm = Drule.cterm_rule o thm; (* morphism combinators *) val identity = morphism "" {binding = [], typ = [], term = [], fact = []}; val default = the_default identity; fun compose phi1 phi2 = if is_empty phi1 then phi2 else if is_empty phi2 then phi1 else let val {context = context1, names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1} = rep phi1; val {context = context2, names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2} = rep phi2; in Morphism { context = join_context (context1, context2), names = names1 @ names2, binding = binding1 @ binding2, typ = typ1 @ typ2, term = term1 @ term2, fact = fact1 @ fact2} end; fun phi1 $> phi2 = compose phi2 phi1; fun transform phi f = fn psi => f (phi $> psi); fun form f = f identity; (* concrete morphisms *) fun binding_morphism a binding = morphism a {binding = [K binding], typ = [], term = [], fact = []}; fun typ_morphism' a typ = morphism a {binding = [], typ = [typ o the_theory], term = [], fact = []}; fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []}; fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []}; fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []}; fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]}; fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]}; fun transfer_morphism thy = fact_morphism "transfer" I |> set_context thy; val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; val transfer_morphism'' = transfer_morphism o Context.theory_of; val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; +fun set_trim_context thy phi = set_context thy phi $> trim_context_morphism; +val set_trim_context' = set_trim_context o Proof_Context.theory_of; +val set_trim_context'' = set_trim_context o Context.theory_of; + (* instantiate *) fun instantiate_frees_morphism (cinstT, cinst) = if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity else let val instT = TFrees.map (K Thm.typ_of) cinstT; val inst = Frees.map (K Thm.term_of) cinst; in morphism "instantiate_frees" {binding = [], typ = if TFrees.is_empty instT then [] else [K (Term_Subst.instantiateT_frees instT)], term = [K (Term_Subst.instantiate_frees (instT, inst))], fact = [K (map (Thm.instantiate_frees (cinstT, cinst)))]} end; fun instantiate_morphism (cinstT, cinst) = if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity else let val instT = TVars.map (K Thm.typ_of) cinstT; val inst = Vars.map (K Thm.term_of) cinst; in morphism "instantiate" {binding = [], typ = if TVars.is_empty instT then [] else [K (Term_Subst.instantiateT instT)], term = [K (Term_Subst.instantiate (instT, inst))], fact = [K (map (Thm.instantiate (cinstT, cinst)))]} end; end; structure Basic_Morphism: BASIC_MORPHISM = Morphism; open Basic_Morphism;