# HG changeset patch # User wenzelm # Date 1114113726 -7200 # Node ID d2f5ca3c048d88f68d95f303740e5b9e5cb68431 # Parent f2215ed004386c39f3f8676a118005b80d053f26 superceded by Pure.thy and CPure.thy; diff -r f2215ed00438 -r d2f5ca3c048d NEWS --- a/NEWS Thu Apr 21 22:00:28 2005 +0200 +++ b/NEWS Thu Apr 21 22:02:06 2005 +0200 @@ -189,6 +189,13 @@ * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific selections of theorems in named facts via indices. +* Pure: reorganized bootstrapping of the Pure theories; CPure is now + derived from Pure, which contains all common declarations already. + Both theories are defined via plain Isabelle/Isar .thy files. + INCOMPATIBILITY: elements of CPure (such as the CPure.intro / + CPure.elim / CPure.dest attributes) now appear in the Pure name + space; use isatool fixcpure to adapt your theory and ML sources. + *** Document preparation *** diff -r f2215ed00438 -r d2f5ca3c048d bin/isabelle-process --- a/bin/isabelle-process Thu Apr 21 22:00:28 2005 +0200 +++ b/bin/isabelle-process Thu Apr 21 22:02:06 2005 +0200 @@ -1,10 +1,7 @@ #!/usr/bin/env bash # - # $Id$ - # Author: Markus Wenzel, TU Muenchen -# License: GPL (GNU GENERAL PUBLIC LICENSE) # # Isabelle process startup script. diff -r f2215ed00438 -r d2f5ca3c048d src/HOL/Bali/DefiniteAssignment.thy --- a/src/HOL/Bali/DefiniteAssignment.thy Thu Apr 21 22:00:28 2005 +0200 +++ b/src/HOL/Bali/DefiniteAssignment.thy Thu Apr 21 22:02:06 2005 +0200 @@ -1346,7 +1346,7 @@ subseteq_B_B': "B \ B'" shows "\ A'. Env \ B' \t\ A'" proof - - note assigned.select_convs [CPure.intro] + note assigned.select_convs [Pure.intro] from da show "\ B'. B \ B' \ \ A'. Env\ B' \t\ A'" (is "PROP ?Hyp Env B t") proof (induct) diff -r f2215ed00438 -r d2f5ca3c048d src/HOL/Extraction/Higman.thy --- a/src/HOL/Extraction/Higman.thy Thu Apr 21 22:00:28 2005 +0200 +++ b/src/HOL/Extraction/Higman.thy Thu Apr 21 22:02:06 2005 +0200 @@ -20,50 +20,50 @@ inductive emb intros - emb0 [CPure.intro]: "([], bs) \ emb" - emb1 [CPure.intro]: "(as, bs) \ emb \ (as, b # bs) \ emb" - emb2 [CPure.intro]: "(as, bs) \ emb \ (a # as, a # bs) \ emb" + emb0 [Pure.intro]: "([], bs) \ emb" + emb1 [Pure.intro]: "(as, bs) \ emb \ (as, b # bs) \ emb" + emb2 [Pure.intro]: "(as, bs) \ emb \ (a # as, a # bs) \ emb" consts L :: "letter list \ letter list list set" inductive "L v" intros - L0 [CPure.intro]: "(w, v) \ emb \ w # ws \ L v" - L1 [CPure.intro]: "ws \ L v \ w # ws \ L v" + L0 [Pure.intro]: "(w, v) \ emb \ w # ws \ L v" + L1 [Pure.intro]: "ws \ L v \ w # ws \ L v" consts good :: "letter list list set" inductive good intros - good0 [CPure.intro]: "ws \ L w \ w # ws \ good" - good1 [CPure.intro]: "ws \ good \ w # ws \ good" + good0 [Pure.intro]: "ws \ L w \ w # ws \ good" + good1 [Pure.intro]: "ws \ good \ w # ws \ good" consts R :: "letter \ (letter list list \ letter list list) set" inductive "R a" intros - R0 [CPure.intro]: "([], []) \ R a" - R1 [CPure.intro]: "(vs, ws) \ R a \ (w # vs, (a # w) # ws) \ R a" + R0 [Pure.intro]: "([], []) \ R a" + R1 [Pure.intro]: "(vs, ws) \ R a \ (w # vs, (a # w) # ws) \ R a" consts T :: "letter \ (letter list list \ letter list list) set" inductive "T a" intros - T0 [CPure.intro]: "a \ b \ (ws, zs) \ R b \ (w # zs, (a # w) # zs) \ T a" - T1 [CPure.intro]: "(ws, zs) \ T a \ (w # ws, (a # w) # zs) \ T a" - T2 [CPure.intro]: "a \ b \ (ws, zs) \ T a \ (ws, (b # w) # zs) \ T a" + T0 [Pure.intro]: "a \ b \ (ws, zs) \ R b \ (w # zs, (a # w) # zs) \ T a" + T1 [Pure.intro]: "(ws, zs) \ T a \ (w # ws, (a # w) # zs) \ T a" + T2 [Pure.intro]: "a \ b \ (ws, zs) \ T a \ (ws, (b # w) # zs) \ T a" consts bar :: "letter list list set" inductive bar intros - bar1 [CPure.intro]: "ws \ good \ ws \ bar" - bar2 [CPure.intro]: "(\w. w # ws \ bar) \ ws \ bar" + bar1 [Pure.intro]: "ws \ good \ ws \ bar" + bar2 [Pure.intro]: "(\w. w # ws \ bar) \ ws \ bar" theorem prop1: "([] # ws) \ bar" by rules diff -r f2215ed00438 -r d2f5ca3c048d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Apr 21 22:00:28 2005 +0200 +++ b/src/HOL/HOL.thy Thu Apr 21 22:02:06 2005 +0200 @@ -11,28 +11,6 @@ ("~~/src/Provers/eqsubst.ML") begin -subsection {* Rules That Belong in Pure *} - -text{*These meta-level elimination rules facilitate the use of assumptions -that contain !! and ==>, especially in linear scripts. *} - -lemma meta_mp: - assumes major: "PROP P ==> PROP Q" and minor: "PROP P" - shows "PROP Q" -proof - - show "PROP Q" by (rule major [OF minor]) -qed - -lemma meta_spec: - assumes major: "!!x. PROP P x" - shows "PROP P x" -proof - - show "PROP P x" by (rule major) -qed - -lemmas meta_allE = meta_spec [CPure.elim_format] - - subsection {* Primitive logic *} subsubsection {* Core syntax *} @@ -849,14 +827,14 @@ with 1 show R by (rule notE) qed -lemmas [CPure.elim!] = disjE iffE FalseE conjE exE - and [CPure.intro!] = iffI conjI impI TrueI notI allI refl - and [CPure.elim 2] = allE notE' impE' - and [CPure.intro] = exI disjI2 disjI1 +lemmas [Pure.elim!] = disjE iffE FalseE conjE exE + and [Pure.intro!] = iffI conjI impI TrueI notI allI refl + and [Pure.elim 2] = allE notE' impE' + and [Pure.intro] = exI disjI2 disjI1 lemmas [trans] = trans and [sym] = sym not_sym - and [CPure.elim?] = iffD1 iffD2 impE + and [Pure.elim?] = iffD1 iffD2 impE subsubsection {* Atomizing meta-level connectives *} diff -r f2215ed00438 -r d2f5ca3c048d src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Apr 21 22:00:28 2005 +0200 +++ b/src/HOL/Transitive_Closure.thy Thu Apr 21 22:02:06 2005 +0200 @@ -25,16 +25,16 @@ inductive "r^*" intros - rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*" - rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" + rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*" + rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" consts trancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^+)" [1000] 999) inductive "r^+" intros - r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+" - trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" + r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" + trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" syntax "_reflcl" :: "('a \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/IsaMakefile Thu Apr 21 22:02:06 2005 +0200 @@ -23,43 +23,42 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: General/ROOT.ML General/buffer.ML General/file.ML \ - General/graph.ML General/heap.ML General/history.ML \ - General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML \ - General/object.ML General/output.ML General/path.ML General/position.ML\ - General/pretty.ML General/scan.ML General/seq.ML General/source.ML \ - General/susp.ML General/symbol.ML General/table.ML General/url.ML \ - General/xml.ML\ - IsaPlanner/isaplib.ML IsaPlanner/term_lib.ML\ - IsaPlanner/isa_fterm.ML IsaPlanner/upterm_lib.ML\ - IsaPlanner/focus_term_lib.ML\ - IsaPlanner/rw_tools.ML IsaPlanner/rw_inst.ML\ - IsaPlanner/isand.ML\ - Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \ - Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML\ - Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \ - Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML\ - Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML \ - Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML \ - Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \ - Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML \ - Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML\ - ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \ - ML-Systems/polyml.ML ML-Systems/polyml-time-limit.ML \ - ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML \ - ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML \ - ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML \ - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML Proof/proofchecker.ML\ - Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ - Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \ - Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML\ - Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML Thy/thm_database.ML\ - Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML \ - Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML codegen.ML context.ML display.ML\ - drule.ML envir.ML fact_index.ML goals.ML install_pp.ML library.ML logic.ML\ - meta_simplifier.ML net.ML pattern.ML proof_general.ML proofterm.ML pure.ML\ - pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML\ - theory_data.ML thm.ML type.ML type_infer.ML unify.ML +$(OUT)/Pure: General/ROOT.ML General/buffer.ML General/file.ML \ + General/graph.ML General/heap.ML General/history.ML \ + General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML \ + General/object.ML General/output.ML General/path.ML \ + General/position.ML General/pretty.ML General/scan.ML General/seq.ML \ + General/source.ML General/susp.ML General/symbol.ML General/table.ML \ + General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \ + IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML \ + IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML \ + IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \ + Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML \ + Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \ + Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML \ + Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML \ + Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML \ + Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \ + Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML \ + Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML \ + ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \ + ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \ + ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML \ + ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML \ + ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML \ + Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ + Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML \ + Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML \ + Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \ + Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ + Syntax/type_ext.ML Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML \ + Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML \ + Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML codegen.ML \ + context.ML display.ML drule.ML envir.ML fact_index.ML goals.ML \ + install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML pattern.ML \ + proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML sorts.ML \ + tactic.ML tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML \ + type_infer.ML unify.ML CPure.thy @./mk diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Apr 21 22:02:06 2005 +0200 @@ -40,7 +40,6 @@ val no_args: 'a attribute -> src -> 'a attribute val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute val attribute: (theory attribute * ProofContext.context attribute) -> src - val setup: (theory -> theory) list end; structure Attrib: ATTRIB = @@ -82,6 +81,7 @@ end; structure AttributesData = TheoryDataFun(AttributesDataArgs); +val _ = Context.add_setup [AttributesData.init]; val print_attributes = AttributesData.print; @@ -487,15 +487,12 @@ fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x; fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x; -val setup_internal_attribute = +val _ = Context.add_setup [PureThy.global_path, add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")], PureThy.local_path]; - -(** theory setup **) - (* pure_attributes *) val pure_attributes = @@ -522,14 +519,10 @@ ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")] @ rule_atts; - -(* setup *) +val _ = Context.add_setup [add_attributes pure_attributes]; -val setup = - AttributesData.init :: setup_internal_attribute @ [add_attributes pure_attributes]; end; structure BasicAttrib: BASIC_ATTRIB = Attrib; open BasicAttrib; - diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/calculation.ML Thu Apr 21 22:02:06 2005 +0200 @@ -25,7 +25,6 @@ -> Proof.state -> Proof.state Seq.seq val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state - val setup: (theory -> theory) list end; structure Calculation: CALCULATION = @@ -54,6 +53,7 @@ end; structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs); +val _ = Context.add_setup [GlobalCalculation.init]; val print_global_rules = GlobalCalculation.print; @@ -69,6 +69,7 @@ end; structure LocalCalculation = ProofDataFun(LocalCalculationArgs); +val _ = Context.add_setup [LocalCalculation.init]; val get_local_rules = #1 o LocalCalculation.get o Proof.context_of; val print_local_rules = LocalCalculation.print; @@ -129,6 +130,16 @@ (Attrib.add_del_args sym_add_global sym_del_global, Attrib.add_del_args sym_add_local sym_del_local); +val _ = Context.add_setup + [Attrib.add_attributes + [("trans", trans_attr, "declaration of transitivity rule"), + ("sym", sym_attr, "declaration of symmetry rule"), + ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local), + "resolution with symmetry rule")], + #1 o PureThy.add_thms + [(("", transitive_thm), [trans_add_global]), + (("", symmetric_thm), [sym_add_global])]]; + (** proof commands **) @@ -207,18 +218,4 @@ fun ultimately print = collect true print; - -(** theory setup **) - -val setup = - [GlobalCalculation.init, LocalCalculation.init, - Attrib.add_attributes - [("trans", trans_attr, "declaration of transitivity rule"), - ("sym", sym_attr, "declaration of symmetry rule"), - ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local), - "resolution with symmetry rule")], - #1 o PureThy.add_thms - [(("", transitive_thm), [trans_add_global]), - (("", symmetric_thm), [sym_add_global])]]; - end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/context_rules.ML Thu Apr 21 22:02:06 2005 +0200 @@ -49,7 +49,6 @@ val addXEs_local: ProofContext.context * thm list -> ProofContext.context val addXDs_local: ProofContext.context * thm list -> ProofContext.context val delrules_local: ProofContext.context * thm list -> ProofContext.context - val setup: (theory -> theory) list end; structure ContextRules: CONTEXT_RULES = @@ -145,6 +144,7 @@ end; structure GlobalRules = TheoryDataFun(GlobalRulesArgs); +val _ = Context.add_setup [GlobalRules.init]; val print_global_rules = GlobalRules.print; structure LocalRulesArgs = @@ -156,6 +156,7 @@ end; structure LocalRules = ProofDataFun(LocalRulesArgs); +val _ = Context.add_setup [LocalRules.init]; val print_local_rules = LocalRules.print; @@ -248,6 +249,9 @@ end; +val _ = Context.add_setup + [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]]; + (* low-level modifiers *) @@ -265,11 +269,4 @@ val delrules_local = modifier rule_del_local; - -(** theory setup **) - -val setup = - [GlobalRules.init, LocalRules.init]; - - end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/induct_attrib.ML --- a/src/Pure/Isar/induct_attrib.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/induct_attrib.ML Thu Apr 21 22:02:06 2005 +0200 @@ -36,7 +36,6 @@ val inductN: string val typeN: string val setN: string - val setup: (theory -> theory) list end; structure InductAttrib: INDUCT_ATTRIB = @@ -126,6 +125,7 @@ end; structure GlobalInduct = TheoryDataFun(GlobalInductArgs); +val _ = Context.add_setup [GlobalInduct.init]; val print_global_rules = GlobalInduct.print; val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; @@ -142,6 +142,7 @@ end; structure LocalInduct = ProofDataFun(LocalInductArgs); +val _ = Context.add_setup [LocalInduct.init]; val print_local_rules = LocalInduct.print; val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get; @@ -223,15 +224,10 @@ end; +val _ = Context.add_setup + [Attrib.add_attributes + [(casesN, cases_attr, "declaration of cases rule for type or set"), + (inductN, induct_attr, "declaration of induction rule for type or set")]]; -(** theory setup **) - -val setup = - [GlobalInduct.init, LocalInduct.init, - Attrib.add_attributes - [(casesN, cases_attr, "declaration of cases rule for type or set"), - (inductN, induct_attr, "declaration of induction rule for type or set")]]; - end; - diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 21 22:02:06 2005 +0200 @@ -257,7 +257,7 @@ val setupP = OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl - (P.text >> (Toplevel.theory o Context.use_setup)); + (P.text >> (Toplevel.theory o IsarThy.generic_setup)); val method_setupP = OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Apr 21 22:02:06 2005 +0200 @@ -151,6 +151,7 @@ val typed_print_translation: bool * string -> theory -> theory val print_ast_translation: bool * string -> theory -> theory val token_translation: string -> theory -> theory + val generic_setup: string -> theory -> theory val method_setup: bstring * string * string -> theory -> theory val add_oracle: bstring * string -> theory -> theory val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory @@ -581,7 +582,13 @@ "Theory.add_tokentrfuns token_translation"; -(* add method *) +(* generic_setup *) + +val generic_setup = + Context.use_let "val setup: (theory -> theory) list" "Library.apply setup"; + + +(* method_setup *) fun method_setup (name, txt, cmt) = Context.use_let diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/locale.ML Thu Apr 21 22:02:06 2005 +0200 @@ -90,9 +90,6 @@ string * term list -> thm -> theory -> theory val add_local_witness: string * term list -> thm -> context -> context - - (* Theory setup for locales *) - val setup: (theory -> theory) list end; structure Locale: LOCALE = @@ -183,6 +180,9 @@ end; structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); +val _ = Context.add_setup [GlobalLocalesData.init]; + + (** context data **) @@ -199,6 +199,7 @@ end; structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); +val _ = Context.add_setup [LocalLocalesData.init]; (* access locales *) @@ -1882,11 +1883,14 @@ in val add_locale = gen_add_locale read_context intern_expr; - val add_locale_i = gen_add_locale cert_context (K I); end; +val _ = Context.add_setup + [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]], + add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]]; + (** Interpretation commands **) @@ -2090,13 +2094,4 @@ end; (* local *) - -(** locale theory setup **) - -val setup = - [GlobalLocalesData.init, LocalLocalesData.init, - add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]], - add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]]; - end; - diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/method.ML Thu Apr 21 22:02:06 2005 +0200 @@ -115,7 +115,6 @@ -> src -> Proof.context -> Proof.method val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method - val setup: (theory -> theory) list end; structure Method: METHOD = @@ -529,6 +528,7 @@ end; structure MethodsData = TheoryDataFun(MethodsDataArgs); +val _ = Context.add_setup [MethodsData.init]; val print_methods = MethodsData.print; @@ -769,9 +769,6 @@ val global_done_proof = global_term_proof false (done_text, NONE); - -(** theory setup **) - (* misc tactic emulations *) val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac; @@ -812,17 +809,10 @@ ("prolog", thms_args prolog, "simple prolog interpreter"), ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]; - -(* setup *) - -val setup = - [MethodsData.init, add_methods pure_methods, - (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [ContextRules.intro_query_global NONE])])]; +val _ = Context.add_setup [add_methods pure_methods]; end; - structure BasicMethod: BASIC_METHOD = Method; open BasicMethod; - diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/object_logic.ML Thu Apr 21 22:02:06 2005 +0200 @@ -26,7 +26,6 @@ val rulify_no_asm: thm -> thm val rule_format: 'a attribute val rule_format_no_asm: 'a attribute - val setup: (theory -> theory) list end; structure ObjectLogic: OBJECT_LOGIC = @@ -58,6 +57,8 @@ end; structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs); +val _ = Context.add_setup [ObjectLogicData.init]; + (** generic treatment of judgments -- with a single argument only **) @@ -182,10 +183,4 @@ fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x; - -(** theory setup **) - -val setup = [ObjectLogicData.init]; - - end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 21 22:02:06 2005 +0200 @@ -6,6 +6,7 @@ *) val show_structs = ref false; +val thms_containing_limit = ref 40; signature PROOF_CONTEXT = sig @@ -153,9 +154,7 @@ val prems_limit: int ref val pretty_asms: context -> Pretty.T list val pretty_context: context -> Pretty.T list - val thms_containing_limit: int ref val print_thms_containing: context -> int option -> string list -> unit - val setup: (theory -> theory) list end; signature PRIVATE_PROOF_CONTEXT = @@ -268,6 +267,7 @@ end; structure ProofDataData = TheoryDataFun(ProofDataDataArgs); +val _ = Context.add_setup [ProofDataData.init]; val print_proof_data = ProofDataData.print; @@ -1464,8 +1464,6 @@ in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end; -val thms_containing_limit = ref 40; - fun print_thms_containing ctxt opt_limit ss = let val prt_term = pretty_term ctxt; @@ -1499,9 +1497,4 @@ end; - -(** theory setup **) - -val setup = [ProofDataData.init]; - end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Isar/skip_proof.ML Thu Apr 21 22:02:06 2005 +0200 @@ -15,7 +15,6 @@ (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq val global_skip_proof: bool -> Proof.state -> theory * ((string * string) * (string * thm list) list) - val setup: (theory -> theory) list end; structure SkipProof: SKIP_PROOF = @@ -38,8 +37,8 @@ if ! quick_and_dirty then t else error "Proof may be skipped in quick_and_dirty mode only!"; -val setup = - [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path]; +val _ = Context.add_setup + [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path]; (* basic cheating *) diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Apr 21 22:02:06 2005 +0200 @@ -25,8 +25,6 @@ val mk_typ : typ -> term val etype_of : theory -> string list -> typ list -> term -> typ val realizes_of: theory -> string list -> term -> term -> term - val parsers: OuterSyntax.parser list - val setup: (theory -> theory) list end; structure Extraction : EXTRACTION = @@ -226,6 +224,7 @@ end; structure ExtractionData = TheoryDataFun(ExtractionArgs); +val _ = Context.add_setup [ExtractionData.init]; fun read_condeq thy = let val sg = sign_of (add_syntax thy) @@ -404,6 +403,7 @@ fun add_expand_thms thms thy = Library.foldl (fst o add_expand_thm) (thy, thms); + (** types with computational content **) fun add_types tys thy = @@ -417,6 +417,58 @@ end; +(** Pure setup **) + +val _ = Context.add_setup + [add_types [("prop", ([], NONE))], + + add_typeof_eqns + ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ + \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ + \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))", + + "(typeof (PROP Q)) == (Type (TYPE(Null))) ==> \ + \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE(Null)))", + + "(typeof (PROP P)) == (Type (TYPE('P))) ==> \ + \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ + \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('P => 'Q)))", + + "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ + \ (typeof (!!x. PROP P (x))) == (Type (TYPE(Null)))", + + "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==> \ + \ (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))", + + "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==> \ + \ (typeof (f)) == (Type (TYPE('f)))"], + + add_realizes_eqns + ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ + \ (realizes (r) (PROP P ==> PROP Q)) == \ + \ (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))", + + "(typeof (PROP P)) == (Type (TYPE('P))) ==> \ + \ (typeof (PROP Q)) == (Type (TYPE(Null))) ==> \ + \ (realizes (r) (PROP P ==> PROP Q)) == \ + \ (!!x::'P. PROP realizes (x) (PROP P) ==> PROP realizes (Null) (PROP Q))", + + "(realizes (r) (PROP P ==> PROP Q)) == \ + \ (!!x. PROP realizes (x) (PROP P) ==> PROP realizes (r (x)) (PROP Q))", + + "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ + \ (realizes (r) (!!x. PROP P (x))) == \ + \ (!!x. PROP realizes (Null) (PROP P (x)))", + + "(realizes (r) (!!x. PROP P (x))) == \ + \ (!!x. PROP realizes (r (x)) (PROP P (x)))"], + + Attrib.add_attributes + [("extraction_expand", + (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute), + "specify theorems / definitions to be expanded during extraction")]]; + + (**** extract program ****) val dummyt = Const ("dummy", dummyT); @@ -753,61 +805,8 @@ (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy))); -val parsers = [realizersP, realizabilityP, typeofP, extractP]; - -val setup = - [ExtractionData.init, - - add_types [("prop", ([], NONE))], - - add_typeof_eqns - ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ - \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ - \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))", - - "(typeof (PROP Q)) == (Type (TYPE(Null))) ==> \ - \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE(Null)))", - - "(typeof (PROP P)) == (Type (TYPE('P))) ==> \ - \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ - \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('P => 'Q)))", - - "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ - \ (typeof (!!x. PROP P (x))) == (Type (TYPE(Null)))", - - "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==> \ - \ (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))", - - "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==> \ - \ (typeof (f)) == (Type (TYPE('f)))"], - - add_realizes_eqns - ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ - \ (realizes (r) (PROP P ==> PROP Q)) == \ - \ (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))", - - "(typeof (PROP P)) == (Type (TYPE('P))) ==> \ - \ (typeof (PROP Q)) == (Type (TYPE(Null))) ==> \ - \ (realizes (r) (PROP P ==> PROP Q)) == \ - \ (!!x::'P. PROP realizes (x) (PROP P) ==> PROP realizes (Null) (PROP Q))", - - "(realizes (r) (PROP P ==> PROP Q)) == \ - \ (!!x. PROP realizes (x) (PROP P) ==> PROP realizes (r (x)) (PROP Q))", - - "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ - \ (realizes (r) (!!x. PROP P (x))) == \ - \ (!!x. PROP realizes (Null) (PROP P (x)))", - - "(realizes (r) (!!x. PROP P (x))) == \ - \ (!!x. PROP realizes (r (x)) (PROP P (x)))"], - - Attrib.add_attributes - [("extraction_expand", - (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute), - "specify theorems / definitions to be expanded during extraction")]]; +val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP]; val etype_of = etype_of o sign_of o add_syntax; end; - -OuterSyntax.add_parsers Extraction.parsers; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 21 22:02:06 2005 +0200 @@ -12,7 +12,6 @@ val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof - val setup : (theory -> theory) list end; structure ProofRewriteRules : PROOF_REWRITE_RULES = @@ -182,7 +181,7 @@ in rew' end; fun rprocs b = [("Pure/meta_equality", rew b)]; -val setup = [Proofterm.add_prf_rprocs (rprocs false)]; +val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)]; (**** apply rewriting function to all terms in proof ****) diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/ROOT.ML Thu Apr 21 22:02:06 2005 +0200 @@ -63,7 +63,7 @@ use "codegen.ML"; use "Proof/extraction.ML"; -(*old-style goal package*) +(*old goal package -- obsolete*) use "goals.ML"; (*the IsaPlanner subsystem*) @@ -72,8 +72,10 @@ (*configuration for Proof General*) use "proof_general.ML"; -(*final Pure theory setup*) -use "pure.ML"; +(*the Pure theories*) +use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end; +use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end; + (*several object-logics declare theories that hide basis library structures*) structure BasisLibrary = diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/html.ML Thu Apr 21 22:02:06 2005 +0200 @@ -38,7 +38,6 @@ val section: string -> text val subsection: string -> text val subsubsection: string -> text - val setup: (theory -> theory) list end; structure HTML: HTML = @@ -254,6 +253,8 @@ ("var", style "var"), ("xstr", style "xstr")]; +val _ = Context.add_setup [Theory.add_mode_tokentrfuns htmlN html_trans]; + (** HTML markup **) @@ -427,10 +428,4 @@ fun subsubsection heading = "\n\n

