src/HOL/Import/import_syntax.ML
author skalberg
Sun Apr 04 15:34:14 2004 +0200 (2004-04-04)
changeset 14518 c3019a66180f
parent 14516 a183dec876ab
child 14620 1be590fd2422
permissions -rw-r--r--
Added a number of explicit type casts and delayed evaluations (all seemingly
needless) so that SML/NJ 110.9.1 would accept the importer...
skalberg@14516
     1
signature HOL4_IMPORT_SYNTAX =
skalberg@14516
     2
sig
skalberg@14516
     3
    type token = OuterSyntax.token
skalberg@14516
     4
skalberg@14516
     5
    val import_segment: token list -> (theory -> theory) * token list
skalberg@14516
     6
    val import_theory : token list -> (theory -> theory) * token list
skalberg@14516
     7
    val end_import    : token list -> (theory -> theory) * token list
skalberg@14516
     8
skalberg@14516
     9
    val setup_theory  : token list -> (theory -> theory) * token list
skalberg@14516
    10
    val end_setup     : token list -> (theory -> theory) * token list
skalberg@14516
    11
skalberg@14516
    12
    val thm_maps      : token list -> (theory -> theory) * token list
skalberg@14516
    13
    val ignore_thms   : token list -> (theory -> theory) * token list
skalberg@14516
    14
    val type_maps     : token list -> (theory -> theory) * token list
skalberg@14516
    15
    val def_maps      : token list -> (theory -> theory) * token list
skalberg@14516
    16
    val const_maps    : token list -> (theory -> theory) * token list
skalberg@14516
    17
    val const_moves   : token list -> (theory -> theory) * token list
skalberg@14516
    18
    val const_renames : token list -> (theory -> theory) * token list
skalberg@14516
    19
skalberg@14516
    20
    val setup        : unit -> unit
skalberg@14516
    21
end
skalberg@14516
    22
skalberg@14516
    23
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
skalberg@14516
    24
struct
skalberg@14516
    25
skalberg@14516
    26
type token = OuterSyntax.token
skalberg@14516
    27
skalberg@14516
    28
local structure P = OuterParse and K = OuterSyntax.Keyword in
skalberg@14516
    29
skalberg@14516
    30
(* Parsers *)
skalberg@14516
    31
skalberg@14516
    32
val import_segment = P.name >> set_import_segment
skalberg@14516
    33
skalberg@14516
    34
val import_theory = P.name >> (fn thyname =>
skalberg@14516
    35
			       fn thy =>
skalberg@14516
    36
				  thy |> set_generating_thy thyname
skalberg@14516
    37
				      |> Theory.add_path thyname
skalberg@14516
    38
				      |> add_dump (";setup_theory " ^ thyname))
skalberg@14516
    39
skalberg@14518
    40
fun end_import toks =
skalberg@14518
    41
    Scan.succeed
skalberg@14518
    42
	(fn thy =>
skalberg@14518
    43
	    let
skalberg@14518
    44
		val thyname = get_generating_thy thy
skalberg@14518
    45
		val segname = get_import_segment thy
skalberg@14518
    46
		val (int_thms,facts) = Replay.setup_int_thms thyname thy
skalberg@14518
    47
		val thmnames = filter (not o should_ignore thyname thy) facts
skalberg@14518
    48
	    in
skalberg@14518
    49
		thy |> clear_import_thy
skalberg@14518
    50
		    |> set_segment thyname segname
skalberg@14518
    51
		    |> set_used_names facts
skalberg@14518
    52
		    |> Replay.import_thms thyname int_thms thmnames
skalberg@14518
    53
		    |> clear_used_names
skalberg@14518
    54
		    |> export_hol4_pending
skalberg@14518
    55
		    |> Theory.parent_path
skalberg@14518
    56
		    |> dump_import_thy thyname
skalberg@14518
    57
		    |> add_dump ";end_setup"
skalberg@14518
    58
	    end) toks
skalberg@14516
    59
skalberg@14516
    60
val ignore_thms = Scan.repeat1 P.name
skalberg@14516
    61
			       >> (fn ignored =>
skalberg@14516
    62
				   fn thy =>
skalberg@14516
    63
				      let
skalberg@14516
    64
					  val thyname = get_import_thy thy
skalberg@14516
    65
				      in
skalberg@14516
    66
					  foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
skalberg@14516
    67
				      end)
skalberg@14516
    68
skalberg@14516
    69
