src/HOL/Import/import_syntax.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 27835 ff8b8513965a
child 32960 69916a850301
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     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 {do_recover = false} orig_source
   160 	val lexes = Unsynchronized.ref
   161 	  (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
   162 		  Scan.empty_lexicon)
   163 	val get_lexes = fn () => !lexes
   164 	val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
   165 	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
   166 	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
   167 	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
   168 	val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
   169 	val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
   170 	val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
   171 	val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
   172 	val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
   173 	val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
   174 	val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
   175 	val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
   176 	fun apply [] thy = thy
   177 	  | apply (f::fs) thy = apply fs (f thy)
   178     in
   179 	apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
   180     end
   181 
   182 fun create_int_thms thyname thy =
   183     if ! quick_and_dirty
   184     then thy
   185     else
   186 	case ImportData.get thy of
   187 	    NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
   188 	  | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
   189 
   190 fun clear_int_thms thy =
   191     if ! quick_and_dirty
   192     then thy
   193     else
   194 	case ImportData.get thy of
   195 	    NONE => error "Import data already cleared - forgotten a setup_theory?"
   196 	  | SOME _ => ImportData.put NONE thy
   197 
   198 val setup_theory = P.name
   199 		       >>
   200 		       (fn thyname =>
   201 			fn thy =>
   202 			   (case HOL4DefThy.get thy of
   203 				NoImport => thy
   204 			      | Generating _ => error "Currently generating a theory!"
   205 			      | Replaying _ => thy |> clear_import_thy)
   206 			       |> import_thy thyname
   207 			       |> create_int_thms thyname)
   208 
   209 fun end_setup toks =
   210     Scan.succeed
   211 	(fn thy =>
   212 	    let
   213 		val thyname = get_import_thy thy
   214 		val segname = get_import_segment thy
   215 	    in
   216 		thy |> set_segment thyname segname
   217 		    |> clear_import_thy
   218 		    |> clear_int_thms
   219 		    |> Sign.parent_path
   220 	    end) toks
   221 
   222 val set_dump  = P.string -- P.string   >> setup_dump
   223 fun fl_dump toks  = Scan.succeed flush_dump toks
   224 val append_dump = (P.verbatim || P.string) >> add_dump
   225 
   226 fun setup () =
   227   (OuterKeyword.keyword ">";
   228    OuterSyntax.command "import_segment"
   229 		       "Set import segment name"
   230 		       K.thy_decl (import_segment >> Toplevel.theory);
   231    OuterSyntax.command "import_theory"
   232 		       "Set default HOL4 theory name"
   233 		       K.thy_decl (import_theory >> Toplevel.theory);
   234    OuterSyntax.command "end_import"
   235 		       "End HOL4 import"
   236 		       K.thy_decl (end_import >> Toplevel.theory);
   237    OuterSyntax.command "skip_import_dir" 
   238                        "Sets caching directory for skipping importing"
   239                        K.thy_decl (skip_import_dir >> Toplevel.theory);
   240    OuterSyntax.command "skip_import" 
   241                        "Switches skipping importing on or off"
   242                        K.thy_decl (skip_import >> Toplevel.theory);		      
   243    OuterSyntax.command "setup_theory"
   244 		       "Setup HOL4 theory replaying"
   245 		       K.thy_decl (setup_theory >> Toplevel.theory);
   246    OuterSyntax.command "end_setup"
   247 		       "End HOL4 setup"
   248 		       K.thy_decl (end_setup >> Toplevel.theory);
   249    OuterSyntax.command "setup_dump"
   250 		       "Setup the dump file name"
   251 		       K.thy_decl (set_dump >> Toplevel.theory);
   252    OuterSyntax.command "append_dump"
   253 		       "Add text to dump file"
   254 		       K.thy_decl (append_dump >> Toplevel.theory);
   255    OuterSyntax.command "flush_dump"
   256 		       "Write the dump to file"
   257 		       K.thy_decl (fl_dump >> Toplevel.theory);
   258    OuterSyntax.command "ignore_thms"
   259 		       "Theorems to ignore in next HOL4 theory import"
   260 		       K.thy_decl (ignore_thms >> Toplevel.theory);
   261    OuterSyntax.command "type_maps"
   262 		       "Map HOL4 type names to existing Isabelle/HOL type names"
   263 		       K.thy_decl (type_maps >> Toplevel.theory);
   264    OuterSyntax.command "def_maps"
   265 		       "Map HOL4 constant names to their primitive definitions"
   266 		       K.thy_decl (def_maps >> Toplevel.theory);
   267    OuterSyntax.command "thm_maps"
   268 		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
   269 		       K.thy_decl (thm_maps >> Toplevel.theory);
   270    OuterSyntax.command "const_renames"
   271 		       "Rename HOL4 const names"
   272 		       K.thy_decl (const_renames >> Toplevel.theory);
   273    OuterSyntax.command "const_moves"
   274 		       "Rename HOL4 const names to other HOL4 constants"
   275 		       K.thy_decl (const_moves >> Toplevel.theory);
   276    OuterSyntax.command "const_maps"
   277 		       "Map HOL4 const names to existing Isabelle/HOL const names"
   278 		       K.thy_decl (const_maps >> Toplevel.theory));
   279 
   280 end
   281 
   282 end