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