--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/import_syntax.ML Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,227 @@
+signature HOL4_IMPORT_SYNTAX =
+sig
+ type token = OuterSyntax.token
+
+ val import_segment: token list -> (theory -> theory) * token list
+ val import_theory : token list -> (theory -> theory) * token list
+ val end_import : token list -> (theory -> theory) * token list
+
+ val setup_theory : token list -> (theory -> theory) * token list
+ val end_setup : token list -> (theory -> theory) * token list
+
+ val thm_maps : token list -> (theory -> theory) * token list
+ val ignore_thms : token list -> (theory -> theory) * token list
+ val type_maps : token list -> (theory -> theory) * token list
+ val def_maps : token list -> (theory -> theory) * token list
+ val const_maps : token list -> (theory -> theory) * token list
+ val const_moves : token list -> (theory -> theory) * token list
+ val const_renames : token list -> (theory -> theory) * token list
+
+ val setup : unit -> unit
+end
+
+structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
+struct
+
+type token = OuterSyntax.token
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+(* Parsers *)
+
+val import_segment = P.name >> set_import_segment
+
+val import_theory = P.name >> (fn thyname =>
+ fn thy =>
+ thy |> set_generating_thy thyname
+ |> Theory.add_path thyname
+ |> add_dump (";setup_theory " ^ thyname))
+
+val end_import = 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 (not o should_ignore thyname thy) facts
+ in
+ thy |> clear_import_thy
+ |> set_segment thyname segname
+ |> set_used_names facts
+ |> Replay.import_thms thyname int_thms thmnames
+ |> clear_used_names
+ |> export_hol4_pending
+ |> Theory.parent_path
+ |> dump_import_thy thyname
+ |> add_dump ";end_setup"
+ end)
+
+val ignore_thms = Scan.repeat1 P.name
+ >> (fn ignored =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
+ end)
+
+val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+ >> (fn thmmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ 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)
+ >> (fn typmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ 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)
+ >> (fn defmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
+ end)
+
+val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
+ >> (fn renames =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ 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))
+ >> (fn constmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy
+ | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
+ end)
+
+val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+ >> (fn constmaps =>
+ fn thy =>
+ let
+ val thyname = get_import_thy thy
+ in
+ foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy
+ | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
+ end)
+
+fun import_thy s =
+ let
+ val is = TextIO.openIn(s ^ ".imp")
+ val inp = TextIO.inputAll is
+ val _ = TextIO.closeIn is
+ val orig_source = Source.of_string inp
+ val symb_source = Symbol.source false orig_source
+ val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
+ Scan.empty_lexicon)
+ val get_lexes = fn () => !lexes
+ val token_source = OuterLex.source false get_lexes (Position.line 1) symb_source
+ val token_list = filter (not o (OuterLex.is_kind OuterLex.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 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"
+ fun apply [] thy = thy
+ | apply (f::fs) thy = apply fs (f thy)
+ in
+ apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
+ end
+
+val setup_theory = P.name
+ >>
+ (fn thyname =>
+ fn thy =>
+ case HOL4DefThy.get thy of
+ NoImport => thy |> import_thy thyname
+ | Generating _ => error "Currently generating a theory!"
+ | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
+
+val end_setup = 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
+ |> Theory.parent_path
+ end)
+
+val set_dump = P.string -- P.string >> setup_dump
+val fl_dump = Scan.succeed flush_dump
+val append_dump = (P.verbatim || P.string) >> add_dump
+
+val parsers =
+ [OuterSyntax.command "import_segment"
+ "Set import segment name"
+ K.thy_decl (import_segment >> Toplevel.theory),
+ OuterSyntax.command "import_theory"
+ "Set default HOL4 theory name"
+ K.thy_decl (import_theory >> Toplevel.theory),
+ OuterSyntax.command "end_import"
+ "End HOL4 import"
+ K.thy_decl (end_import >> Toplevel.theory),
+ OuterSyntax.command "setup_theory"
+ "Setup HOL4 theory replaying"
+ K.thy_decl (setup_theory >> Toplevel.theory),
+ OuterSyntax.command "end_setup"
+ "End HOL4 setup"
+ K.thy_decl (end_setup >> Toplevel.theory),
+ OuterSyntax.command "setup_dump"
+ "Setup the dump file name"
+ K.thy_decl (set_dump >> Toplevel.theory),
+ OuterSyntax.command "append_dump"
+ "Add text to dump file"
+ K.thy_decl (append_dump >> Toplevel.theory),
+ OuterSyntax.command "flush_dump"
+ "Write the dump to file"
+ K.thy_decl (fl_dump >> Toplevel.theory),
+ OuterSyntax.command "ignore_thms"
+ "Theorems to ignore in next HOL4 theory import"
+ K.thy_decl (ignore_thms >> Toplevel.theory),
+ OuterSyntax.command "type_maps"
+ "Map HOL4 type names to existing Isabelle/HOL type names"
+ K.thy_decl (type_maps >> Toplevel.theory),
+ OuterSyntax.command "def_maps"
+ "Map HOL4 constant names to their primitive definitions"
+ K.thy_decl (def_maps >> Toplevel.theory),
+ OuterSyntax.command "thm_maps"
+ "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
+ K.thy_decl (thm_maps >> Toplevel.theory),
+ OuterSyntax.command "const_renames"
+ "Rename HOL4 const names"
+ K.thy_decl (const_renames >> Toplevel.theory),
+ OuterSyntax.command "const_moves"
+ "Rename HOL4 const names to other HOL4 constants"
+ K.thy_decl (const_moves >> Toplevel.theory),
+ OuterSyntax.command "const_maps"
+ "Map HOL4 const names to existing Isabelle/HOL const names"
+ K.thy_decl (const_maps >> Toplevel.theory)]
+
+fun setup () = (OuterSyntax.add_keywords[">"];
+ OuterSyntax.add_parsers parsers)
+
+end
+
+end