val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
skalberg@14516
    70
			    >> (fn thmmaps =>
skalberg@14516
    71
				fn thy =>
skalberg@14516
    72
				   let
skalberg@14516
    73
				       val thyname = get_import_thy thy
skalberg@14516
    74
				   in
skalberg@14516
    75
				       foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
skalberg@14516
    76
				   end)
skalberg@14516
    77
skalberg@14516
    78
val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
skalberg@14516
    79
			     >> (fn typmaps =>
skalberg@14516
    80
				 fn thy =>
skalberg@14516
    81
				    let
skalberg@14516
    82
					val thyname = get_import_thy thy
skalberg@14516
    83
				    in
skalberg@14516
    84
					foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
skalberg@14516
    85
				    end)
skalberg@14516
    86
skalberg@14516
    87
val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
skalberg@14516
    88
			    >> (fn defmaps =>
skalberg@14516
    89
				fn thy =>
skalberg@14516
    90
				   let
skalberg@14516
    91
				       val thyname = get_import_thy thy
skalberg@14516
    92
				   in
skalberg@14516
    93
				       foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
skalberg@14516
    94
				   end)
skalberg@14516
    95
skalberg@14516
    96
val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
skalberg@14516
    97
				 >> (fn renames =>
skalberg@14516
    98
				     fn thy =>
skalberg@14516
    99
					let
skalberg@14516
   100
					    val thyname = get_import_thy thy
skalberg@14516
   101
					in
skalberg@14516
   102
					    foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
skalberg@14516
   103
					end)
skalberg@14516
   104
																      
skalberg@14516
   105
val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
skalberg@14516
   106
			      >> (fn constmaps =>
skalberg@14516
   107
				  fn thy =>
skalberg@14516
   108
				     let
skalberg@14516
   109
					 val thyname = get_import_thy thy
skalberg@14516
   110
				     in
skalberg@14516
   111
					 foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy
skalberg@14516
   112
						 | (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)
skalberg@14516
   113
				     end)
skalberg@14516
   114
skalberg@14516
   115
val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
skalberg@14516
   116
			       >> (fn constmaps =>
skalberg@14516
   117
				   fn thy =>
skalberg@14516
   118
				      let
skalberg@14516
   119
					  val thyname = get_import_thy thy
skalberg@14516
   120
				      in
skalberg@14516
   121
					  foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy
skalberg@14516
   122
						  | (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)
skalberg@14516
   123
				      end)
skalberg@14516
   124
skalberg@14516
   125
fun import_thy s =
skalberg@14516
   126
    let
skalberg@14516
   127
	val is = TextIO.openIn(s ^ ".imp")
skalberg@14516
   128
	val inp = TextIO.inputAll is
skalberg@14516
   129
	val _ = TextIO.closeIn is
skalberg@14516
   130
	val orig_source = Source.of_string inp
skalberg@14516
   131
	val symb_source = Symbol.source false orig_source
skalberg@14516
   132
	val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
skalberg@14516
   133
			 Scan.empty_lexicon)
skalberg@14516
   134
	val get_lexes = fn () => !lexes
skalberg@14516
   135
	val token_source = OuterLex.source false get_lexes (Position.line 1) symb_source
skalberg@14516
   136
	val token_list = filter (not o (OuterLex.is_kind OuterLex.Space)) (Source.exhaust token_source)
skalberg@14516
   137
	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
skalberg@14516
   138
	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
skalberg@14516
   139
	val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
skalberg@14516
   140
	val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
skalberg@14516
   141
	val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
skalberg@14516
   142
	val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
skalberg@14516
   143
	val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
skalberg@14516
   144
	val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
skalberg@14516
   145
	val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
skalberg@14516
   146
	val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
skalberg@14516
   147
	fun apply [] thy = thy
skalberg@14516
   148
	  | apply (f::fs) thy = apply fs (f thy)
skalberg@14516
   149
    in
skalberg@14516
   150
	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
skalberg@14516
   151
    end
skalberg@14516
   152
skalberg@14516
   153
val setup_theory = P.name
skalberg@14516
   154
		       >>
