src/HOL/Import/import_syntax.ML
changeset 14516 a183dec876ab
child 14518 c3019a66180f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,227 @@
     1.4 +signature HOL4_IMPORT_SYNTAX =
     1.5 +sig
     1.6 +    type token = OuterSyntax.token
     1.7 +
     1.8 +    val import_segment: token list -> (theory -> theory) * token list
     1.9 +    val import_theory : token list -> (theory -> theory) * token list
    1.10 +    val end_import    : token list -> (theory -> theory) * token list
    1.11 +
    1.12 +    val setup_theory  : token list -> (theory -> theory) * token list
    1.13 +    val end_setup     : token list -> (theory -> theory) * token list
    1.14 +
    1.15 +    val thm_maps      : token list -> (theory -> theory) * token list
    1.16 +    val ignore_thms   : token list -> (theory -> theory) * token list
    1.17 +    val type_maps     : token list -> (theory -> theory) * token list
    1.18 +    val def_maps      : token list -> (theory -> theory) * token list
    1.19 +    val const_maps    : token list -> (theory -> theory) * token list
    1.20 +    val const_moves   : token list -> (theory -> theory) * token list
    1.21 +    val const_renames : token list -> (theory -> theory) * token list
    1.22 +
    1.23 +    val setup        : unit -> unit
    1.24 +end
    1.25 +
    1.26 +structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
    1.27 +struct
    1.28 +
    1.29 +type token = OuterSyntax.token
    1.30 +
    1.31 +local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.32 +
    1.33 +(* Parsers *)
    1.34 +
    1.35 +val import_segment = P.name >> set_import_segment
    1.36 +
    1.37 +val import_theory = P.name >> (fn thyname =>
    1.38 +			       fn thy =>
    1.39 +				  thy |> set_generating_thy thyname
    1.40 +				      |> Theory.add_path thyname
    1.41 +				      |> add_dump (";setup_theory " ^ thyname))
    1.42 +
    1.43 +val end_import = Scan.succeed
    1.44 +		     (fn thy =>
    1.45 +			 let
    1.46 +			     val thyname = get_generating_thy thy
    1.47 +			     val segname = get_import_segment thy
    1.48 +			     val (int_thms,facts) = Replay.setup_int_thms thyname thy
    1.49 +			     val thmnames = filter (not o should_ignore thyname thy) facts
    1.50 +			 in
    1.51 +			     thy |> clear_import_thy
    1.52 +				 |> set_segment thyname segname
    1.53 +				 |> set_used_names facts
    1.54 +				 |> Replay.import_thms thyname int_thms thmnames
    1.55 +				 |> clear_used_names
    1.56 +				 |> export_hol4_pending
    1.57 +				 |> Theory.parent_path
    1.58 +				 |> dump_import_thy thyname
    1.59 +				 |> add_dump ";end_setup"
    1.60 +			 end)
    1.61 +
    1.62 +val ignore_thms = Scan.repeat1 P.name
    1.63 +			       >> (fn ignored =>
    1.64 +				   fn thy =>
    1.65 +				      let
    1.66 +					  val thyname = get_import_thy thy
    1.67 +				      in
    1.68 +					  foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
    1.69 +				      end)
    1.70 +
    1.71 +val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    1.72 +			    >> (fn thmmaps =>
    1.73 +				fn thy =>
    1.74 +				   let
    1.75 +				       val thyname = get_import_thy thy
    1.76 +				   in
    1.77 +				       foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
    1.78 +				   end)
    1.79 +
    1.80 +val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    1.81 +			     >> (fn typmaps =>
    1.82 +				 fn thy =>
    1.83 +				    let
    1.84 +					val thyname = get_import_thy thy
    1.85 +				    in
    1.86 +					foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
    1.87 +				    end)
    1.88 +
    1.89 +val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    1.90 +			    >> (fn defmaps =>
    1.91 +				fn thy =>
    1.92 +				   let
    1.93 +				       val thyname = get_import_thy thy
    1.94 +				   in
    1.95 +				       foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
    1.96 +				   end)
    1.97 +
    1.98 +val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
    1.99 +				 >> (fn renames =>
   1.100 +				     fn thy =>
   1.101 +					let
   1.102 +					    val thyname = get_import_thy thy
   1.103 +					in
   1.104 +					    foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
   1.105 +					end)
   1.106 +																      
   1.107 +val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
   1.108 +			      >> (fn constmaps =>
   1.109 +				  fn thy =>
   1.110 +				     let
   1.111 +					 val thyname = get_import_thy thy
   1.112 +				     in
   1.113 +					 foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy
   1.114 +						 | (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)
   1.115 +				     end)
   1.116 +
   1.117 +val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
   1.118 +			       >> (fn constmaps =>
   1.119 +				   fn thy =>
   1.120 +				      let
   1.121 +					  val thyname = get_import_thy thy
   1.122 +				      in
   1.123 +					  foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy
   1.124 +						  | (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)
   1.125 +				      end)
   1.126 +
   1.127 +fun import_thy s =
   1.128 +    let
   1.129 +	val is = TextIO.openIn(s ^ ".imp")
   1.130 +	val inp = TextIO.inputAll is
   1.131 +	val _ = TextIO.closeIn is
   1.132 +	val orig_source = Source.of_string inp
   1.133 +	val symb_source = Symbol.source false orig_source
   1.134 +	val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
   1.135 +			 Scan.empty_lexicon)
   1.136 +	val get_lexes = fn () => !lexes
   1.137 +	val token_source = OuterLex.source false get_lexes (Position.line 1) symb_source
   1.138 +	val token_list = filter (not o (OuterLex.is_kind OuterLex.Space)) (Source.exhaust token_source)
   1.139 +	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
   1.140 +	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
   1.141 +	val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
   1.142 +	val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
   1.143 +	val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
   1.144 +	val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
   1.145 +	val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
   1.146 +	val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
   1.147 +	val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
   1.148 +	val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
   1.149 +	fun apply [] thy = thy
   1.150 +	  | apply (f::fs) thy = apply fs (f thy)
   1.151 +    in
   1.152 +	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
   1.153 +    end
   1.154 +
   1.155 +val setup_theory = P.name
   1.156 +		       >>
   1.157 +		       (fn thyname =>
   1.158 +			fn thy =>
   1.159 +			   case HOL4DefThy.get thy of
   1.160 +			       NoImport => thy |> import_thy thyname
   1.161 +			     | Generating _ => error "Currently generating a theory!"
   1.162 +			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
   1.163 +
   1.164 +val end_setup = Scan.succeed (fn thy =>
   1.165 +				 let
   1.166 +				     val thyname = get_import_thy thy
   1.167 +				     val segname = get_import_segment thy
   1.168 +				 in
   1.169 +				     thy |> set_segment thyname segname
   1.170 +					 |> clear_import_thy
   1.171 +					 |> Theory.parent_path
   1.172 +				 end)
   1.173 +
   1.174 +val set_dump  = P.string -- P.string   >> setup_dump
   1.175 +val fl_dump   = Scan.succeed flush_dump
   1.176 +val append_dump = (P.verbatim || P.string) >> add_dump
   1.177 +
   1.178 +val parsers = 
   1.179 +  [OuterSyntax.command "import_segment"
   1.180 +		       "Set import segment name"
   1.181 +		       K.thy_decl (import_segment >> Toplevel.theory),
   1.182 +   OuterSyntax.command "import_theory"
   1.183 +		       "Set default HOL4 theory name"
   1.184 +		       K.thy_decl (import_theory >> Toplevel.theory),
   1.185 +   OuterSyntax.command "end_import"
   1.186 +		       "End HOL4 import"
   1.187 +		       K.thy_decl (end_import >> Toplevel.theory),
   1.188 +   OuterSyntax.command "setup_theory"
   1.189 +		       "Setup HOL4 theory replaying"
   1.190 +		       K.thy_decl (setup_theory >> Toplevel.theory),
   1.191 +   OuterSyntax.command "end_setup"
   1.192 +		       "End HOL4 setup"
   1.193 +		       K.thy_decl (end_setup >> Toplevel.theory),
   1.194 +   OuterSyntax.command "setup_dump"
   1.195 +		       "Setup the dump file name"
   1.196 +		       K.thy_decl (set_dump >> Toplevel.theory),
   1.197 +   OuterSyntax.command "append_dump"
   1.198 +		       "Add text to dump file"
   1.199 +		       K.thy_decl (append_dump >> Toplevel.theory),
   1.200 +   OuterSyntax.command "flush_dump"
   1.201 +		       "Write the dump to file"
   1.202 +		       K.thy_decl (fl_dump >> Toplevel.theory),
   1.203 +   OuterSyntax.command "ignore_thms"
   1.204 +		       "Theorems to ignore in next HOL4 theory import"
   1.205 +		       K.thy_decl (ignore_thms >> Toplevel.theory),
   1.206 +   OuterSyntax.command "type_maps"
   1.207 +		       "Map HOL4 type names to existing Isabelle/HOL type names"
   1.208 +		       K.thy_decl (type_maps >> Toplevel.theory),
   1.209 +   OuterSyntax.command "def_maps"
   1.210 +		       "Map HOL4 constant names to their primitive definitions"
   1.211 +		       K.thy_decl (def_maps >> Toplevel.theory),
   1.212 +   OuterSyntax.command "thm_maps"
   1.213 +		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
   1.214 +		       K.thy_decl (thm_maps >> Toplevel.theory),
   1.215 +   OuterSyntax.command "const_renames"
   1.216 +		       "Rename HOL4 const names"
   1.217 +		       K.thy_decl (const_renames >> Toplevel.theory),
   1.218 +   OuterSyntax.command "const_moves"
   1.219 +		       "Rename HOL4 const names to other HOL4 constants"
   1.220 +		       K.thy_decl (const_moves >> Toplevel.theory),
   1.221 +   OuterSyntax.command "const_maps"
   1.222 +		       "Map HOL4 const names to existing Isabelle/HOL const names"
   1.223 +		       K.thy_decl (const_maps >> Toplevel.theory)]
   1.224 +
   1.225 +fun setup () = (OuterSyntax.add_keywords[">"];
   1.226 +		OuterSyntax.add_parsers parsers)
   1.227 +
   1.228 +end
   1.229 +
   1.230 +end