--- 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 ***
--- 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.
--- 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 \<subseteq> B'"
shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
proof -
- note assigned.select_convs [CPure.intro]
+ note assigned.select_convs [Pure.intro]
from da
show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
proof (induct)
--- 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) \<in> emb"
- emb1 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (as, b # bs) \<in> emb"
- emb2 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (a # as, a # bs) \<in> emb"
+ emb0 [Pure.intro]: "([], bs) \<in> emb"
+ emb1 [Pure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (as, b # bs) \<in> emb"
+ emb2 [Pure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (a # as, a # bs) \<in> emb"
consts
L :: "letter list \<Rightarrow> letter list list set"
inductive "L v"
intros
- L0 [CPure.intro]: "(w, v) \<in> emb \<Longrightarrow> w # ws \<in> L v"
- L1 [CPure.intro]: "ws \<in> L v \<Longrightarrow> w # ws \<in> L v"
+ L0 [Pure.intro]: "(w, v) \<in> emb \<Longrightarrow> w # ws \<in> L v"
+ L1 [Pure.intro]: "ws \<in> L v \<Longrightarrow> w # ws \<in> L v"
consts
good :: "letter list list set"
inductive good
intros
- good0 [CPure.intro]: "ws \<in> L w \<Longrightarrow> w # ws \<in> good"
- good1 [CPure.intro]: "ws \<in> good \<Longrightarrow> w # ws \<in> good"
+ good0 [Pure.intro]: "ws \<in> L w \<Longrightarrow> w # ws \<in> good"
+ good1 [Pure.intro]: "ws \<in> good \<Longrightarrow> w # ws \<in> good"
consts
R :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
inductive "R a"
intros
- R0 [CPure.intro]: "([], []) \<in> R a"
- R1 [CPure.intro]: "(vs, ws) \<in> R a \<Longrightarrow> (w # vs, (a # w) # ws) \<in> R a"
+ R0 [Pure.intro]: "([], []) \<in> R a"
+ R1 [Pure.intro]: "(vs, ws) \<in> R a \<Longrightarrow> (w # vs, (a # w) # ws) \<in> R a"
consts
T :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
inductive "T a"
intros
- T0 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> R b \<Longrightarrow> (w # zs, (a # w) # zs) \<in> T a"
- T1 [CPure.intro]: "(ws, zs) \<in> T a \<Longrightarrow> (w # ws, (a # w) # zs) \<in> T a"
- T2 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> T a \<Longrightarrow> (ws, (b # w) # zs) \<in> T a"
+ T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> R b \<Longrightarrow> (w # zs, (a # w) # zs) \<in> T a"
+ T1 [Pure.intro]: "(ws, zs) \<in> T a \<Longrightarrow> (w # ws, (a # w) # zs) \<in> T a"
+ T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> T a \<Longrightarrow> (ws, (b # w) # zs) \<in> T a"
consts
bar :: "letter list list set"
inductive bar
intros
- bar1 [CPure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
- bar2 [CPure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
+ bar1 [Pure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
+ bar2 [Pure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
theorem prop1: "([] # ws) \<in> bar" by rules
--- 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 *}
--- 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 \<times> 'a) set => ('a \<times> '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 \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999)
--- 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
--- 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;
-
--- 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;
--- 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;
--- 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;
-
--- 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
--- 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
--- 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;
-
--- 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;
-
--- 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;
--- 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;
--- 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 *)
--- 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;
--- 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 ****)
--- 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 =
--- 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<h4>" ^ plain heading ^ "</h4>\n";
-(** theory setup **)
-
-val setup =
- [Theory.add_mode_tokentrfuns htmlN html_trans];
-
-
end;
--- 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 =
--- 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;
--- 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 =
--- 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;
--- 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 =
--- 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;
-
--- 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;
--- 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;
--- 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 ***)
--- 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 *)
--- 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;
--- 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 ==>"),
--- 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;
-