diff --git a/src/HOL/ex/Join_Theory.thy b/src/HOL/ex/Join_Theory.thy --- a/src/HOL/ex/Join_Theory.thy +++ b/src/HOL/ex/Join_Theory.thy @@ -1,47 +1,47 @@ (* Title: HOL/ex/Join_Theory.thy Author: Makarius *) section \Join theory content from independent (parallel) specifications\ theory Join_Theory imports Main begin subsection \Example template\ definition "test = True" lemma test: "test" by (simp add: test_def) subsection \Specification as Isabelle/ML function\ ML \ fun spec i lthy = let val b = Binding.name ("test" ^ string_of_int i) val ((t, (_, def)), lthy') = lthy |> Local_Theory.define ((b, NoSyn), ((Binding.empty, []), \<^term>\True\)); val th = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop t) (fn {context = goal_ctxt, ...} => asm_full_simp_tac (goal_ctxt addsimps [def]) 1); val (_, lthy'') = lthy' |> Local_Theory.note ((b, []), [th]); in lthy'' end; \ subsection \Example application\ setup \ fn thy => let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10) - in Theory.join_theory forked_thys end + in Context.join_thys forked_thys end \ term test1 thm test1 term test10 thm test10 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,785 +1,786 @@ (* 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, hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes), (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) fun change_locale name = Locales.map o Name_Space.map_table_entry name o map_locale o apsnd; (** Primitive operations **) fun parameters_of thy = #parameters o the_locale thy; val params_of = #2 oo parameters_of; fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> map (Morphism.term morph o Free o #1); fun specification_of thy = #spec o the_locale thy; fun hyp_spec_of thy = #hyp_spec o the_locale thy; fun dependencies_of thy = #dependencies o the_locale thy; fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; (* Print instance and qualifiers *) fun pretty_reg_inst ctxt qs (name, ts) = let fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?"); fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs)); val prt_term = Pretty.quote o Syntax.pretty_term ctxt; fun prt_term' t = if Config.get ctxt show_types then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] else prt_term t; fun prt_inst ts = Pretty.block (Pretty.breaks (pretty_name ctxt name :: map prt_term' ts)); in (case qs of [] => prt_inst ts | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts]) end; fun pretty_reg ctxt export (name, morph) = let val thy = Proof_Context.theory_of ctxt; val morph' = morph $> export; val qs = Morphism.binding_prefix morph'; val ts = instance_of thy name morph'; in pretty_reg_inst ctxt qs (name, ts) end; (*** Identifiers: activated locales in theory or proof context ***) type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *) val empty_idents : idents = Symtab.empty; val insert_idents = Symtab.insert_list (eq_list (op aconv)); val merge_idents = Symtab.merge_list (eq_list (op aconv)); fun redundant_ident thy idents (name, instance) = exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name); structure Idents = Generic_Data ( type T = idents; val empty = empty_idents; val 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 old_thys = + 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 (Syntax.init_pretty_global (#1 old_thys)) [] id)); + Pretty.string_of (pretty_reg_inst ctxt0 [] id)); in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end; - in recursive_merge 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) (the_default Morphism.identity export) dep |-> Idents.put |> Context_Position.restore_visible_generic context; fun activate_declarations dep = Context.proof_map (fn context => context |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep |-> Idents.put |> Context_Position.restore_visible_generic context); fun init name thy = let val context = Context.Proof (Proof_Context.init_global thy); val marked = Idents.get context; in context |> Context_Position.set_visible_generic false |> pair empty_idents |> activate_all name thy init_element Morphism.transfer_morphism'' |-> (fn marked' => Idents.put (merge_idents (marked, marked'))) |> Context_Position.restore_visible_generic context |> Context.proof_of end; (*** Add and extend registrations ***) type registration = Locale.registration; fun amend_registration {mixin = NONE, ...} context = context | amend_registration {inst = (name, morph), mixin = SOME mixin, export} context = let val thy = Context.theory_of context; val ctxt = Context.proof_of context; val regs = get_regs context; val base = instance_of thy name (morph $> export); val serial' = (case Idtab.lookup regs (name, base) of NONE => error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^ " with\nparameter instantiation " ^ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available") | SOME {serial = serial', ...} => serial'); in add_mixin serial' mixin context end; (* Note that a registration that would be subsumed by an existing one will not be generated, and it will not be possible to amend it. *) fun add_registration {inst = (name, base_morph), mixin, export} context = let val thy = Context.theory_of context; val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix); val inst = instance_of thy name mix_morph; val idents = Idents.get context; in if redundant_ident thy idents (name, inst) then context (* FIXME amend mixins? *) else (idents, context) (* add new registrations with inherited mixins *) |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2 (* add mixin *) |> amend_registration {inst = (name, mix_morph), mixin = mixin, export = export} (* activate import hierarchy as far as not already active *) |> activate_facts (SOME export) (name, mix_morph $> pos_morph) end; (*** 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 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/axclass.ML b/src/Pure/axclass.ML --- a/src/Pure/axclass.ML +++ b/src/Pure/axclass.ML @@ -1,480 +1,483 @@ (* Title: Pure/axclass.ML Author: Markus Wenzel, TU Muenchen Type classes defined as predicates, associated with a record of parameters. Proven class relations and type arities. *) signature AXCLASS = sig type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} val get_info: theory -> class -> info val class_of_param: theory -> string -> class option val instance_name: string * class -> string val param_of_inst: theory -> string * string -> string val inst_of_param: theory -> string -> (string * string) option val unoverload: Proof.context -> thm -> thm val overload: Proof.context -> thm -> thm val unoverload_conv: Proof.context -> conv val overload_conv: Proof.context -> conv val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option val unoverload_const: theory -> string * typ -> string val cert_classrel: theory -> class * class -> class * class val read_classrel: theory -> xstring * xstring -> class * class val declare_overloaded: string * typ -> theory -> term * theory val define_overloaded: binding -> string * term -> theory -> thm * theory val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory val prove_classrel: class * class -> (Proof.context -> tactic) -> theory -> theory val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory val define_class: binding * class list -> string list -> (Thm.binding * term list) list -> theory -> class * theory val classrel_axiomatization: (class * class) list -> theory -> theory val arity_axiomatization: arity -> theory -> theory val class_axiomatization: binding * class list -> theory -> theory end; structure Axclass: AXCLASS = struct (** theory data **) (* axclass info *) type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}; fun make_axclass (def, intro, axioms, params): info = {def = def, intro = intro, axioms = axioms, params = params}; (* class parameters (canonical order) *) type param = string * class; fun add_param ctxt ((x, c): param) params = (case AList.lookup (op =) params x of NONE => (x, c) :: params | SOME c' => error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^ (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))); (* setup data *) datatype data = Data of {axclasses: info Symtab.table, params: param list, (*arity theorems with theory name*) inst_params: (string * thm) Symtab.table Symtab.table * (*constant name ~> type constructor ~> (constant name, equation)*) (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)}; +fun rep_data (Data args) = args; + fun make_data (axclasses, params, inst_params) = Data {axclasses = axclasses, params = params, inst_params = inst_params}; structure Data = Theory_Data' ( type T = data; val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty)); - fun merge old_thys - (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1}, - Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) = + fun merge args = let - val old_ctxt = Syntax.init_pretty_global (fst old_thys); + val ctxt0 = Syntax.init_pretty_global (#1 (hd args)); - val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); - val params' = + fun merge_params (params1, params2) = if null params1 then params2 else - fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p) + fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt0 p) params2 params1; - val inst_params' = + fun merge_inst_params (inst_params1, inst_params2) = (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); + + val axclasses' = Library.foldl1 (Symtab.merge (K true)) (map (#axclasses o rep_data o #2) args); + val params' = Library.foldl1 merge_params (map (#params o rep_data o #2) args); + val inst_params' = Library.foldl1 merge_inst_params (map (#inst_params o rep_data o #2) args); in make_data (axclasses', params', inst_params') end; ); fun map_data f = Data.map (fn Data {axclasses, params, inst_params} => make_data (f (axclasses, params, inst_params))); fun map_axclasses f = map_data (fn (axclasses, params, inst_params) => (f axclasses, params, inst_params)); fun map_params f = map_data (fn (axclasses, params, inst_params) => (axclasses, f params, inst_params)); fun map_inst_params f = map_data (fn (axclasses, params, inst_params) => (axclasses, params, f inst_params)); -val rep_data = Data.get #> (fn Data args => args); +val rep_theory_data = Data.get #> rep_data; -val axclasses_of = #axclasses o rep_data; -val params_of = #params o rep_data; -val inst_params_of = #inst_params o rep_data; +val axclasses_of = #axclasses o rep_theory_data; +val params_of = #params o rep_theory_data; +val inst_params_of = #inst_params o rep_theory_data; (* axclasses with parameters *) fun get_info thy c = (case Symtab.lookup (axclasses_of thy) c of SOME {def, intro, axioms, params} => {def = Thm.transfer thy def, intro = Thm.transfer thy intro, axioms = map (Thm.transfer thy) axioms, params = params} | NONE => error ("No such axclass: " ^ quote c)); fun all_params_of thy S = let val params = params_of thy; in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end; fun class_of_param thy = AList.lookup (op =) (params_of thy); (* maintain instance parameters *) fun get_inst_param thy (c, tyco) = (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of SOME (a, th) => (a, Thm.transfer thy th) | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco)); fun add_inst_param (c, tyco) (a, th) = (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, (a, Thm.trim_context th))) #> (map_inst_params o apsnd) (Symtab.update_new (a, (c, tyco))); val inst_of_param = Symtab.lookup o #2 o inst_params_of; val param_of_inst = #1 oo get_inst_param; fun inst_thms ctxt = Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) []; fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt); fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt)); fun unoverload_conv ctxt = Raw_Simplifier.rewrite ctxt true (inst_thms ctxt); fun overload_conv ctxt = Raw_Simplifier.rewrite ctxt true (map Thm.symmetric (inst_thms ctxt)); fun lookup_inst_param consts params (c, T) = (case get_inst_tyco consts (c, T) of SOME tyco => AList.lookup (op =) params (c, tyco) | NONE => NONE); fun unoverload_const thy (c_ty as (c, _)) = if is_some (class_of_param thy c) then (case get_inst_tyco (Sign.consts_of thy) c_ty of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c | NONE => c) else c; (** instances **) val classrel_prefix = "classrel_"; val arity_prefix = "arity_"; fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a; (* class relations *) fun cert_classrel thy raw_rel = let val string_of_sort = Syntax.string_of_sort_global thy; val (c1, c2) = apply2 (Sign.certify_class thy) raw_rel; val _ = Sign.primitive_classrel (c1, c2) thy; val _ = (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of [] => () | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); in (c1, c2) end; fun read_classrel thy raw_rel = cert_classrel thy (apply2 (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) handle TYPE (msg, _, _) => error msg; (* declaration and definition of instances of overloaded constants *) fun inst_tyco_of thy (c, T) = (case get_inst_tyco (Sign.consts_of thy) (c, T) of SOME tyco => tyco | NONE => error ("Illegal type for instantiation of class parameter: " ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); fun declare_overloaded (c, T) thy = let val class = (case class_of_param thy c of SOME class => class | NONE => error ("Not a class parameter: " ^ quote c)); val tyco = inst_tyco_of thy (c, T); val name_inst = instance_name (tyco, class) ^ "_inst"; val c' = instance_name (tyco, c); val T' = Type.strip_sorts T; in thy |> Sign.qualified_path true (Binding.name name_inst) |> Sign.declare_const_global ((Binding.name c', T'), NoSyn) |-> (fn const' as Const (c'', _) => Thm.add_def_global false true (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) #>> apsnd Thm.varifyT_global #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm) #> Global_Theory.add_thm ((Binding.concealed (Binding.name c'), thm), []) #> #2 #> pair (Const (c, T)))) ||> Sign.restore_naming thy end; fun define_overloaded b (c, t) thy = let val T = Term.fastype_of t; val tyco = inst_tyco_of thy (c, T); val (c', eq) = get_inst_param thy (c, tyco); val prop = Logic.mk_equals (Const (c', T), t); val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b; in thy |> Thm.add_def_global false false (b', prop) |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm]) end; (* primitive rules *) fun add_classrel raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); val binding = Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2)))); in thy |> Global_Theory.store_thm (binding, th) |-> Thm.add_classrel end; fun add_arity raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); val binding = Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity))); val args = Name.invent_names Name.context Name.aT Ss; val missing_params = Sign.complete_sort thy [c] |> maps (these o Option.map #params o try (get_info thy)) |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) |> (map o apsnd o map_atyps) (K (Type (t, map TFree args))); in thy |> Global_Theory.store_thm (binding, th) |-> Thm.add_arity |> fold (#2 oo declare_overloaded) missing_params end; (* tactical proofs *) fun prove_classrel raw_rel tac thy = let val ctxt = Proof_Context.init_global thy; val (c1, c2) = cert_classrel thy raw_rel; val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (fn {context, ...} => tac context) handle ERROR msg => cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ quote (Syntax.string_of_classrel ctxt [c1, c2])); in thy |> add_classrel th end; fun prove_arity raw_arity tac thy = let val ctxt = Proof_Context.init_global thy; val arity = Proof_Context.cert_arity ctxt raw_arity; val props = Logic.mk_arities arity; val ths = Goal.prove_common ctxt NONE [] [] props (fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context) handle ERROR msg => cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ quote (Syntax.string_of_arity ctxt arity)); in thy |> fold add_arity ths end; (** class definitions **) fun split_defined n eq = let val intro = (eq RS Drule.equal_elim_rule2) |> Conjunction.curry_balanced n |> n = 0 ? Thm.eq_assumption 1; val dests = if n = 0 then [] else (eq RS Drule.equal_elim_rule1) |> Balanced_Tree.dest (fn th => (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; in (intro, dests) end; fun define_class (bclass, raw_super) raw_params raw_specs thy = let val ctxt = Syntax.init_pretty_global thy; (* class *) val bconst = Binding.map_name Logic.const_of_class bclass; val class = Sign.full_name thy bclass; val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); fun check_constraint (a, S) = if Sign.subsort thy (super, S) then () else error ("Sort constraint of type variable " ^ Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^ " needs to be weaker than " ^ Syntax.string_of_sort ctxt super); (* params *) val params = raw_params |> map (fn p => let val T = Sign.the_const_type thy p; val _ = (case Term.add_tvarsT T [] of [((a, _), S)] => check_constraint (a, S) | _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); val T' = Term.map_type_tvar (K (Term.aT [class])) T; in (p, T') end); (* axioms *) fun prep_axiom t = (case Term.add_tfrees t [] of [(a, S)] => check_constraint (a, S) | [] => () | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t); t |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) |> Logic.close_form); val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; val name_atts = map fst raw_specs; (* definition *) val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss; val class_eq = Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs); val ([def], def_thy) = thy |> Sign.primitive_class (bclass, super) |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])]; val (raw_intro, (raw_classrel, raw_axioms)) = split_defined (length conjs) def ||> chop (length super); (* facts *) val class_triv = Thm.class_triv def_thy class; val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = def_thy |> Sign.qualified_path true bconst |> Global_Theory.note_thmss "" [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]), ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]), ((Binding.name "axioms", []), [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])] ||> Sign.restore_naming def_thy; (* result *) val axclass = make_axclass (Thm.trim_context def, Thm.trim_context intro, map Thm.trim_context axioms, params); val result_thy = facts_thy |> fold (fn th => Thm.add_classrel (class_triv RS th)) classrel |> Sign.qualified_path false bconst |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2 |> Sign.restore_naming facts_thy |> map_axclasses (Symtab.update (class, axclass)) |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params); in (class, result_thy) end; (** axiomatizations **) local (*old-style axioms*) fun add_axioms prep mk name add raw_args thy = let val args = prep thy raw_args; val specs = mk args; val names = name args; in thy |> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs) |-> fold (add o Drule.export_without_context o snd) end; fun class_const_dep c = ((Defs.Const, Logic.const_of_class c), [Term.aT []]); in val classrel_axiomatization = add_axioms (map o cert_classrel) (map Logic.mk_classrel) (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; val arity_axiomatization = add_axioms (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities (map (prefix arity_prefix) o Logic.name_arities) add_arity; fun class_axiomatization (bclass, raw_super) thy = let val class = Sign.full_name thy bclass; val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy; in thy |> Sign.primitive_class (bclass, super) |> classrel_axiomatization (map (fn c => (class, c)) super) |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super) end; end; end; diff --git a/src/Pure/context.ML b/src/Pure/context.ML --- a/src/Pure/context.ML +++ b/src/Pure/context.ML @@ -1,760 +1,756 @@ (* Title: Pure/context.ML Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, monotonic development graph and history support. Generic proof contexts with arbitrarily typed data. Firm naming conventions: thy, thy', thy1, thy2: theory ctxt, ctxt', ctxt1, ctxt2: Proof.context context: Context.generic *) signature BASIC_CONTEXT = sig type theory exception THEORY of string * theory list structure Proof: sig type context end structure Proof_Context: sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: {long: bool} -> theory -> string -> Proof.context end end; signature CONTEXT = sig include BASIC_CONTEXT (*theory context*) type theory_id val theory_id: theory -> theory_id val timing: bool Unsynchronized.ref val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_id_ord: theory_id ord val theory_id_name: {long: bool} -> theory_id -> string val theory_long_name: theory -> string val theory_base_name: theory -> string val theory_name: {long: bool} -> theory -> string val theory_identifier: theory -> serial val PureN: string val pretty_thy: theory -> Pretty.T val pretty_abbrev_thy: theory -> Pretty.T val get_theory: {long: bool} -> theory -> string -> theory val eq_thy_id: theory_id * theory_id -> bool val eq_thy: theory * theory -> bool val proper_subthy_id: theory_id * theory_id -> bool val proper_subthy: theory * theory -> bool val subthy_id: theory_id * theory_id -> bool val subthy: theory * theory -> bool val trace_theories: bool Unsynchronized.ref val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int} - val join_thys: theory * theory -> theory + val join_thys: theory list -> theory val begin_thy: string -> theory list -> theory val finish_thy: theory -> theory val theory_data_sizeof1: theory -> (Position.T * int) list (*proof context*) val raw_transfer: theory -> Proof.context -> Proof.context (*certificate*) datatype certificate = Certificate of theory | Certificate_Id of theory_id val certificate_theory: certificate -> theory val certificate_theory_id: certificate -> theory_id val eq_certificate: certificate * certificate -> bool val join_certificate: certificate * certificate -> certificate (*generic context*) datatype generic = Theory of theory | Proof of Proof.context val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val the_theory: generic -> theory val the_proof: generic -> Proof.context val map_theory: (theory -> theory) -> generic -> generic val map_proof: (Proof.context -> Proof.context) -> generic -> generic val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val theory_map: (generic -> generic) -> theory -> theory val proof_map: (generic -> generic) -> Proof.context -> Proof.context val theory_of: generic -> theory (*total*) val proof_of: generic -> Proof.context (*total*) (*thread data*) val get_generic_context: unit -> generic option val put_generic_context: generic option -> unit val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b val the_generic_context: unit -> generic val the_global_context: unit -> theory val the_local_context: unit -> Proof.context val >> : (generic -> generic) -> unit val >>> : (generic -> 'a * generic) -> 'a end; signature PRIVATE_CONTEXT = sig include CONTEXT structure Theory_Data: sig - val declare: Position.T -> Any.T -> (theory * theory -> Any.T * Any.T -> Any.T) -> serial + val declare: Position.T -> Any.T -> ((theory * Any.T) list -> Any.T) -> serial val get: serial -> (Any.T -> 'a) -> theory -> 'a val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory end structure Proof_Data: sig val declare: (theory -> Any.T) -> serial val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context end end; structure Context: PRIVATE_CONTEXT = struct (*** theory context ***) (*private copy avoids potential conflict of table exceptions*) structure Datatab = Table(type key = int val ord = int_ord); (** datatype theory **) +(* implicit state *) + +type state = {stage: int} Synchronized.var; + +fun make_state () : state = + Synchronized.var "Context.state" {stage = 0}; + +fun next_stage (state: state) = + Synchronized.change_result state (fn {stage} => (stage + 1, {stage = stage + 1})); + + +(* theory_id *) + abstype theory_id = Theory_Id of {id: serial, (*identifier*) ids: Intset.T, (*cumulative identifiers -- symbolic body content*) name: string, (*official theory name*) stage: int} (*index for anonymous updates*) with fun rep_theory_id (Theory_Id args) = args; val make_theory_id = Theory_Id; end; + +(* theory *) + datatype theory = Theory of + (*allocation state*) + state * (*identity*) {theory_id: theory_id, token: Position.T Unsynchronized.ref} * - (*allocation state*) - {next_stage: unit -> int} * (*ancestry*) {parents: theory list, (*immediate predecessors*) ancestors: theory list} * (*all predecessors -- canonical reverse order*) (*data*) Any.T Datatab.table; (*body content*) exception THEORY of string * theory list; fun rep_theory (Theory args) = args; -val theory_identity = #1 o rep_theory; +val state_of = #1 o rep_theory; +val theory_identity = #2 o rep_theory; val theory_id = #theory_id o theory_identity; val identity_of = rep_theory_id o theory_id; -val state_of = #2 o rep_theory; val ancestry_of = #3 o rep_theory; val data_of = #4 o rep_theory; -fun make_state () = {next_stage = Counter.make ()}; -fun next_stage {next_stage: unit -> int} = next_stage (); - fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; fun stage_final stage = stage = 0; val theory_id_stage = #stage o rep_theory_id; val theory_id_final = stage_final o theory_id_stage; val theory_id_ord = int_ord o apply2 (#id o rep_theory_id); fun theory_id_name {long} thy_id = let val name = #name (rep_theory_id thy_id) in if long then name else Long_Name.base_name name end; val theory_long_name = #name o identity_of; val theory_base_name = Long_Name.base_name o theory_long_name; fun theory_name {long} = if long then theory_long_name else theory_base_name; val theory_identifier = #id o identity_of; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; (* names *) val PureN = "Pure"; fun display_name thy_id = let val name = theory_id_name {long = false} thy_id; val final = theory_id_final thy_id; in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end; fun display_names thy = let val name = display_name (theory_id thy); val ancestor_names = map theory_long_name (ancestors_of thy); in rev (name :: ancestor_names) end; val pretty_thy = Pretty.str_list "{" "}" o display_names; val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); fun pretty_abbrev_thy thy = let val names = display_names thy; val n = length names; val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; fun get_theory long thy name = if theory_name long thy <> name then (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) else if theory_id_final (theory_id thy) then thy else error ("Unfinished theory " ^ quote name); -(* build ids *) +(* identity *) -val merge_ids = - apply2 identity_of #> - (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) => - Intset.merge (ids1, ids2) - |> Intset.insert id1 - |> Intset.insert id2); - - -(* equality and inclusion *) +fun merge_ids thys = + fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id)) + thys Intset.empty; val eq_thy_id = op = o apply2 (#id o rep_theory_id); val eq_thy = op = o apply2 (#id o identity_of); val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id); val proper_subthy = proper_subthy_id o apply2 theory_id; fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; val subthy = subthy_id o apply2 theory_id; (* consistent ancestors *) fun eq_thy_consistent (thy1, thy2) = eq_thy (thy1, thy2) orelse (theory_base_name thy1 = theory_base_name thy2 andalso raise THEORY ("Duplicate theory name", [thy1, thy2])); fun extend_ancestors thy thys = if member eq_thy_consistent thys thy then raise THEORY ("Duplicate theory node", thy :: thys) else thy :: thys; val merge_ancestors = merge eq_thy_consistent; +val eq_ancestry = + apply2 ancestry_of #> + (fn ({parents, ancestors}, {parents = parents', ancestors = ancestors'}) => + eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')); + (** theory data **) (* data kinds and access methods *) val timing = Unsynchronized.ref false; local type kind = {pos: Position.T, empty: Any.T, - merge: theory * theory -> Any.T * Any.T -> Any.T}; + merge: (theory * Any.T) list -> Any.T}; val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); -fun invoke name f k x = +fun the_kind k = (case Datatab.lookup (Synchronized.value kinds) k of - SOME kind => - if ! timing andalso name <> "" then - Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) - (fn () => f kind x) - else f kind x + SOME kind => kind | NONE => raise Fail "Invalid theory data identifier"); in -fun invoke_pos k = invoke "" (K o #pos) k (); -fun invoke_empty k = invoke "" (K o #empty) k (); -fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys); +val invoke_pos = #pos o the_kind; +val invoke_empty = #empty o the_kind; + +fun invoke_merge kind args = + if ! timing then + Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind)) + (fn () => #merge kind args) + else #merge kind args; fun declare_data pos empty merge = let val k = serial (); val kind = {pos = pos, empty = empty, merge = merge}; val _ = Synchronized.change kinds (Datatab.update (k, kind)); in k end; +fun lookup_data k thy = Datatab.lookup (data_of thy) k; + fun get_data k thy = - (case Datatab.lookup (data_of thy) k of + (case lookup_data k thy of SOME x => x | NONE => invoke_empty k); -fun merge_data thys = Datatab.join (invoke_merge thys); +fun merge_data [] = Datatab.empty + | merge_data [thy] = data_of thy + | merge_data thys = + let + fun merge (k, kind) data = + (case map_filter (fn thy => lookup_data k thy |> Option.map (pair thy)) thys of + [] => data + | [(_, x)] => Datatab.default (k, x) data + | args => Datatab.update (k, invoke_merge kind args) data); + in Datatab.fold merge (Synchronized.value kinds) (data_of (hd thys)) end; end; (** build theories **) (* create theory *) val trace_theories = Unsynchronized.ref false; local val theories = Synchronized.var "theory_tokens" ([]: Position.T Unsynchronized.ref option Unsynchronized.ref list); val dummy_token = Unsynchronized.ref Position.none; fun make_token () = if ! trace_theories then let val token = Unsynchronized.ref (Position.thread_data ()); val _ = Synchronized.change theories (cons (Weak.weak (SOME token))); in token end else dummy_token; in fun theories_trace () = let val trace = Synchronized.value theories; val _ = ML_Heap.full_gc (); val active_positions = fold (fn Unsynchronized.ref (SOME pos) => cons (! pos) | _ => I) trace []; in {active_positions = active_positions, active = length active_positions, total = length trace} end; -fun create_thy ids name stage state ancestry data = +fun create_thy state ids name stage ancestry data = let val theory_id = make_theory_id {id = serial (), ids = ids, name = name, stage = stage}; - val token = make_token (); - in Theory ({theory_id = theory_id, token = token}, state, ancestry, data) end; + val identity = {theory_id = theory_id, token = make_token ()}; + in Theory (state, identity, ancestry, data) end; end; (* primitives *) val pre_pure_thy = let val state = make_state (); val stage = next_stage state; - in create_thy Intset.empty PureN stage state (make_ancestry [] []) Datatab.empty end; + in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end; local fun change_thy finish f thy = let - val {id, ids, name, stage} = identity_of thy; - val Theory (_, state, ancestry, data) = thy; + val {name, stage, ...} = identity_of thy; + val Theory (state, _, ancestry, data) = thy; val ancestry' = if stage_final stage then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)) else ancestry; - val ids' = Intset.insert id ids; + val ids' = merge_ids [thy]; val stage' = if finish then 0 else next_stage state; val data' = f data; - in create_thy ids' name stage' state ancestry' data' end; + in create_thy state ids' name stage' ancestry' data' end; in val update_thy = change_thy false; -val extend_thy = change_thy false I; val finish_thy = change_thy true I; end; -(* join: anonymous theory nodes *) - -local - -fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]); - -fun join_stage (thy1, thy2) = - apply2 identity_of (thy1, thy2) |> - (fn ({name, stage, ...}, {name = name', stage = stage', ...}) => - if name <> name' orelse stage_final stage orelse stage_final stage' - then bad_join (thy1, thy2) - else - let val state = state_of thy1 - in {name = name, stage = next_stage state, state = state} end) +(* join: unfinished theory nodes *) -fun join_ancestry thys = - apply2 ancestry_of thys |> - (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) => - if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors') - then ancestry else bad_join thys); - -in +fun join_thys [] = raise List.Empty + | join_thys thys = + let + val thy0 = hd thys; + val name0 = theory_long_name thy0; + val state0 = state_of thy0; -fun join_thys thys = - let - val ids = merge_ids thys; - val {name, stage, state} = join_stage thys; - val ancestry = join_ancestry thys; - val data = merge_data thys (apply2 data_of thys); - in create_thy ids name stage state ancestry data end; + fun ok thy = + not (theory_id_final (theory_id thy)) andalso + theory_long_name thy = name0 andalso + eq_ancestry (thy0, thy); + val _ = + (case filter_out ok thys of + [] => () + | bad => raise THEORY ("Cannot join theories", bad)); -end; + val stage = next_stage state0; + val ids = merge_ids thys; + val data = merge_data thys; + in create_thy state0 ids name0 stage (ancestry_of thy0) data end; -(* merge: named theory nodes *) - -local +(* merge: finished theory nodes *) -fun merge_thys thys = - let - val ids = merge_ids thys; - val state = state_of (#1 thys); - val ancestry = make_ancestry [] []; - val data = merge_data thys (apply2 data_of thys); - in create_thy ids "" 0 state ancestry data end; - -fun maximal_thys thys = - thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); - -in +fun make_parents thys = + let val thys' = distinct eq_thy thys + in thys' |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys') end; fun begin_thy name imports = if name = "" then error ("Bad theory name: " ^ quote name) + else if null imports then error "Missing theory imports" else let - val parents = maximal_thys (distinct eq_thy imports); + val parents = make_parents imports; val ancestors = - Library.foldl merge_ancestors ([], map ancestors_of parents) + Library.foldl1 merge_ancestors (map ancestors_of parents) |> fold extend_ancestors parents; - - val thy0 = - (case parents of - [] => error "Missing theory imports" - | [thy] => extend_thy thy - | thy :: thys => Library.foldl merge_thys (thy, thys)); - val ids = #ids (identity_of thy0); + val ancestry = make_ancestry parents ancestors; val state = make_state (); val stage = next_stage state; - val ancestry = make_ancestry parents ancestors; - in create_thy ids name stage state ancestry (data_of thy0) |> tap finish_thy end; - -end; + val ids = merge_ids parents; + val data = merge_data parents; + in create_thy state ids name stage ancestry data |> tap finish_thy end; (* theory data *) structure Theory_Data = struct val declare = declare_data; fun get k dest thy = dest (get_data k thy); fun put k make x = update_thy (Datatab.update (k, make x)); fun sizeof1 k thy = Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1; end; fun theory_data_sizeof1 thy = build (data_of thy |> Datatab.fold_rev (fn (k, _) => (case Theory_Data.sizeof1 k thy of NONE => I | SOME n => (cons (invoke_pos k, n))))); (*** proof context ***) (* datatype Proof.context *) structure Proof = struct datatype context = Context of Any.T Datatab.table * theory; end; (* proof data kinds *) local val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table); fun init_data thy = Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy); fun init_new_data thy = Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data => if Datatab.defined data k then data else Datatab.update (k, init thy) data); fun init_fallback k thy = (case Datatab.lookup (Synchronized.value kinds) k of SOME init => init thy | NONE => raise Fail "Invalid proof data identifier"); in fun raw_transfer thy' (Proof.Context (data, thy)) = let val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; val data' = init_new_data thy' data; in Proof.Context (data', thy') end; structure Proof_Context = struct fun theory_of (Proof.Context (_, thy)) = thy; fun init_global thy = Proof.Context (init_data thy, thy); fun get_global long thy name = init_global (get_theory long thy name); end; structure Proof_Data = struct fun declare init = let val k = serial (); val _ = Synchronized.change kinds (Datatab.update (k, init)); in k end; fun get k dest (Proof.Context (data, thy)) = (case Datatab.lookup data k of SOME x => x | NONE => init_fallback k thy) |> dest; fun put k make x (Proof.Context (data, thy)) = Proof.Context (Datatab.update (k, make x) data, thy); end; end; (*** theory certificate ***) datatype certificate = Certificate of theory | Certificate_Id of theory_id; fun certificate_theory (Certificate thy) = thy | certificate_theory (Certificate_Id thy_id) = error ("No content for theory certificate " ^ display_name thy_id); fun certificate_theory_id (Certificate thy) = theory_id thy | certificate_theory_id (Certificate_Id thy_id) = thy_id; fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2) | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2) | eq_certificate _ = false; fun join_certificate (cert1, cert2) = let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2) else if proper_subthy_id (thy_id2, thy_id1) then cert1 else if proper_subthy_id (thy_id1, thy_id2) then cert2 else error ("Cannot join unrelated theory certificates " ^ display_name thy_id1 ^ " and " ^ display_name thy_id2) end; (*** generic context ***) datatype generic = Theory of theory | Proof of Proof.context; fun cases f _ (Theory thy) = f thy | cases _ g (Proof prf) = g prf; fun mapping f g = cases (Theory o f) (Proof o g); fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); val the_theory = cases I (fn _ => error "Ill-typed context: theory expected"); val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I; fun map_theory f = Theory o f o the_theory; fun map_proof f = Proof o f o the_proof; fun map_theory_result f = apsnd Theory o f o the_theory; fun map_proof_result f = apsnd Proof o f o the_proof; fun theory_map f = the_theory o f o Theory; fun proof_map f = the_proof o f o Proof; val theory_of = cases I Proof_Context.theory_of; val proof_of = cases Proof_Context.init_global I; (** thread data **) local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in fun get_generic_context () = Thread_Data.get generic_context_var; val put_generic_context = Thread_Data.put generic_context_var; fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context; fun the_generic_context () = (case get_generic_context () of SOME context => context | _ => error "Unknown context"); val the_global_context = theory_of o the_generic_context; val the_local_context = proof_of o the_generic_context; end; fun >>> f = let val (res, context') = f (the_generic_context ()); val _ = put_generic_context (SOME context'); in res end; nonfix >>; fun >> f = >>> (fn context => ((), f context)); val _ = put_generic_context (SOME (Theory pre_pure_thy)); end; structure Basic_Context: BASIC_CONTEXT = Context; open Basic_Context; (*** type-safe interfaces for data declarations ***) (** theory data **) signature THEORY_DATA'_ARGS = sig type T val empty: T - val merge: theory * theory -> T * T -> T + val merge: (theory * T) list -> T end; signature THEORY_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature THEORY_DATA = sig type T val get: theory -> T val put: T -> theory -> theory val map: (T -> T) -> theory -> theory end; functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA = struct type T = Data.T; exception Data of T; val kind = let val pos = Position.thread_data () in Context.Theory_Data.declare pos (Data Data.empty) - (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2))) + (Data o Data.merge o map (fn (thy, Data x) => (thy, x))) end; val get = Context.Theory_Data.get kind (fn Data x => x); val put = Context.Theory_Data.put kind Data; fun map f thy = put (f (get thy)) thy; end; functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = Theory_Data' ( type T = Data.T; val empty = Data.empty; - fun merge _ = Data.merge; + fun merge args = Library.foldl (fn (a, (_, b)) => Data.merge (a, b)) (#2 (hd args), tl args) ); (** proof data **) signature PROOF_DATA_ARGS = sig type T val init: theory -> T end; signature PROOF_DATA = sig type T val get: Proof.context -> T val put: T -> Proof.context -> Proof.context val map: (T -> T) -> Proof.context -> Proof.context end; functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = struct type T = Data.T; exception Data of T; val kind = Context.Proof_Data.declare (Data o Data.init); val get = Context.Proof_Data.get kind (fn Data x => x); val put = Context.Proof_Data.put kind Data; fun map f prf = put (f (get prf)) prf; end; (** generic data **) signature GENERIC_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature GENERIC_DATA = sig type T val get: Context.generic -> T val put: T -> Context.generic -> Context.generic val map: (T -> T) -> Context.generic -> Context.generic end; functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = struct structure Thy_Data = Theory_Data(Data); structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get); type T = Data.T; fun get (Context.Theory thy) = Thy_Data.get thy | get (Context.Proof prf) = Prf_Data.get prf; fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy) | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf); fun map f ctxt = put (f (get ctxt)) ctxt; end; (*hide private interface*) structure Context: CONTEXT = Context; diff --git a/src/Pure/sign.ML b/src/Pure/sign.ML --- a/src/Pure/sign.ML +++ b/src/Pure/sign.ML @@ -1,538 +1,537 @@ (* Title: Pure/sign.ML Author: Lawrence C Paulson and Markus Wenzel Logical signature content: naming conventions, concrete syntax, type signature, polymorphic constants. *) signature SIGN = sig val change_begin: theory -> theory val change_end: theory -> theory val change_end_local: Proof.context -> Proof.context val change_check: theory -> theory val syn_of: theory -> Syntax.syntax val tsig_of: theory -> Type.tsig val classes_of: theory -> Sorts.algebra val all_classes: theory -> class list val super_classes: theory -> class -> class list val minimize_sort: theory -> sort -> sort val complete_sort: theory -> sort -> sort val set_defsort: sort -> theory -> theory val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool val inter_sort: theory -> sort * sort -> sort val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list val logical_types: theory -> string list val typ_instance: theory -> typ * typ -> bool val typ_equiv: theory -> typ * typ -> bool val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int val consts_of: theory -> Consts.T val the_const_constraint: theory -> string -> typ val const_type: theory -> string -> typ option val the_const_type: theory -> string -> typ val declared_tyname: theory -> string -> bool val declared_const: theory -> string -> bool val naming_of: theory -> Name_Space.naming val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory val restore_naming: theory -> theory -> theory val inherit_naming: theory -> Proof.context -> Context.generic val full_name: theory -> binding -> string val full_name_path: theory -> string -> binding -> string val full_bname: theory -> bstring -> string val full_bname_path: theory -> string -> bstring -> string val const_monomorphic: theory -> string -> bool val const_typargs: theory -> string * typ -> typ list val const_instance: theory -> string * typ list -> typ val mk_const: theory -> string * typ list -> term val class_space: theory -> Name_Space.T val type_space: theory -> Name_Space.T val const_space: theory -> Name_Space.T val intern_class: theory -> xstring -> string val intern_type: theory -> xstring -> string val intern_const: theory -> xstring -> string val type_alias: binding -> string -> theory -> theory val const_alias: binding -> string -> theory -> theory val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class val certify_sort: theory -> sort -> sort val certify_typ: theory -> typ -> typ val certify_typ_mode: Type.mode -> theory -> typ -> typ val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int val certify_term: theory -> term -> term * typ * int val cert_term: theory -> term -> term val cert_prop: theory -> term -> term val no_frees: Proof.context -> term -> term val no_vars: Proof.context -> term -> term val add_type: Proof.context -> binding * int * mixfix -> theory -> theory val add_types_global: (binding * int * mixfix) list -> theory -> theory val add_nonterminals: Proof.context -> binding list -> theory -> theory val add_nonterminals_global: binding list -> theory -> theory val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory val add_abbrev: string -> binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory val primitive_class: binding * class list -> theory -> theory val primitive_classrel: class * class -> theory -> theory val primitive_arity: arity -> theory -> theory val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val parse_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val print_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory val get_scope: theory -> Binding.scope option val new_scope: theory -> Binding.scope * theory val new_group: theory -> theory val reset_group: theory -> theory val add_path: string -> theory -> theory val root_path: theory -> theory val parent_path: theory -> theory val mandatory_path: string -> theory -> theory val qualified_path: bool -> binding -> theory -> theory val local_path: theory -> theory val init_naming: theory -> theory val private_scope: Binding.scope -> theory -> theory val private: Position.T -> theory -> theory val qualified_scope: Binding.scope -> theory -> theory val qualified: Position.T -> theory -> theory val concealed: theory -> theory val hide_class: bool -> string -> theory -> theory val hide_type: bool -> string -> theory -> theory val hide_const: bool -> string -> theory -> theory end structure Sign: SIGN = struct (** datatype sign **) datatype sign = Sign of {syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*) tsig: Type.tsig, (*order-sorted signature of types*) consts: Consts.T}; (*polymorphic constants*) +fun rep_sign (Sign args) = args; fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts}; structure Data = Theory_Data' ( type T = sign; val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty); - fun merge old_thys (sign1, sign2) = + fun merge args = let - val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1; - val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2; - - val syn = Syntax.merge_syntax (syn1, syn2); - val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2); - val consts = Consts.merge (consts1, consts2); - in make_sign (syn, tsig, consts) end; + val context0 = Context.Theory (#1 (hd args)); + val syn' = Library.foldl1 Syntax.merge_syntax (map (#syn o rep_sign o #2) args); + val tsig' = Library.foldl1 (Type.merge_tsig context0) (map (#tsig o rep_sign o #2) args); + val consts' = Library.foldl1 Consts.merge (map (#consts o rep_sign o #2) args); + in make_sign (syn', tsig', consts') end; ); -fun rep_sg thy = Data.get thy |> (fn Sign args => args); +val rep_sg = rep_sign o Data.get; fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts))); fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts)); fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts)); fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts)); (* linear change discipline *) fun change_base begin = map_sign (fn (syn, tsig, consts) => (syn, Type.change_base begin tsig, Consts.change_base begin consts)); val change_begin = change_base true; val change_end = change_base false; fun change_end_local ctxt = Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt; fun change_check thy = if can change_end thy then raise Fail "Unfinished linear change of theory content" else thy; (* syntax *) val syn_of = #syn o rep_sg; (* type signature *) val tsig_of = #tsig o rep_sg; val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; val all_classes = Sorts.all_classes o classes_of; val super_classes = Sorts.super_classes o classes_of; val minimize_sort = Sorts.minimize_sort o classes_of; val complete_sort = Sorts.complete_sort o classes_of; val set_defsort = map_tsig o Type.set_defsort; val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; val of_sort = Type.of_sort o tsig_of; val inter_sort = Type.inter_sort o tsig_of; val witness_sorts = Type.witness_sorts o tsig_of; val logical_types = Type.logical_types o tsig_of; val typ_instance = Type.typ_instance o tsig_of; fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); val typ_match = Type.typ_match o tsig_of; val typ_unify = Type.unify o tsig_of; (* polymorphic constants *) val consts_of = #consts o rep_sg; val the_const_constraint = Consts.the_constraint o consts_of; val the_const_type = #2 oo (Consts.the_const o consts_of); val const_type = try o the_const_type; val const_monomorphic = Consts.is_monomorphic o consts_of; val const_typargs = Consts.typargs o consts_of; val const_instance = Consts.instance o consts_of; fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts)); fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none); val declared_const = can o the_const_constraint; (* naming *) val naming_of = Name_Space.naming_of o Context.Theory; val map_naming = Context.theory_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; fun inherit_naming thy = Name_Space.map_naming (K (naming_of thy)) o Context.Proof; val full_name = Name_Space.full_name o naming_of; fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy)); fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name; fun full_bname_path thy path = full_name_path thy path o Binding.name; (** name spaces **) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; (** certify entities **) (*exception TYPE*) (* certify wrt. type signature *) val arity_number = Type.arity_number o tsig_of; fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy); val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; val certify_typ = Type.cert_typ o tsig_of; fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of; (* certify term/prop *) local fun type_check context tm = let fun err_appl bs t T u U = let val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U; in raise TYPE (msg, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T | typ_of (_, Free (_, T)) = T | typ_of (_, Var (_, T)) = T | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript => raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i])) | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body) | typ_of (bs, t $ u) = let val T = typ_of (bs, t) and U = typ_of (bs, u) in (case T of Type ("fun", [T1, T2]) => if T1 = U then T2 else err_appl bs t T u U | _ => err_appl bs t T u U) end; in typ_of ([], tm) end; fun err msg = raise TYPE (msg, [], []); fun check_vars (t $ u) = (check_vars t; check_vars u) | check_vars (Abs (_, _, t)) = check_vars t | check_vars (Free (x, _)) = if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else () | check_vars (Var (xi as (_, i), _)) = if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else () | check_vars _ = (); in fun certify' prop context do_expand consts thy tm = let val _ = check_vars tm; val tm' = Term.map_types (certify_typ thy) tm; val T = type_check context tm'; val _ = if prop andalso T <> propT then err "Term not of type prop" else (); val tm'' = tm' |> Consts.certify context (tsig_of thy) do_expand consts |> Soft_Type_System.global_purge thy; in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end; fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy; fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy; val cert_term = #1 oo certify_term; fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy; end; (* specifications *) fun no_variables kind add addT mk mkT ctxt tm = (case (add tm [], addT tm []) of ([], []) => tm | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees))))); val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree; val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar; (** signature extension functions **) (*exception ERROR/TYPE*) (* add type constructors *) fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) => let val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx); val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn; val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig; in (syn', tsig', consts) end); fun add_types_global types thy = fold (add_type (Syntax.init_pretty_global thy)) types thy; (* add nonterminals *) fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts)); fun add_nonterminals_global ns thy = add_nonterminals (Syntax.init_pretty_global thy) ns thy; (* add type abbreviations *) fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts)); (* modify syntax *) fun gen_syntax parse_typ add mode args thy = let val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy); fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c); in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end; val syntax = gen_syntax (K I); val syntax_cmd = gen_syntax Syntax.read_typ; fun type_notation add mode args = let fun type_syntax (Type (c, args), mx) = SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end; fun notation add mode args thy = let fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; in syntax add mode (map_filter const_syntax args) thy end; (* add constants *) local fun gen_add_consts prep_typ ctxt raw_args thy = let val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt; fun prep (b, raw_T, mx) = let val c = full_name thy b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ Binding.print b); val T' = Logic.varifyT_global T; in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) |> syntax true Syntax.mode_default (map #2 args) |> pair (map #3 args) end; in fun add_consts args thy = #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy); fun add_consts_cmd args thy = #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx); fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy; end; (* abbreviations *) fun add_abbrev mode (b, raw_t) thy = (* FIXME proper ctxt (?) *) let val ctxt = Syntax.init_pretty_global thy; val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy; val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg) handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val (res, consts') = consts_of thy |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t); in (res, thy |> map_consts (K consts')) end; fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c); (* add constraints *) fun add_const_constraint (c, opt_T) thy = let fun prepT raw_T = let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T))) in cert_term thy (Const (c, T)); T end handle TYPE (msg, _, _) => error msg; in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; (* primitive classes and arities *) fun primitive_class (bclass, classes) thy = thy |> map_sign (fn (syn, tsig, consts) => let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig; in (syn, tsig', consts) end) |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg); fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.Theory thy) arg); (* add translation functions *) local fun mk trs = map Syntax_Ext.mk_trfun trs; in fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], [])); fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], [])); fun print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), [])); fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, [])); fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's)); end; (* translation rules *) val add_trrules = map_syn o Syntax.update_trrules; val del_trrules = map_syn o Syntax.remove_trrules; (* naming *) val get_scope = Name_Space.get_scope o naming_of; fun new_scope thy = let val (scope, naming') = Name_Space.new_scope (naming_of thy); val thy' = map_naming (K naming') thy; in (scope, thy') end; val new_group = map_naming Name_Space.new_group; val reset_group = map_naming Name_Space.reset_group; val add_path = map_naming o Name_Space.add_path; val root_path = map_naming Name_Space.root_path; val parent_path = map_naming Name_Space.parent_path; val mandatory_path = map_naming o Name_Space.mandatory_path; val qualified_path = map_naming oo Name_Space.qualified_path; fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy); fun init_naming thy = let val theory_naming = Name_Space.global_naming |> Name_Space.set_theory_long_name (Context.theory_long_name thy); in map_naming (K theory_naming) thy end; val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* hide names *) val hide_class = map_tsig oo Type.hide_class; val hide_type = map_tsig oo Type.hide_type; val hide_const = map_consts oo Consts.hide; end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,353 +1,350 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val local_setup: (Proof.context -> Proof.context) -> unit val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory - val join_theory: theory list -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_const: string -> theory -> theory val add_deps_type: string -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun local_setup f = Context.>> (Context.map_proof f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; +fun rep_thy (Thy args) = args; + fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], [])); - fun merge old_thys (thy1, thy2) = + fun merge args = let - val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; - val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; + val thy0 = #1 (hd args); + val {pos, id, ...} = rep_thy (#2 (hd args)); - val axioms' = Name_Space.merge_tables (axioms1, axioms2); - val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); - val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); - val ens' = Library.merge (eq_snd op =) (ens1, ens2); + val merge_defs = Defs.merge (Defs.global_context thy0); + val merge_wrappers = Library.merge (eq_snd op =); + + val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args); + val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args); + val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args); + val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args); in make_thy (pos, id, axioms', defs', (bgs', ens')) end; ); -fun rep_theory thy = Thy.get thy |> (fn Thy args => args); +val rep_theory = rep_thy o Thy.get; fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Position.make_entity_markup def id Markup.theoryN (name, pos); fun init_markup (name, pos) thy = let val id = serial (); val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)]; in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup {def = false} (Context.theory_long_name thy) id pos end; fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = Context.get_theory long thy name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => map (Context.theory_name long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; -(* join theory *) - -fun join_theory [] = raise List.Empty - | join_theory [thy] = thy - | join_theory thys = foldl1 Context.join_thys thys; - - (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.init_naming |> Sign.local_path |> apply_wrappers wrappers |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs)); val rhs_extras = TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd)) |> TFrees.keys; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun add_deps_const c thy = let val T = Logic.unvarifyT_global (Sign.the_const_type thy c); in thy |> add_deps_global "" (const_dep thy (c, T)) [] end; fun add_deps_type c thy = let val n = Sign.arity_number thy c; val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); in thy |> add_deps_global "" (type_dep (c, args)) [] end fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; end;