--- a/src/HOL/Import/import_syntax.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Mon May 17 23:54:15 2010 +0200
@@ -28,25 +28,23 @@
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
struct
-local structure P = OuterParse and K = OuterKeyword in
-
(* Parsers *)
-val import_segment = P.name >> set_import_segment
+val import_segment = Parse.name >> set_import_segment
-val import_theory = P.name >> (fn thyname =>
+val import_theory = Parse.name >> (fn thyname =>
fn thy =>
thy |> set_generating_thy thyname
|> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
-val skip_import_dir = P.string >> do_skip_import_dir
+val skip_import_dir = Parse.string >> do_skip_import_dir
val lower = String.map Char.toLower
fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
-val skip_import = P.short_ident >> do_skip_import
+val skip_import = Parse.short_ident >> do_skip_import
fun end_import toks =
Scan.succeed
@@ -78,7 +76,7 @@
|> add_dump ";end_setup"
end) toks
-val ignore_thms = Scan.repeat1 P.name
+val ignore_thms = Scan.repeat1 Parse.name
>> (fn ignored =>
fn thy =>
let
@@ -87,7 +85,7 @@
Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
end)
-val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn thmmaps =>
fn thy =>
let
@@ -96,7 +94,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
end)
-val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn typmaps =>
fn thy =>
let
@@ -105,7 +103,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
end)
-val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn defmaps =>
fn thy =>
let
@@ -114,7 +112,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
end)
-val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
+val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
>> (fn renames =>
fn thy =>
let
@@ -123,7 +121,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
end)
-val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -133,7 +131,7 @@
| (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
-val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -156,16 +154,16 @@
val get_lexes = fn () => !lexes
val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
- val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
- val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
- val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
- val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
- val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
- val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
- val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
- val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
+ 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 = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
+ val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
fun apply [] thy = thy
| apply (f::fs) thy = apply fs (f thy)
in
@@ -188,7 +186,7 @@
NONE => error "Import data already cleared - forgotten a setup_theory?"
| SOME _ => ImportData.put NONE thy
-val setup_theory = P.name
+val setup_theory = Parse.name
>>
(fn thyname =>
fn thy =>
@@ -212,64 +210,62 @@
|> Sign.parent_path
end) toks
-val set_dump = P.string -- P.string >> setup_dump
+val set_dump = Parse.string -- Parse.string >> setup_dump
fun fl_dump toks = Scan.succeed flush_dump toks
-val append_dump = (P.verbatim || P.string) >> add_dump
+val append_dump = (Parse.verbatim || Parse.string) >> add_dump
fun setup () =
- (OuterKeyword.keyword ">";
- OuterSyntax.command "import_segment"
+ (Keyword.keyword ">";
+ Outer_Syntax.command "import_segment"
"Set import segment name"
- K.thy_decl (import_segment >> Toplevel.theory);
- OuterSyntax.command "import_theory"
+ Keyword.thy_decl (import_segment >> Toplevel.theory);
+ Outer_Syntax.command "import_theory"
"Set default HOL4 theory name"
- K.thy_decl (import_theory >> Toplevel.theory);
- OuterSyntax.command "end_import"
+ Keyword.thy_decl (import_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_import"
"End HOL4 import"
- K.thy_decl (end_import >> Toplevel.theory);
- OuterSyntax.command "skip_import_dir"
+ Keyword.thy_decl (end_import >> Toplevel.theory);
+ Outer_Syntax.command "skip_import_dir"
"Sets caching directory for skipping importing"
- K.thy_decl (skip_import_dir >> Toplevel.theory);
- OuterSyntax.command "skip_import"
+ Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
+ Outer_Syntax.command "skip_import"
"Switches skipping importing on or off"
- K.thy_decl (skip_import >> Toplevel.theory);
- OuterSyntax.command "setup_theory"
+ Keyword.thy_decl (skip_import >> Toplevel.theory);
+ Outer_Syntax.command "setup_theory"
"Setup HOL4 theory replaying"
- K.thy_decl (setup_theory >> Toplevel.theory);
- OuterSyntax.command "end_setup"
+ Keyword.thy_decl (setup_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_setup"
"End HOL4 setup"
- K.thy_decl (end_setup >> Toplevel.theory);
- OuterSyntax.command "setup_dump"
+ Keyword.thy_decl (end_setup >> Toplevel.theory);
+ Outer_Syntax.command "setup_dump"
"Setup the dump file name"
- K.thy_decl (set_dump >> Toplevel.theory);
- OuterSyntax.command "append_dump"
+ Keyword.thy_decl (set_dump >> Toplevel.theory);
+ Outer_Syntax.command "append_dump"
"Add text to dump file"
- K.thy_decl (append_dump >> Toplevel.theory);
- OuterSyntax.command "flush_dump"
+ Keyword.thy_decl (append_dump >> Toplevel.theory);
+ Outer_Syntax.command "flush_dump"
"Write the dump to file"
- K.thy_decl (fl_dump >> Toplevel.theory);
- OuterSyntax.command "ignore_thms"
+ Keyword.thy_decl (fl_dump >> Toplevel.theory);
+ Outer_Syntax.command "ignore_thms"
"Theorems to ignore in next HOL4 theory import"
- K.thy_decl (ignore_thms >> Toplevel.theory);
- OuterSyntax.command "type_maps"
+ Keyword.thy_decl (ignore_thms >> Toplevel.theory);
+ Outer_Syntax.command "type_maps"
"Map HOL4 type names to existing Isabelle/HOL type names"
- K.thy_decl (type_maps >> Toplevel.theory);
- OuterSyntax.command "def_maps"
+ Keyword.thy_decl (type_maps >> Toplevel.theory);
+ Outer_Syntax.command "def_maps"
"Map HOL4 constant names to their primitive definitions"
- K.thy_decl (def_maps >> Toplevel.theory);
- OuterSyntax.command "thm_maps"
+ Keyword.thy_decl (def_maps >> Toplevel.theory);
+ Outer_Syntax.command "thm_maps"
"Map HOL4 theorem names to existing Isabelle/HOL theorem names"
- K.thy_decl (thm_maps >> Toplevel.theory);
- OuterSyntax.command "const_renames"
+ Keyword.thy_decl (thm_maps >> Toplevel.theory);
+ Outer_Syntax.command "const_renames"
"Rename HOL4 const names"
- K.thy_decl (const_renames >> Toplevel.theory);
- OuterSyntax.command "const_moves"
+ Keyword.thy_decl (const_renames >> Toplevel.theory);
+ Outer_Syntax.command "const_moves"
"Rename HOL4 const names to other HOL4 constants"
- K.thy_decl (const_moves >> Toplevel.theory);
- OuterSyntax.command "const_maps"
+ Keyword.thy_decl (const_moves >> Toplevel.theory);
+ Outer_Syntax.command "const_maps"
"Map HOL4 const names to existing Isabelle/HOL const names"
- K.thy_decl (const_maps >> Toplevel.theory));
+ Keyword.thy_decl (const_maps >> Toplevel.theory));
end
-
-end