skalberg@14620: (* Title: HOL/Import/import_syntax.ML skalberg@14620: Author: Sebastian Skalberg (TU Muenchen) skalberg@14620: *) skalberg@14620: skalberg@14516: signature HOL4_IMPORT_SYNTAX = skalberg@14516: sig wenzelm@36959: val import_segment: (theory -> theory) parser wenzelm@36959: val import_theory : (theory -> theory) parser wenzelm@36959: val end_import : (theory -> theory) parser wenzelm@36959: wenzelm@36959: val setup_theory : (theory -> theory) parser wenzelm@36959: val end_setup : (theory -> theory) parser wenzelm@36959: wenzelm@36959: val thm_maps : (theory -> theory) parser wenzelm@36959: val ignore_thms : (theory -> theory) parser wenzelm@36959: val type_maps : (theory -> theory) parser wenzelm@36959: val def_maps : (theory -> theory) parser wenzelm@36959: val const_maps : (theory -> theory) parser wenzelm@36959: val const_moves : (theory -> theory) parser wenzelm@36959: val const_renames : (theory -> theory) parser skalberg@14516: wenzelm@36959: val skip_import_dir : (theory -> theory) parser wenzelm@36959: val skip_import : (theory -> theory) parser obua@19064: skalberg@14516: val setup : unit -> unit skalberg@14516: end skalberg@14516: skalberg@14516: structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX = skalberg@14516: struct skalberg@14516: skalberg@14516: (* Parsers *) skalberg@14516: wenzelm@36960: val import_segment = Parse.name >> set_import_segment skalberg@14516: obua@19064: wenzelm@36960: val import_theory = Parse.name >> (fn thyname => wenzelm@32960: fn thy => wenzelm@32960: thy |> set_generating_thy thyname wenzelm@32960: |> Sign.add_path thyname wenzelm@32960: |> add_dump (";setup_theory " ^ thyname)) skalberg@14516: obua@19064: fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I) wenzelm@36960: val skip_import_dir = Parse.string >> do_skip_import_dir obua@19064: obua@19064: val lower = String.map Char.toLower obua@19064: fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I) wenzelm@36960: val skip_import = Parse.short_ident >> do_skip_import obua@19064: skalberg@14518: fun end_import toks = skalberg@14518: Scan.succeed wenzelm@32960: (fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_generating_thy thy wenzelm@32960: val segname = get_import_segment thy wenzelm@32960: val (int_thms,facts) = Replay.setup_int_thms thyname thy wenzelm@33317: val thmnames = filter_out (should_ignore thyname thy) facts wenzelm@32960: fun replay thy = wenzelm@32960: let wenzelm@32960: val _ = ImportRecorder.load_history thyname wenzelm@32960: val thy = Replay.import_thms thyname int_thms thmnames thy wenzelm@32960: handle x => (ImportRecorder.save_history thyname; raise x) wenzelm@32960: val _ = ImportRecorder.save_history thyname wenzelm@32960: val _ = ImportRecorder.clear_history () wenzelm@32960: in wenzelm@32960: thy wenzelm@32960: end wenzelm@32960: in wenzelm@32960: thy |> clear_import_thy wenzelm@32960: |> set_segment thyname segname wenzelm@32960: |> set_used_names facts wenzelm@32960: |> replay wenzelm@32960: |> clear_used_names wenzelm@32960: |> export_hol4_pending wenzelm@32960: |> Sign.parent_path wenzelm@32960: |> dump_import_thy thyname wenzelm@32960: |> add_dump ";end_setup" wenzelm@32960: end) toks skalberg@14516: wenzelm@36960: val ignore_thms = Scan.repeat1 Parse.name wenzelm@32960: >> (fn ignored => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored) wenzelm@32960: end) skalberg@14516: wenzelm@36960: val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) wenzelm@32960: >> (fn thmmaps => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps) wenzelm@32960: end) skalberg@14516: wenzelm@36960: val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) wenzelm@32960: >> (fn typmaps => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps) wenzelm@32960: end) skalberg@14516: wenzelm@36960: val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) wenzelm@32960: >> (fn defmaps => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps) wenzelm@32960: end) skalberg@14516: wenzelm@36960: val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name) wenzelm@32960: >> (fn renames => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames) wenzelm@32960: end) wenzelm@32960: wenzelm@36960: val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ)) wenzelm@32960: >> (fn constmaps => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy wenzelm@32960: | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps) wenzelm@32960: end) skalberg@14516: wenzelm@36960: val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ)) wenzelm@32960: >> (fn constmaps => wenzelm@32960: fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: in wenzelm@32960: Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy wenzelm@32960: | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps) wenzelm@32960: end) skalberg@14516: skalberg@14516: fun import_thy s = skalberg@14516: let wenzelm@32960: val is = TextIO.openIn(s ^ ".imp") wenzelm@32960: val inp = TextIO.inputAll is wenzelm@32960: val _ = TextIO.closeIn is wenzelm@32960: val orig_source = Source.of_string inp wenzelm@32960: val symb_source = Symbol.source {do_recover = false} orig_source wenzelm@32960: val lexes = Unsynchronized.ref wenzelm@32960: (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]), wenzelm@32960: Scan.empty_lexicon) wenzelm@32960: val get_lexes = fn () => !lexes wenzelm@36959: val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source wenzelm@36959: val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source) wenzelm@36960: val import_segmentP = Parse.$$$ "import_segment" |-- import_segment wenzelm@36960: val type_mapsP = Parse.$$$ "type_maps" |-- type_maps wenzelm@36960: val def_mapsP = Parse.$$$ "def_maps" |-- def_maps wenzelm@36960: val const_mapsP = Parse.$$$ "const_maps" |-- const_maps wenzelm@36960: val const_movesP = Parse.$$$ "const_moves" |-- const_moves wenzelm@36960: val const_renamesP = Parse.$$$ "const_renames" |-- const_renames wenzelm@36960: val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms wenzelm@36960: val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps wenzelm@32960: val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP wenzelm@36960: val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end" wenzelm@32960: fun apply [] thy = thy wenzelm@32960: | apply (f::fs) thy = apply fs (f thy) skalberg@14516: in wenzelm@32960: apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list))) skalberg@14516: end skalberg@14516: skalberg@14620: fun create_int_thms thyname thy = wenzelm@17370: if ! quick_and_dirty skalberg@14627: then thy skalberg@14627: else wenzelm@32960: case ImportData.get thy of wenzelm@32960: NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy wenzelm@32960: | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?" skalberg@14620: skalberg@14620: fun clear_int_thms thy = wenzelm@17370: if ! quick_and_dirty skalberg@14627: then thy skalberg@14627: else wenzelm@32960: case ImportData.get thy of wenzelm@32960: NONE => error "Import data already cleared - forgotten a setup_theory?" wenzelm@32960: | SOME _ => ImportData.put NONE thy skalberg@14620: wenzelm@36960: val setup_theory = Parse.name wenzelm@32960: >> wenzelm@32960: (fn thyname => wenzelm@32960: fn thy => wenzelm@32960: (case HOL4DefThy.get thy of wenzelm@32960: NoImport => thy wenzelm@32960: | Generating _ => error "Currently generating a theory!" wenzelm@32960: | Replaying _ => thy |> clear_import_thy) wenzelm@32960: |> import_thy thyname wenzelm@32960: |> create_int_thms thyname) skalberg@14516: skalberg@14518: fun end_setup toks = skalberg@14518: Scan.succeed wenzelm@32960: (fn thy => wenzelm@32960: let wenzelm@32960: val thyname = get_import_thy thy wenzelm@32960: val segname = get_import_segment thy wenzelm@32960: in wenzelm@32960: thy |> set_segment thyname segname wenzelm@32960: |> clear_import_thy wenzelm@32960: |> clear_int_thms wenzelm@32960: |> Sign.parent_path wenzelm@32960: end) toks skalberg@14516: wenzelm@36960: val set_dump = Parse.string -- Parse.string >> setup_dump skalberg@14518: fun fl_dump toks = Scan.succeed flush_dump toks wenzelm@36960: val append_dump = (Parse.verbatim || Parse.string) >> add_dump skalberg@14516: wenzelm@24867: fun setup () = wenzelm@36960: (Keyword.keyword ">"; wenzelm@36960: Outer_Syntax.command "import_segment" wenzelm@32960: "Set import segment name" wenzelm@36960: Keyword.thy_decl (import_segment >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "import_theory" wenzelm@32960: "Set default HOL4 theory name" wenzelm@36960: Keyword.thy_decl (import_theory >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "end_import" wenzelm@32960: "End HOL4 import" wenzelm@36960: Keyword.thy_decl (end_import >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "skip_import_dir" obua@19064: "Sets caching directory for skipping importing" wenzelm@36960: Keyword.thy_decl (skip_import_dir >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "skip_import" obua@19064: "Switches skipping importing on or off" wenzelm@36960: Keyword.thy_decl (skip_import >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "setup_theory" wenzelm@32960: "Setup HOL4 theory replaying" wenzelm@36960: Keyword.thy_decl (setup_theory >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "end_setup" wenzelm@32960: "End HOL4 setup" wenzelm@36960: Keyword.thy_decl (end_setup >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "setup_dump" wenzelm@32960: "Setup the dump file name" wenzelm@36960: Keyword.thy_decl (set_dump >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "append_dump" wenzelm@32960: "Add text to dump file" wenzelm@36960: Keyword.thy_decl (append_dump >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "flush_dump" wenzelm@32960: "Write the dump to file" wenzelm@36960: Keyword.thy_decl (fl_dump >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "ignore_thms" wenzelm@32960: "Theorems to ignore in next HOL4 theory import" wenzelm@36960: Keyword.thy_decl (ignore_thms >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "type_maps" wenzelm@32960: "Map HOL4 type names to existing Isabelle/HOL type names" wenzelm@36960: Keyword.thy_decl (type_maps >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "def_maps" wenzelm@32960: "Map HOL4 constant names to their primitive definitions" wenzelm@36960: Keyword.thy_decl (def_maps >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "thm_maps" wenzelm@32960: "Map HOL4 theorem names to existing Isabelle/HOL theorem names" wenzelm@36960: Keyword.thy_decl (thm_maps >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "const_renames" wenzelm@32960: "Rename HOL4 const names" wenzelm@36960: Keyword.thy_decl (const_renames >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "const_moves" wenzelm@32960: "Rename HOL4 const names to other HOL4 constants" wenzelm@36960: Keyword.thy_decl (const_moves >> Toplevel.theory); wenzelm@36960: Outer_Syntax.command "const_maps" wenzelm@32960: "Map HOL4 const names to existing Isabelle/HOL const names" wenzelm@36960: Keyword.thy_decl (const_maps >> Toplevel.theory)); skalberg@14516: skalberg@14516: end