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