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