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