--- a/src/HOL/Import/Importer.thy Sun Mar 04 00:17:13 2012 +0100
+++ b/src/HOL/Import/Importer.thy Sun Mar 04 00:26:23 2012 +0100
@@ -4,10 +4,12 @@
theory Importer
imports Main
-uses "shuffler.ML" ("import_rews.ML") ("proof_kernel.ML") ("replay.ML") ("import.ML") ("import_syntax.ML")
+uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
begin
-setup Shuffler.setup
+setup {* Shuffler.setup #> importer_setup *}
+
+parse_ast_translation smarter_trueprop_parsing
lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
proof
@@ -220,20 +222,11 @@
lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
by simp
-use "import_rews.ML"
-
-setup importer_setup
-parse_ast_translation smarter_trueprop_parsing
-
use "proof_kernel.ML"
use "replay.ML"
use "import.ML"
setup Import.setup
-use "import_syntax.ML"
-
-ML {* Importer_Import_Syntax.setup() *}
-
end
--- a/src/HOL/Import/import.ML Sun Mar 04 00:17:13 2012 +0100
+++ b/src/HOL/Import/import.ML Sun Mar 04 00:26:23 2012 +0100
@@ -66,5 +66,224 @@
(fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
"import external theorem"
+(* Parsers *)
+
+val import_segment = Parse.name >> set_import_segment
+
+
+val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) =>
+ fn thy =>
+ thy |> set_generating_thy thyname
+ |> Sign.add_path thyname
+ |> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname))
+
+fun end_import toks =
+ Scan.succeed
+ (fn thy =>
+ let
+ val thyname = get_generating_thy thy
+ val segname = get_import_segment thy
+ val (int_thms,facts) = Replay.setup_int_thms thyname thy
+ val thmnames = filter_out (should_ignore thyname thy) facts
+ fun replay thy = Replay.import_thms thyname int_thms thmnames thy
+ in
+ thy |> clear_import_thy
+ |> set_segment thyname segname
+ |> set_used_names facts
+ |> replay
+ |> clear_used_names
+ |> export_importer_pending
+ |> Sign.parent_path
+ |> dump_import_thy thyname
+ |> add_dump ";end_setup"
+ end) toks
+
+val ignore_thms = Scan.repeat1 Parse.name
+ >> (fn ignored =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,thmname) => ignore_importer thyname thmname thy) (thy,ignored)
+ end)
+
+val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
+ >> (fn thmmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_mapping thyname hol isa thy) (thy,thmmaps)
+ end)
+
+val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
+ >> (fn typmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_type_mapping thyname hol false isa thy) (thy,typmaps)
+ end)
+
+val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
+ >> (fn defmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
+ end)
+
+val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
+ >> (fn renames =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_const_renaming thyname hol isa thy) (thy,renames)
+ end)
+
+val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
+ >> (fn constmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol false isa thy
+ | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+ end)
+
+val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
+ >> (fn constmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol true isa thy
+ | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+ end)
+
+fun import_thy location s =
+ let
+ val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp"))
+ val is = TextIO.openIn (File.platform_path src_location)
+ val inp = TextIO.inputAll is
+ val _ = TextIO.closeIn is
+ val orig_source = Source.of_string inp
+ val symb_source = Symbol.source orig_source
+ val lexes =
+ (Scan.make_lexicon
+ (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
+ Scan.empty_lexicon)
+ val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
+ val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
+ val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
+ val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
+ val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
+ val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
+ val const_movesP = Parse.$$$ "const_moves" |-- const_moves
+ val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
+ val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
+ val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
+ val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
+ val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
+ fun apply [] thy = thy
+ | apply (f::fs) thy = apply fs (f thy)
+ in
+ apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list))
+ end
+
+fun create_int_thms thyname thy =
+ if ! quick_and_dirty
+ then thy
+ else
+ case ImportData.get thy of
+ NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
+ | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
+
+fun clear_int_thms thy =
+ if ! quick_and_dirty
+ then thy
+ else
+ case ImportData.get thy of
+ NONE => error "Import data already cleared - forgotten a setup_theory?"
+ | SOME _ => ImportData.put NONE thy
+
+val setup_theory = (Parse.name -- Parse.name)
+ >>
+ (fn (location, thyname) =>
+ fn thy =>
+ (case Importer_DefThy.get thy of
+ NoImport => thy
+ | Generating _ => error "Currently generating a theory!"
+ | Replaying _ => thy |> clear_import_thy)
+ |> import_thy location thyname
+ |> create_int_thms thyname)
+
+fun end_setup toks =
+ Scan.succeed
+ (fn thy =>
+ let
+ val thyname = get_import_thy thy
+ val segname = get_import_segment thy
+ in
+ thy |> set_segment thyname segname
+ |> clear_import_thy
+ |> clear_int_thms
+ |> Sign.parent_path
+ end) toks
+
+val set_dump = Parse.string -- Parse.string >> setup_dump
+fun fl_dump toks = Scan.succeed flush_dump toks
+val append_dump = (Parse.verbatim || Parse.string) >> add_dump
+
+val _ =
+ (Keyword.keyword ">";
+ Outer_Syntax.command "import_segment"
+ "Set import segment name"
+ Keyword.thy_decl (import_segment >> Toplevel.theory);
+ Outer_Syntax.command "import_theory"
+ "Set default external theory name"
+ Keyword.thy_decl (import_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_import"
+ "End external import"
+ Keyword.thy_decl (end_import >> Toplevel.theory);
+ Outer_Syntax.command "setup_theory"
+ "Setup external theory replaying"
+ Keyword.thy_decl (setup_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_setup"
+ "End external setup"
+ Keyword.thy_decl (end_setup >> Toplevel.theory);
+ Outer_Syntax.command "setup_dump"
+ "Setup the dump file name"
+ Keyword.thy_decl (set_dump >> Toplevel.theory);
+ Outer_Syntax.command "append_dump"
+ "Add text to dump file"
+ Keyword.thy_decl (append_dump >> Toplevel.theory);
+ Outer_Syntax.command "flush_dump"
+ "Write the dump to file"
+ Keyword.thy_decl (fl_dump >> Toplevel.theory);
+ Outer_Syntax.command "ignore_thms"
+ "Theorems to ignore in next external theory import"
+ Keyword.thy_decl (ignore_thms >> Toplevel.theory);
+ Outer_Syntax.command "type_maps"
+ "Map external type names to existing Isabelle/HOL type names"
+ Keyword.thy_decl (type_maps >> Toplevel.theory);
+ Outer_Syntax.command "def_maps"
+ "Map external constant names to their primitive definitions"
+ Keyword.thy_decl (def_maps >> Toplevel.theory);
+ Outer_Syntax.command "thm_maps"
+ "Map external theorem names to existing Isabelle/HOL theorem names"
+ Keyword.thy_decl (thm_maps >> Toplevel.theory);
+ Outer_Syntax.command "const_renames"
+ "Rename external const names"
+ Keyword.thy_decl (const_renames >> Toplevel.theory);
+ Outer_Syntax.command "const_moves"
+ "Rename external const names to other external constants"
+ Keyword.thy_decl (const_moves >> Toplevel.theory);
+ Outer_Syntax.command "const_maps"
+ "Map external const names to existing Isabelle/HOL const names"
+ Keyword.thy_decl (const_maps >> Toplevel.theory));
+
end
--- a/src/HOL/Import/import_rews.ML Sun Mar 04 00:17:13 2012 +0100
+++ b/src/HOL/Import/import_rews.ML Sun Mar 04 00:26:23 2012 +0100
@@ -622,18 +622,12 @@
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
end
-local
- fun initial_maps thy =
- thy |> add_importer_type_mapping "min" "bool" false @{type_name bool}
- |> add_importer_type_mapping "min" "fun" false "fun"
- |> add_importer_type_mapping "min" "ind" false @{type_name ind}
- |> add_importer_const_mapping "min" "=" false @{const_name HOL.eq}
- |> add_importer_const_mapping "min" "==>" false @{const_name HOL.implies}
- |> add_importer_const_mapping "min" "@" false @{const_name "Eps"}
-in
val importer_setup =
- initial_maps #>
- Attrib.setup @{binding import_rew}
- (Scan.succeed (Thm.mixed_attribute add_importer_rewrite)) "external rewrite rule"
-
-end
+ add_importer_type_mapping "min" "bool" false @{type_name bool}
+ #> add_importer_type_mapping "min" "fun" false "fun"
+ #> add_importer_type_mapping "min" "ind" false @{type_name ind}
+ #> add_importer_const_mapping "min" "=" false @{const_name HOL.eq}
+ #> add_importer_const_mapping "min" "==>" false @{const_name HOL.implies}
+ #> add_importer_const_mapping "min" "@" false @{const_name "Eps"}
+ #> Attrib.setup @{binding import_rew}
+ (Scan.succeed (Thm.mixed_attribute add_importer_rewrite)) "external rewrite rule";
--- a/src/HOL/Import/import_syntax.ML Sun Mar 04 00:17:13 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML Sun Mar 04 00:26:23 2012 +0100
@@ -9,223 +9,4 @@
structure Importer_Import_Syntax : IMPORTER_IMPORT_SYNTAX =
struct
-(* Parsers *)
-
-val import_segment = Parse.name >> set_import_segment
-
-
-val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) =>
- fn thy =>
- thy |> set_generating_thy thyname
- |> Sign.add_path thyname
- |> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname))
-
-fun end_import toks =
- Scan.succeed
- (fn thy =>
- let
- val thyname = get_generating_thy thy
- val segname = get_import_segment thy
- val (int_thms,facts) = Replay.setup_int_thms thyname thy
- val thmnames = filter_out (should_ignore thyname thy) facts
- fun replay thy = Replay.import_thms thyname int_thms thmnames thy
- in
- thy |> clear_import_thy
- |> set_segment thyname segname
- |> set_used_names facts
- |> replay
- |> clear_used_names
- |> export_importer_pending
- |> Sign.parent_path
- |> dump_import_thy thyname
- |> add_dump ";end_setup"
- end) toks
-
-val ignore_thms = Scan.repeat1 Parse.name
- >> (fn ignored =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,thmname) => ignore_importer thyname thmname thy) (thy,ignored)
- end)
-
-val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
- >> (fn thmmaps =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,(hol,isa)) => add_importer_mapping thyname hol isa thy) (thy,thmmaps)
- end)
-
-val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
- >> (fn typmaps =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,(hol,isa)) => add_importer_type_mapping thyname hol false isa thy) (thy,typmaps)
- end)
-
-val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
- >> (fn defmaps =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
- end)
-
-val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
- >> (fn renames =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,(hol,isa)) => add_importer_const_renaming thyname hol isa thy) (thy,renames)
- end)
-
-val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
- >> (fn constmaps =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol false isa thy
- | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
- end)
-
-val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
- >> (fn constmaps =>
- fn thy =>
- let
- val thyname = get_import_thy thy
- in
- Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol true isa thy
- | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
- end)
-
-fun import_thy location s =
- let
- val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp"))
- val is = TextIO.openIn (File.platform_path src_location)
- val inp = TextIO.inputAll is
- val _ = TextIO.closeIn is
- val orig_source = Source.of_string inp
- val symb_source = Symbol.source orig_source
- val lexes =
- (Scan.make_lexicon
- (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
- Scan.empty_lexicon)
- val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
- val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
- val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
- val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
- val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
- val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
- val const_movesP = Parse.$$$ "const_moves" |-- const_moves
- val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
- val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
- val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
- val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
- val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
- fun apply [] thy = thy
- | apply (f::fs) thy = apply fs (f thy)
- in
- apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list))
- end
-
-fun create_int_thms thyname thy =
- if ! quick_and_dirty
- then thy
- else
- case ImportData.get thy of
- NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
- | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
-
-fun clear_int_thms thy =
- if ! quick_and_dirty
- then thy
- else
- case ImportData.get thy of
- NONE => error "Import data already cleared - forgotten a setup_theory?"
- | SOME _ => ImportData.put NONE thy
-
-val setup_theory = (Parse.name -- Parse.name)
- >>
- (fn (location, thyname) =>
- fn thy =>
- (case Importer_DefThy.get thy of
- NoImport => thy
- | Generating _ => error "Currently generating a theory!"
- | Replaying _ => thy |> clear_import_thy)
- |> import_thy location thyname
- |> create_int_thms thyname)
-
-fun end_setup toks =
- Scan.succeed
- (fn thy =>
- let
- val thyname = get_import_thy thy
- val segname = get_import_segment thy
- in
- thy |> set_segment thyname segname
- |> clear_import_thy
- |> clear_int_thms
- |> Sign.parent_path
- end) toks
-
-val set_dump = Parse.string -- Parse.string >> setup_dump
-fun fl_dump toks = Scan.succeed flush_dump toks
-val append_dump = (Parse.verbatim || Parse.string) >> add_dump
-
-val _ =
- (Keyword.keyword ">";
- Outer_Syntax.command "import_segment"
- "Set import segment name"
- Keyword.thy_decl (import_segment >> Toplevel.theory);
- Outer_Syntax.command "import_theory"
- "Set default external theory name"
- Keyword.thy_decl (import_theory >> Toplevel.theory);
- Outer_Syntax.command "end_import"
- "End external import"
- Keyword.thy_decl (end_import >> Toplevel.theory);
- Outer_Syntax.command "setup_theory"
- "Setup external theory replaying"
- Keyword.thy_decl (setup_theory >> Toplevel.theory);
- Outer_Syntax.command "end_setup"
- "End external setup"
- Keyword.thy_decl (end_setup >> Toplevel.theory);
- Outer_Syntax.command "setup_dump"
- "Setup the dump file name"
- Keyword.thy_decl (set_dump >> Toplevel.theory);
- Outer_Syntax.command "append_dump"
- "Add text to dump file"
- Keyword.thy_decl (append_dump >> Toplevel.theory);
- Outer_Syntax.command "flush_dump"
- "Write the dump to file"
- Keyword.thy_decl (fl_dump >> Toplevel.theory);
- Outer_Syntax.command "ignore_thms"
- "Theorems to ignore in next external theory import"
- Keyword.thy_decl (ignore_thms >> Toplevel.theory);
- Outer_Syntax.command "type_maps"
- "Map external type names to existing Isabelle/HOL type names"
- Keyword.thy_decl (type_maps >> Toplevel.theory);
- Outer_Syntax.command "def_maps"
- "Map external constant names to their primitive definitions"
- Keyword.thy_decl (def_maps >> Toplevel.theory);
- Outer_Syntax.command "thm_maps"
- "Map external theorem names to existing Isabelle/HOL theorem names"
- Keyword.thy_decl (thm_maps >> Toplevel.theory);
- Outer_Syntax.command "const_renames"
- "Rename external const names"
- Keyword.thy_decl (const_renames >> Toplevel.theory);
- Outer_Syntax.command "const_moves"
- "Rename external const names to other external constants"
- Keyword.thy_decl (const_moves >> Toplevel.theory);
- Outer_Syntax.command "const_maps"
- "Map external const names to existing Isabelle/HOL const names"
- Keyword.thy_decl (const_maps >> Toplevel.theory));
-
end