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