skalberg@14516
   155
		       (fn thyname =>
skalberg@14516
   156
			fn thy =>
skalberg@14516
   157
			   case HOL4DefThy.get thy of
skalberg@14516
   158
			       NoImport => thy |> import_thy thyname
skalberg@14516
   159
			     | Generating _ => error "Currently generating a theory!"
skalberg@14516
   160
			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
skalberg@14516
   161
skalberg@14518
   162
fun end_setup toks =
skalberg@14518
   163
    Scan.succeed
skalberg@14518
   164
	(fn thy =>
skalberg@14518
   165
	    let
skalberg@14518
   166
		val thyname = get_import_thy thy
skalberg@14518
   167
		val segname = get_import_segment thy
skalberg@14518
   168
	    in
skalberg@14518
   169
		thy |> set_segment thyname segname
skalberg@14518
   170
		    |> clear_import_thy
skalberg@14518
   171
		    |> Theory.parent_path
skalberg@14518
   172
	    end) toks
skalberg@14516
   173
skalberg@14516
   174
val set_dump  = P.string -- P.string   >> setup_dump
skalberg@14518
   175
fun fl_dump toks  = Scan.succeed flush_dump toks
skalberg@14516
   176
val append_dump = (P.verbatim || P.string) >> add_dump
skalberg@14516
   177
skalberg@14516
   178
val parsers = 
skalberg@14516
   179
  [OuterSyntax.command "import_segment"
skalberg@14516
   180
		       "Set import segment name"
skalberg@14516
   181
		       K.thy_decl (import_segment >> Toplevel.theory),
skalberg@14516
   182
   OuterSyntax.command "import_theory"
skalberg@14516
   183
		       "Set default HOL4 theory name"
skalberg@14516
   184
		       K.thy_decl (import_theory >> Toplevel.theory),
skalberg@14516
   185
   OuterSyntax.command "end_import"
skalberg@14516
   186
		       "End HOL4 import"
skalberg@14516
   187
		       K.thy_decl (end_import >> Toplevel.theory),
skalberg@14516
   188
   OuterSyntax.command "setup_theory"
skalberg@14516
   189
		       "Setup HOL4 theory replaying"
skalberg@14516
   190
		       K.thy_decl (setup_theory >> Toplevel.theory),
skalberg@14516
   191
   OuterSyntax.command "end_setup"
skalberg@14516
   192
		       "End HOL4 setup"
skalberg@14516
   193
		       K.thy_decl (end_setup >> Toplevel.theory),
skalberg@14516
   194
   OuterSyntax.command "setup_dump"
skalberg@14516
   195
		       "Setup the dump file name"
skalberg@14516
   196
		       K.thy_decl (set_dump >> Toplevel.theory),
skalberg@14516
   197
   OuterSyntax.command "append_dump"
skalberg@14516
   198
		       "Add text to dump file"
skalberg@14516
   199
		       K.thy_decl (append_dump >> Toplevel.theory),
skalberg@14516
   200
   OuterSyntax.command "flush_dump"
skalberg@14516
   201
		       "Write the dump to file"
skalberg@14516
   202
		       K.thy_decl (fl_dump >> Toplevel.theory),
skalberg@14516
   203
   OuterSyntax.command "ignore_thms"
skalberg@14516
   204
		       "Theorems to ignore in next HOL4 theory import"
skalberg@14516
   205
		       K.thy_decl (ignore_thms >> Toplevel.theory),
skalberg@14516
   206
   OuterSyntax.command "type_maps"
skalberg@14516
   207
		       "Map HOL4 type names to existing Isabelle/HOL type names"
skalberg@14516
   208
		       K.thy_decl (type_maps >> Toplevel.theory),
skalberg@14516
   209
   OuterSyntax.command "def_maps"
skalberg@14516
   210
		       "Map HOL4 constant names to their primitive definitions"
skalberg@14516
   211
		       K.thy_decl (def_maps >> Toplevel.theory),
skalberg@14516
   212
   OuterSyntax.command "thm_maps"
skalberg@14516
   213
		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
skalberg@14516
   214
		       K.thy_decl (thm_maps >> Toplevel.theory),
skalberg@14516
   215
   OuterSyntax.command "const_renames"
skalberg@14516
   216
		       "Rename HOL4 const names"
skalberg@14516
   217
		       K.thy_decl (const_renames >> Toplevel.theory),
skalberg@14516
   218
   OuterSyntax.command "const_moves"
skalberg@14516
   219
		       "Rename HOL4 const names to other HOL4 constants"
skalberg@14516
   220
		       K.thy_decl (const_moves >> Toplevel.theory),
skalberg@14516
   221
   OuterSyntax.command "const_maps"
skalberg@14516
   222
		       "Map HOL4 const names to existing Isabelle/HOL const names"
skalberg@14516
   223
		       K.thy_decl (const_maps >> Toplevel.theory)]
skalberg@14516
   224
skalberg@14516
   225
fun setup () = (OuterSyntax.add_keywords[">"];
skalberg@14516
   226
		OuterSyntax.add_parsers parsers)
skalberg@14516
   227
skalberg@14516
   228
end
skalberg@14516
   229
skalberg@14516
   230
end