" ^ plain heading ^ "

\n"; -(** theory setup **) - -val setup = - [Theory.add_mode_tokentrfuns htmlN html_trans]; - - end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/latex.ML Thu Apr 21 22:02:06 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -LaTeX presentation primitives (based on outer lexical syntax). +LaTeX presentation elements -- based on outer lexical syntax. *) signature LATEX = diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/present.ML Thu Apr 21 22:02:06 2005 +0200 @@ -34,7 +34,6 @@ val subsection: string -> unit val subsubsection: string -> unit val drafts: string -> Path.T list -> Path.T - val setup: (theory -> theory) list end; structure Present: PRESENT = @@ -86,6 +85,7 @@ end; structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs); +val _ = Context.add_setup [BrowserInfoData.init]; fun get_info thy = if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty @@ -533,11 +533,6 @@ in Path.ext doc_format doc_path end; - -(** theory setup **) - -val setup = [BrowserInfoData.init]; - end; structure BasicPresent: BASIC_PRESENT = Present; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/thm_database.ML Thu Apr 21 22:02:06 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Interface to thm database. +Interface to the theorem database. *) signature BASIC_THM_DATABASE = diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Apr 21 22:02:06 2005 +0200 @@ -2,7 +2,8 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Theory loader database, including theory and file dependencies. +Main part of theory loader database, including handling of theory and +file dependencies. *) signature BASIC_THY_INFO = @@ -472,6 +473,8 @@ else (change_thys register; perform Update name) end; +val _ = register_theory ProtoPure.thy; + (*final declarations of this structure*) val theory = get_theory; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Apr 21 22:02:06 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Theory loader primitives. +Theory loader primitives, including load path. *) signature BASIC_THY_LOAD = diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/axclass.ML Thu Apr 21 22:02:06 2005 +0200 @@ -29,10 +29,9 @@ val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T - val setup: (theory -> theory) list end; -structure AxClass : AX_CLASS = +structure AxClass: AX_CLASS = struct @@ -192,6 +191,7 @@ end; structure AxclassesData = TheoryDataFun(AxclassesArgs); +val _ = Context.add_setup [AxclassesData.init]; val print_axclasses = AxclassesData.print; @@ -292,20 +292,13 @@ end; -(* intro_classes *) +(* proof methods *) fun intro_classes_tac facts st = (ALLGOALS (Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) THEN Tactic.distinct_subgoals_tac) st; -val intro_classes_method = - ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), - "back-chain introduction rules of axiomatic type classes"); - - -(* default method *) - fun default_intro_classes_tac [] = intro_classes_tac [] | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) @@ -313,8 +306,10 @@ HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE default_intro_classes_tac facts; -val default_method = - ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule"); +val _ = Context.add_setup [Method.add_methods + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + "back-chain introduction rules of axiomatic type classes"), + ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]]; (* old-style axclass_tac *) @@ -419,16 +414,6 @@ val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; - -(** package setup **) - -(* setup theory *) - -val setup = - [AxclassesData.init, - Method.add_methods [intro_classes_method, default_method]]; - - (* outer syntax *) local structure P = OuterParse and K = OuterSyntax.Keyword in @@ -450,4 +435,3 @@ end; end; - diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/codegen.ML Thu Apr 21 22:02:06 2005 +0200 @@ -55,8 +55,6 @@ val test_fn: (int -> (string * term) list option) ref val test_term: theory -> int -> int -> term -> (string * term) list option val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list - val parsers: OuterSyntax.parser list - val setup: (theory -> theory) list end; structure Codegen : CODEGEN = @@ -169,6 +167,7 @@ end; structure CodegenData = TheoryDataFun(CodegenArgs); +val _ = Context.add_setup [CodegenData.init]; val print_codegens = CodegenData.print; @@ -228,6 +227,11 @@ Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser (#attrs (CodegenData.get thy))))); +val _ = Context.add_setup + [Attrib.add_attributes + [("code", (code_attr, K Attrib.undef_local_attribute), + "declare theorems for code generation")]]; + (**** preprocessors ****) @@ -254,6 +258,8 @@ else th) in (add_preprocessor prep thy, eqn) end; +val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)]; + (**** associate constants with target language code ****) @@ -287,6 +293,7 @@ val assoc_consts_i = gen_assoc_consts (K I); val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg); + (**** associate types with target language types ****) fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) => @@ -553,6 +560,10 @@ (invoke_tycodegen thy dep false) (gr', quotes_of ms) in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end); +val _ = Context.add_setup + [add_codegen "default" default_codegen, + add_tycodegen "default" default_tycodegen]; + fun output_code gr xs = implode (map (snd o Graph.get_node gr) (rev (Graph.all_preds gr xs))); @@ -698,6 +709,10 @@ (p, []) => p | _ => error ("Malformed annotation: " ^ quote s)); +val _ = Context.add_setup + [assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]]; + + structure P = OuterParse and K = OuterSyntax.Keyword; val assoc_typeP = @@ -761,18 +776,7 @@ (map (fn f => f (Toplevel.sign_of st))) ps, [])) (get_test_params (Toplevel.theory_of st), [])) g st))); -val parsers = [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP]; - -val setup = - [CodegenData.init, - add_codegen "default" default_codegen, - add_tycodegen "default" default_tycodegen, - assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")], - Attrib.add_attributes [("code", - (code_attr, K Attrib.undef_local_attribute), - "declare theorems for code generation")], - add_attribute "unfold" (Scan.succeed unfold_attr)]; +val _ = OuterSyntax.add_parsers + [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP]; end; - -OuterSyntax.add_parsers Codegen.parsers; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/context.ML --- a/src/Pure/context.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/context.ML Thu Apr 21 22:02:06 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Global theory context. +Theory contexts. *) signature BASIC_CONTEXT = @@ -26,14 +26,15 @@ val use_mltext: string -> bool -> theory option -> unit val use_mltext_theory: string -> bool -> theory -> theory val use_let: string -> string -> string -> theory -> theory - val use_setup: string -> theory -> theory + val add_setup: (theory -> theory) list -> unit + val setup: unit -> (theory -> theory) list end; structure Context: CONTEXT = struct -(* theory context *) +(** implicit theory context in ML **) local val current_theory = ref (NONE: theory option); @@ -82,8 +83,16 @@ fun use_let bind body txt = use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); -val use_setup = - use_let "val setup: (theory -> theory) list" "Library.apply setup"; + + +(** delayed theory setup **) + +local + val setup_fns = ref ([]: (theory -> theory) list); +in + fun add_setup fns = setup_fns := ! setup_fns @ fns; + fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end; +end; end; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/goals.ML --- a/src/Pure/goals.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/goals.ML Thu Apr 21 22:02:06 2005 +0200 @@ -116,7 +116,6 @@ val close_locale: xstring -> theory -> theory val print_scope: theory -> unit val read_cterm: Sign.sg -> string * typ -> cterm - val setup: (theory -> theory) list end; structure Goals: GOALS = @@ -216,6 +215,7 @@ structure LocalesData = TheoryDataFun(LocalesArgs); +val _ = Context.add_setup [LocalesData.init]; val print_locales = LocalesData.print; @@ -627,12 +627,6 @@ else Sign.pretty_term sign; -(** locale theory setup **) - -val setup = - [LocalesData.init]; - - (*** Goal package ***) diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/proof_general.ML Thu Apr 21 22:02:06 2005 +0200 @@ -21,7 +21,6 @@ signature PROOF_GENERAL = sig - val setup: (theory -> theory) list val update_thy_only: string -> unit val try_update_thy_only: string -> unit val inform_file_retracted: string -> unit @@ -156,7 +155,11 @@ ("bound", tagit bound_tag), ("var", var_or_skolem)]; -in val setup = [Theory.add_tokentrfuns proof_general_trans] end; +in + +val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans]; + +end; (* assembling PGIP packets *) diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/pure.ML --- a/src/Pure/pure.ML Thu Apr 21 22:00:28 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -(* Title: Pure/pure.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Final setup of the Pure theories. -*) - -local - val common_setup = - ProofRewriteRules.setup @ - HTML.setup @ - ObjectLogic.setup @ - ProofContext.setup @ - Locale.setup @ - Attrib.setup @ - ContextRules.setup @ - InductAttrib.setup @ - Method.setup @ - Calculation.setup @ - SkipProof.setup @ - AxClass.setup @ - Present.setup @ - ProofGeneral.setup @ - Codegen.setup @ - Extraction.setup @ - Goals.setup; -in - structure Pure = - struct - val thy = - PureThy.begin_theory Sign.PureN [ProtoPure.thy] - |> Theory.add_syntax Syntax.pure_appl_syntax - |> Library.apply common_setup - |> PureThy.end_theory; - end; - - structure CPure = - struct - val thy = - PureThy.begin_theory Sign.CPureN [ProtoPure.thy] - |> Theory.add_syntax Syntax.pure_applC_syntax - |> Library.apply common_setup - |> Theory.copy - |> PureThy.end_theory; - end; -end; - -ThyInfo.register_theory ProtoPure.thy; -ThyInfo.register_theory Pure.thy; -ThyInfo.register_theory CPure.thy; diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/pure_thy.ML Thu Apr 21 22:02:06 2005 +0200 @@ -591,6 +591,7 @@ ("dummy", 0, NoSyn)] |> Theory.add_nonterminals Syntax.pure_nonterms |> Theory.add_syntax Syntax.pure_syntax + |> Theory.add_syntax Syntax.pure_appl_syntax |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax |> Theory.add_syntax [("==>", "[prop, prop] => prop", Delimfix "op ==>"), diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Apr 21 22:00:28 2005 +0200 +++ b/src/Pure/sign.ML Thu Apr 21 22:02:06 2005 +0200 @@ -226,8 +226,10 @@ fun rep_sg (Sg (_, args)) = args; -fun stamp_names_of (Sg ({stamps, ...}, _)) = rev (map ! stamps); -fun exists_stamp name (Sg ({stamps, ...}, _)) = exists (equal name o !) stamps; +fun stamps_of (Sg ({stamps, ...}, _)) = stamps; +val stamp_names_of = rev o map ! o stamps_of; +fun exists_stamp name = exists (equal name o !) o stamps_of; + fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg); val str_of_sg = Pretty.str_of o pretty_sg; val pprint_sg = Pretty.pprint o pretty_sg; @@ -275,11 +277,11 @@ fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) = (check_stale sg1; check_stale sg2; id1 = id2); - fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = - eq_sg (sg1, sg2) orelse mem_stamp (hd s1, s2); + fun subsig (sg1, sg2) = + eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2); - fun subsig_internal (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = - eq_sg (sg1, sg2) orelse subset_stamp (s1, s2); + fun subsig_internal (sg1, sg2) = + eq_sg (sg1, sg2) orelse subset_stamp (stamps_of sg1, stamps_of sg2); end; @@ -288,8 +290,8 @@ (*test if same theory names are contained in signatures' stamps, i.e. if signatures belong to same theory but not necessarily to the same version of it*) -fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = - eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2)); +fun same_sg (sg1, sg2) = + eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2)); (*test for drafts*) fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) = @@ -1187,9 +1189,8 @@ if subsig_internal (sg2, sg1) then sg1 else if subsig_internal (sg1, sg2) then sg2 else - if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse - exists_stamp CPureN sg1 andalso exists_stamp PureN sg2 - then error "Cannot merge Pure and CPure signatures" + if exists_stamp CPureN sg1 <> exists_stamp CPureN sg2 + then error "Cannot merge Pure and CPure developments" else let val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)}, @@ -1239,4 +1240,3 @@ end; end; -