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,800 +1,803 @@ (* 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 -> Morphism.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 -> Morphism.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 transfer_dep thy ({name, morphisms, pos, serial}: dep) : dep = {name = name, morphisms = apply2 (Morphism.set_context thy) morphisms, pos = pos, serial = serial}; fun make_dep (name, morphisms) : dep = {name = name, morphisms = apply2 Morphism.reset_context 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' (morph, b) : mixins -> mixins = Inttab.cons_list (serial', ((Morphism.reset_context morph, b), 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: (Morphism.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.trim_context_ctxt hyp_spec), - ((map (fn decl => (decl, serial ())) syntax_decls, + ((map (fn decl => (Morphism.entity_reset_context 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, 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 (Morphism.set_context thy morph) o Free o #1); fun specification_of thy = #spec o the_locale thy; fun hyp_spec_of thy = map (Element.transfer_ctxt thy) o #hyp_spec o the_locale thy; fun dependencies_of thy = map (transfer_dep thy) o #dependencies o the_locale thy; fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial |> (map o apfst o apfst) (Morphism.set_context thy); (* 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 = (Morphism.reset_context morph, Morphism.reset_context 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; + val form_syntax_decl = + Morphism.form o Morphism.transform morph o Morphism.entity_set_context thy; in - context - |> fold_rev (Morphism.form o Morphism.transform morph o #1) syntax_decls + fold_rev (form_syntax_decl o #1) syntax_decls context handle ERROR msg => activate_err msg "syntax" (name, morph) context end; fun activate_notes activ_elem 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' = Morphism.set_context thy (morph $> mixin); val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name); in (notes', input) |-> fold (fn elem => fn res => activ_elem (Element.transfer_ctxt thy elem) res) end handle ERROR msg => activate_err msg "facts" (name, morph) context; fun activate_notes_trace activ_elem context export' (name, morph) context' = let val _ = trace "facts" (name, morph) context'; in activate_notes activ_elem context export' (name, morph) context' end; fun activate_all name thy activ_elem (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 (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 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 |-> (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.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)]; + let val decl0 = Morphism.entity_reset_context decl in + syntax ? + Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl0, serial ()))) + #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl0)] + end; (*** 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 (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/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,822 +1,829 @@ (* 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 attribute Morphism.entity | Declaration of Morphism.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: 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 attribute Morphism.entity | Declaration of Morphism.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)); (* implicit context *) local -fun context thm_context morphism_context = +fun context thm_context morphism_context attribute_context declaration_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) + | Attribute a => Attribute (attribute_context a) + | Declaration a => Declaration (declaration_context a) | 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); +val trim_context = + context Thm.trim_context Morphism.reset_context + Morphism.entity_reset_context Morphism.entity_reset_context; + +fun transfer thy = + context (Thm.transfer thy) (Morphism.set_context thy) + (Morphism.entity_set_context thy) (Morphism.entity_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/morphism.ML b/src/Pure/morphism.ML --- a/src/Pure/morphism.ML +++ b/src/Pure/morphism.ML @@ -1,243 +1,254 @@ (* Title: Pure/morphism.ML Author: Makarius Abstract morphisms on formal entities. *) infix 1 $> signature BASIC_MORPHISM = sig type morphism 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 type 'a entity val entity: (morphism -> 'a) -> 'a entity + val entity_reset_context: 'a entity -> 'a entity + val entity_set_context: theory -> 'a entity -> 'a entity + val entity_set_context': Proof.context -> 'a entity -> 'a entity + val entity_set_context'': Context.generic -> 'a entity -> 'a entity val transform: morphism -> 'a entity -> 'a entity val form: 'a entity -> 'a val form_entity: (morphism -> 'a) -> 'a type declaration = (Context.generic -> Context.generic) entity type declaration_fn = morphism -> Context.generic -> Context.generic 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}; 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; (* abstract entities *) -datatype 'a entity = Entity of morphism -> 'a -fun entity f = Entity f; +datatype 'a entity = Entity of (morphism -> 'a) * morphism; +fun entity f = Entity (f, identity); -fun transform phi (Entity f) = Entity (fn psi => f (phi $> psi)); -fun form (Entity f) = f identity; +fun entity_morphism g (Entity (f, phi)) = Entity (f, g phi); +fun entity_reset_context a = entity_morphism reset_context a; +fun entity_set_context thy a = entity_morphism (set_context thy) a; +fun entity_set_context' ctxt a = entity_morphism (set_context' ctxt) a; +fun entity_set_context'' context a = entity_morphism (set_context'' context) a; + +fun transform phi2 (Entity (f, phi1)) = Entity (f, phi1 $> phi2); +fun form (Entity (f, phi)) = f phi; + fun form_entity f = f identity; type declaration = (Context.generic -> Context.generic) entity; type declaration_fn = morphism -> Context.generic -> Context.generic; (* 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;