src/HOL/Import/import_syntax.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 24867 e5b55d7be9bb
child 27775 a9d16f8b997a
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     1 (*  Title:      HOL/Import/import_syntax.ML
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 signature HOL4_IMPORT_SYNTAX =
     7 sig
     8     type token = OuterLex.token
     9     type command  = token list -> (theory -> theory) * token list 
    10 
    11     val import_segment: token list -> (theory -> theory) * token list
    12     val import_theory : token list -> (theory -> theory) * token list
    13     val end_import    : token list -> (theory -> theory) * token list
    14 
    15     val setup_theory  : token list -> (theory -> theory) * token list
    16     val end_setup     : token list -> (theory -> theory) * token list
    17 
    18     val thm_maps      : token list -> (theory -> theory) * token list
    19     val ignore_thms   : token list -> (theory -> theory) * token list
    20     val type_maps     : token list -> (theory -> theory) * token list
    21     val def_maps      : token list -> (theory -> theory) * token list
    22     val const_maps    : token list -> (theory -> theory) * token list
    23     val const_moves   : token list -> (theory -> theory) * token list
    24     val const_renames : token list -> (theory -> theory) * token list
    25 
    26     val skip_import_dir : token list -> (theory -> theory) * token list
    27     val skip_import     : token list -> (theory -> theory) * token list
    28 
    29     val setup        : unit -> unit
    30 end
    31 
    32 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
    33 struct
    34 
    35 type token = OuterLex.token
    36 type command  = token list -> (theory -> theory) * token list 
    37 
    38 local structure P = OuterParse and K = OuterKeyword in
    39 
    40 (* Parsers *)
    41 
    42 val import_segment = P.name >> set_import_segment
    43 
    44 
    45 val import_theory = P.name >> (fn thyname =>
    46 			       fn thy =>
    47 				  thy |> set_generating_thy thyname
    48 				      |> Sign.add_path thyname
    49 				      |> add_dump (";setup_theory " ^ thyname))
    50 
    51 fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
    52 val skip_import_dir : command = P.string >> do_skip_import_dir
    53 
    54 val lower = String.map Char.toLower
    55 fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
    56 val skip_import : command = P.short_ident >> do_skip_import
    57 
    58 fun end_import toks =
    59     Scan.succeed
    60 	(fn thy =>
    61 	    let
    62 		val thyname = get_generating_thy thy
    63 		val segname = get_import_segment thy
    64 		val (int_thms,facts) = Replay.setup_int_thms thyname thy
    65 		val thmnames = List.filter (not o should_ignore thyname thy) facts
    66 		fun replay thy = 
    67 		    let
    68 			val _ = ImportRecorder.load_history thyname
    69 			val thy = Replay.import_thms thyname int_thms thmnames thy
    70 			    handle x => (ImportRecorder.save_history thyname; raise x)
    71 			val _ = ImportRecorder.save_history thyname
    72 			val _ = ImportRecorder.clear_history ()
    73 		    in
    74 			thy
    75 		    end					
    76 	    in
    77 		thy |> clear_import_thy
    78 		    |> set_segment thyname segname
    79 		    |> set_used_names facts
    80 		    |> replay 
    81 		    |> clear_used_names
    82 		    |> export_hol4_pending
    83 		    |> Sign.parent_path
    84 		    |> dump_import_thy thyname
    85 		    |> add_dump ";end_setup"
    86 	    end) toks
    87 
    88 val ignore_thms = Scan.repeat1 P.name
    89 			       >> (fn ignored =>
    90 				   fn thy =>
    91 				      let
    92 					  val thyname = get_import_thy thy
    93 				      in
    94 					  Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
    95 				      end)
    96 
    97 val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    98 			    >> (fn thmmaps =>
    99 				fn thy =>
   100 				   let
   101 				       val thyname = get_import_thy thy
   102 				   in
   103 				       Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
   104 				   end)
   105 
   106 val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
   107 			     >> (fn typmaps =>
   108 				 fn thy =>
   109 				    let
   110 					val thyname = get_import_thy thy
   111 				    in
   112 					Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
   113 				    end)
   114 
   115 val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
   116 			    >> (fn defmaps =>
   117 				fn thy =>
   118 				   let
   119 				       val thyname = get_import_thy thy
   120 				   in
   121 				       Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
   122 				   end)
   123 
   124 val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
   125 				 >> (fn renames =>
   126 				     fn thy =>
   127 					let
   128 					    val thyname = get_import_thy thy
   129 					in
   130 					    Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
   131 					end)
   132 																      
   133 val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
   134 			      >> (fn constmaps =>
   135 				  fn thy =>
   136 				     let
   137 					 val thyname = get_import_thy thy
   138 				     in
   139 					 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
   140 						 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
   141 				     end)
   142 
   143 val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
   144 			       >> (fn constmaps =>
   145 				   fn thy =>
   146 				      let
   147 					  val thyname = get_import_thy thy
   148 				      in
   149 					  Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
   150 						  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
   151 				      end)
   152 
   153 fun import_thy s =
   154     let
   155 	val is = TextIO.openIn(s ^ ".imp")
   156 	val inp = TextIO.inputAll is
   157 	val _ = TextIO.closeIn is
   158 	val orig_source = Source.of_string inp
   159 	val symb_source = Symbol.source false orig_source
   160 	val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
   161 			 Scan.empty_lexicon)
   162 	val get_lexes = fn () => !lexes
   163 	val token_source = OuterLex.source NONE get_lexes (Position.line 1) symb_source
   164 	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
   165 	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
   166 	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
   167 	val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
   168 	val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
   169 	val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
   170 	val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
   171 	val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
   172 	val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
   173 	val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
   174 	val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
   175 	fun apply [] thy = thy
   176 	  | apply (f::fs) thy = apply fs (f thy)
   177     in
   178 	apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
   179     end
   180 
   181 fun create_int_thms thyname thy =
   182     if ! quick_and_dirty
   183     then thy
   184     else
   185 	case ImportData.get thy of
   186 	    NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
   187 	  | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
   188 
   189 fun clear_int_thms thy =
   190     if ! quick_and_dirty
   191     then thy
   192     else
   193 	case ImportData.get thy of
   194 	    NONE => error "Import data already cleared - forgotten a setup_theory?"
   195 	  | SOME _ => ImportData.put NONE thy
   196 
   197 val setup_theory = P.name
   198 		       >>
   199 		       (fn thyname =>
   200 			fn thy =>
   201 			   (case HOL4DefThy.get thy of
   202 				NoImport => thy
   203 			      | Generating _ => error "Currently generating a theory!"
   204 			      | Replaying _ => thy |> clear_import_thy)
   205 			       |> import_thy thyname
   206 			       |> create_int_thms thyname)
   207 
   208 fun end_setup toks =
   209     Scan.succeed
   210 	(fn thy =>
   211 	    let
   212 		val thyname = get_import_thy thy
   213 		val segname = get_import_segment thy
   214 	    in
   215 		thy |> set_segment thyname segname
   216 		    |> clear_import_thy
   217 		    |> clear_int_thms
   218 		    |> Sign.parent_path
   219 	    end) toks
   220 
   221 val set_dump  = P.string -- P.string   >> setup_dump
   222 fun fl_dump toks  = Scan.succeed flush_dump toks
   223 val append_dump = (P.verbatim || P.string) >> add_dump
   224 
   225 fun setup () =
   226   (OuterKeyword.keyword ">";
   227    OuterSyntax.command "import_segment"
   228 		       "Set import segment name"
   229 		       K.thy_decl (import_segment >> Toplevel.theory);
   230    OuterSyntax.command "import_theory"
   231 		       "Set default HOL4 theory name"
   232 		       K.thy_decl (import_theory >> Toplevel.theory);
   233    OuterSyntax.command "end_import"
   234 		       "End HOL4 import"
   235 		       K.thy_decl (end_import >> Toplevel.theory);
   236    OuterSyntax.command "skip_import_dir" 
   237                        "Sets caching directory for skipping importing"
   238                        K.thy_decl (skip_import_dir >> Toplevel.theory);
   239    OuterSyntax.command "skip_import" 
   240                        "Switches skipping importing on or off"
   241                        K.thy_decl (skip_import >> Toplevel.theory);		      
   242    OuterSyntax.command "setup_theory"
   243 		       "Setup HOL4 theory replaying"
   244 		       K.thy_decl (setup_theory >> Toplevel.theory);
   245    OuterSyntax.command "end_setup"
   246 		       "End HOL4 setup"
   247 		       K.thy_decl (end_setup >> Toplevel.theory);
   248    OuterSyntax.command "setup_dump"
   249 		       "Setup the dump file name"
   250 		       K.thy_decl (set_dump >> Toplevel.theory);
   251    OuterSyntax.command "append_dump"
   252 		       "Add text to dump file"
   253 		       K.thy_decl (append_dump >> Toplevel.theory);
   254    OuterSyntax.command "flush_dump"
   255 		       "Write the dump to file"
   256 		       K.thy_decl (fl_dump >> Toplevel.theory);
   257    OuterSyntax.command "ignore_thms"
   258 		       "Theorems to ignore in next HOL4 theory import"
   259 		       K.thy_decl (ignore_thms >> Toplevel.theory);
   260    OuterSyntax.command "type_maps"
   261 		       "Map HOL4 type names to existing Isabelle/HOL type names"
   262 		       K.thy_decl (type_maps >> Toplevel.theory);
   263    OuterSyntax.command "def_maps"
   264 		       "Map HOL4 constant names to their primitive definitions"
   265 		       K.thy_decl (def_maps >> Toplevel.theory);
   266    OuterSyntax.command "thm_maps"
   267 		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
   268 		       K.thy_decl (thm_maps >> Toplevel.theory);
   269    OuterSyntax.command "const_renames"
   270 		       "Rename HOL4 const names"
   271 		       K.thy_decl (const_renames >> Toplevel.theory);
   272    OuterSyntax.command "const_moves"
   273 		       "Rename HOL4 const names to other HOL4 constants"
   274 		       K.thy_decl (const_moves >> Toplevel.theory);
   275    OuterSyntax.command "const_maps"
   276 		       "Map HOL4 const names to existing Isabelle/HOL const names"
   277 		       K.thy_decl (const_maps >> Toplevel.theory));
   278 
   279 end
   280 
   281 end