1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Wed Feb 15 21:35:13 2006 +0100
1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Wed Feb 15 23:57:06 2006 +0100
1.3 @@ -5,6 +5,10 @@
1.4
1.5 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
1.6
1.7 +;skip_import_dir "/home/obua/tmp/cache"
1.8 +
1.9 +;skip_import on
1.10 +
1.11 ;import_segment "hollight";
1.12
1.13 setup_dump "../HOLLight" "HOLLight";
1.14 @@ -24,9 +28,9 @@
1.15 DEF_IND_SUC
1.16 DEF_IND_0
1.17 DEF_NUM_REP
1.18 - (* TYDEF_sum
1.19 + TYDEF_sum
1.20 DEF_INL
1.21 - DEF_INR*);
1.22 + DEF_INR;
1.23
1.24 type_maps
1.25 ind > Nat.ind
1.26 @@ -34,8 +38,8 @@
1.27 fun > fun
1.28 N_1 > Product_Type.unit
1.29 prod > "*"
1.30 - num > nat;
1.31 - (* sum > "+";*)
1.32 + num > nat
1.33 + sum > "+";
1.34
1.35 const_renames
1.36 "==" > "eqeq"
1.37 @@ -74,10 +78,10 @@
1.38 "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.39 "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.40 BIT0 > HOLLightCompat.NUMERAL_BIT0
1.41 - BIT1 > HOL4Compat.NUMERAL_BIT1;
1.42 - (* INL > Sum_Type.Inl
1.43 - INR > Sum_Type.Inr
1.44 - HAS_SIZE > HOLLightCompat.HAS_SIZE*)
1.45 + BIT1 > HOL4Compat.NUMERAL_BIT1
1.46 + INL > Sum_Type.Inl
1.47 + INR > Sum_Type.Inr;
1.48 + (* HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
1.49
1.50 (*import_until "TYDEF_sum"
1.51
2.1 --- a/src/HOL/Import/HOL4Compat.thy Wed Feb 15 21:35:13 2006 +0100
2.2 +++ b/src/HOL/Import/HOL4Compat.thy Wed Feb 15 23:57:06 2006 +0100
2.3 @@ -3,7 +3,8 @@
2.4 Author: Sebastian Skalberg (TU Muenchen)
2.5 *)
2.6
2.7 -theory HOL4Compat imports HOL4Setup Divides Primes Real begin
2.8 +theory HOL4Compat imports HOL4Setup Divides Primes Real
2.9 +begin
2.10
2.11 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
2.12 by auto
3.1 --- a/src/HOL/Import/HOL4Setup.thy Wed Feb 15 21:35:13 2006 +0100
3.2 +++ b/src/HOL/Import/HOL4Setup.thy Wed Feb 15 23:57:06 2006 +0100
3.3 @@ -3,9 +3,8 @@
3.4 Author: Sebastian Skalberg (TU Muenchen)
3.5 *)
3.6
3.7 -theory HOL4Setup imports MakeEqual
3.8 - uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
3.9 - ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
3.10 +theory HOL4Setup imports MakeEqual ImportRecorder
3.11 + uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
3.12
3.13 section {* General Setup *}
3.14
4.1 --- a/src/HOL/Import/HOLLightCompat.thy Wed Feb 15 21:35:13 2006 +0100
4.2 +++ b/src/HOL/Import/HOLLightCompat.thy Wed Feb 15 23:57:06 2006 +0100
4.3 @@ -91,6 +91,16 @@
4.4 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
4.5 by (simp add: NUMERAL_BIT1_def)
4.6
4.7 +consts
4.8 + sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
4.9
4.10 +primrec
4.11 + "sumlift f g (Inl a) = f a"
4.12 + "sumlift f g (Inr b) = g b"
4.13 +
4.14 +lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
4.15 + apply (rule exI[where x="sumlift Inl' Inr'"])
4.16 + apply auto
4.17 + done
4.18
4.19 end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Import/ImportRecorder.thy Wed Feb 15 23:57:06 2006 +0100
5.3 @@ -0,0 +1,4 @@
5.4 +theory ImportRecorder imports Main
5.5 +uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
5.6 +begin
5.7 +end
5.8 \ No newline at end of file
6.1 --- a/src/HOL/Import/import_syntax.ML Wed Feb 15 21:35:13 2006 +0100
6.2 +++ b/src/HOL/Import/import_syntax.ML Wed Feb 15 23:57:06 2006 +0100
6.3 @@ -6,6 +6,7 @@
6.4 signature HOL4_IMPORT_SYNTAX =
6.5 sig
6.6 type token = OuterSyntax.token
6.7 + type command = token list -> (theory -> theory) * token list
6.8
6.9 val import_segment: token list -> (theory -> theory) * token list
6.10 val import_theory : token list -> (theory -> theory) * token list
6.11 @@ -22,6 +23,9 @@
6.12 val const_moves : token list -> (theory -> theory) * token list
6.13 val const_renames : token list -> (theory -> theory) * token list
6.14
6.15 + val skip_import_dir : token list -> (theory -> theory) * token list
6.16 + val skip_import : token list -> (theory -> theory) * token list
6.17 +
6.18 val setup : unit -> unit
6.19 end
6.20
6.21 @@ -29,6 +33,7 @@
6.22 struct
6.23
6.24 type token = OuterSyntax.token
6.25 +type command = token list -> (theory -> theory) * token list
6.26
6.27 local structure P = OuterParse and K = OuterKeyword in
6.28
6.29 @@ -36,12 +41,20 @@
6.30
6.31 val import_segment = P.name >> set_import_segment
6.32
6.33 +
6.34 val import_theory = P.name >> (fn thyname =>
6.35 fn thy =>
6.36 thy |> set_generating_thy thyname
6.37 |> Theory.add_path thyname
6.38 |> add_dump (";setup_theory " ^ thyname))
6.39
6.40 +fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
6.41 +val skip_import_dir : command = P.string >> do_skip_import_dir
6.42 +
6.43 +val lower = String.map Char.toLower
6.44 +fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
6.45 +val skip_import : command = P.short_ident >> do_skip_import
6.46 +
6.47 fun end_import toks =
6.48 Scan.succeed
6.49 (fn thy =>
6.50 @@ -50,13 +63,21 @@
6.51 val segname = get_import_segment thy
6.52 val (int_thms,facts) = Replay.setup_int_thms thyname thy
6.53 val thmnames = List.filter (not o should_ignore thyname thy) facts
6.54 - (* val _ = set show_types
6.55 - val _ = set show_sorts*)
6.56 + fun replay thy =
6.57 + let
6.58 + val _ = ImportRecorder.load_history thyname
6.59 + val thy = Replay.import_thms thyname int_thms thmnames thy
6.60 + handle x => (ImportRecorder.save_history thyname; raise x)
6.61 + val _ = ImportRecorder.save_history thyname
6.62 + val _ = ImportRecorder.clear_history ()
6.63 + in
6.64 + thy
6.65 + end
6.66 in
6.67 thy |> clear_import_thy
6.68 |> set_segment thyname segname
6.69 |> set_used_names facts
6.70 - |> Replay.import_thms thyname int_thms thmnames
6.71 + |> replay
6.72 |> clear_used_names
6.73 |> export_hol4_pending
6.74 |> Theory.parent_path
6.75 @@ -211,6 +232,12 @@
6.76 OuterSyntax.command "end_import"
6.77 "End HOL4 import"
6.78 K.thy_decl (end_import >> Toplevel.theory),
6.79 + OuterSyntax.command "skip_import_dir"
6.80 + "Sets caching directory for skipping importing"
6.81 + K.thy_decl (skip_import_dir >> Toplevel.theory),
6.82 + OuterSyntax.command "skip_import"
6.83 + "Switches skipping importing on or off"
6.84 + K.thy_decl (skip_import >> Toplevel.theory),
6.85 OuterSyntax.command "setup_theory"
6.86 "Setup HOL4 theory replaying"
6.87 K.thy_decl (setup_theory >> Toplevel.theory),
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Import/importrecorder.ML Wed Feb 15 23:57:06 2006 +0100
7.3 @@ -0,0 +1,253 @@
7.4 +signature IMPORT_RECORDER =
7.5 +sig
7.6 +
7.7 + datatype deltastate = Consts of (string * typ * mixfix) list
7.8 + | Specification of (string * string * bool) list * term
7.9 + | Hol_mapping of string * string * string
7.10 + | Hol_pending of string * string * term
7.11 + | Hol_const_mapping of string * string * string
7.12 + | Hol_move of string * string
7.13 + | Defs of string * term
7.14 + | Hol_theorem of string * string * term
7.15 + | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
7.16 + | Hol_type_mapping of string * string * string
7.17 + | Indexed_theorem of int * term
7.18 +
7.19 + datatype history = History of history_entry list
7.20 + and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
7.21 +
7.22 + val get_history : unit -> history
7.23 + val set_history : history -> unit
7.24 + val clear_history : unit -> unit
7.25 +
7.26 + val start_replay_proof : string -> string -> unit
7.27 + val stop_replay_proof : string -> string -> unit
7.28 + val abort_replay_proof : string -> string -> unit
7.29 +
7.30 + val add_consts : (string * typ * mixfix) list -> unit
7.31 + val add_specification : (string * string * bool) list -> thm -> unit
7.32 + val add_hol_mapping : string -> string -> string -> unit
7.33 + val add_hol_pending : string -> string -> thm -> unit
7.34 + val add_hol_const_mapping : string -> string -> string -> unit
7.35 + val add_hol_move : string -> string -> unit
7.36 + val add_defs : string -> term -> unit
7.37 + val add_hol_theorem : string -> string -> thm -> unit
7.38 + val add_typedef : string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
7.39 + val add_hol_type_mapping : string -> string -> string -> unit
7.40 + val add_indexed_theorem : int -> thm -> unit
7.41 +
7.42 + val set_skip_import_dir : string option -> unit
7.43 + val get_skip_import_dir : unit -> string option
7.44 +
7.45 + val set_skip_import : bool -> unit
7.46 + val get_skip_import : unit -> bool
7.47 +
7.48 + val save_history : string -> unit
7.49 + val load_history : string -> unit
7.50 +end
7.51 +
7.52 +structure ImportRecorder :> IMPORT_RECORDER =
7.53 +struct
7.54 +
7.55 +datatype deltastate = Consts of (string * typ * mixfix) list
7.56 + | Specification of (string * string * bool) list * term
7.57 + | Hol_mapping of string * string * string
7.58 + | Hol_pending of string * string * term
7.59 + | Hol_const_mapping of string * string * string
7.60 + | Hol_move of string * string
7.61 + | Defs of string * term
7.62 + | Hol_theorem of string * string * term
7.63 + | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
7.64 + | Hol_type_mapping of string * string * string
7.65 + | Indexed_theorem of int * term
7.66 +
7.67 +datatype history_entry = StartReplay of string*string
7.68 + | StopReplay of string*string
7.69 + | AbortReplay of string*string
7.70 + | Delta of deltastate list
7.71 +
7.72 +val history = ref ([]:history_entry list)
7.73 +val history_dir = ref (SOME "")
7.74 +val skip_imports = ref false
7.75 +
7.76 +fun set_skip_import b = skip_imports := b
7.77 +fun get_skip_import () = !skip_imports
7.78 +
7.79 +fun clear_history () = history := []
7.80 +
7.81 +fun add_delta d = history := (case !history of (Delta ds)::hs => (Delta (d::ds))::hs | hs => (Delta [d])::hs)
7.82 +fun add_replay r = history := (r :: (!history))
7.83 +
7.84 +local
7.85 + open XMLConvOutput
7.86 + val consts = list (triple string typ mixfix)
7.87 + val specification = pair (list (triple string string bool)) term
7.88 + val hol_mapping = triple string string string
7.89 + val hol_pending = triple string string term
7.90 + val hol_const_mapping = triple string string string
7.91 + val hol_move = pair string string
7.92 + val defs = pair string term
7.93 + val hol_theorem = triple string string term
7.94 + val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
7.95 + val hol_type_mapping = triple string string string
7.96 + val indexed_theorem = pair int term
7.97 + val entry = pair string string
7.98 +
7.99 + fun delta (Consts args) = wrap "consts" consts args
7.100 + | delta (Specification args) = wrap "specification" specification args
7.101 + | delta (Hol_mapping args) = wrap "hol_mapping" hol_mapping args
7.102 + | delta (Hol_pending args) = wrap "hol_pending" hol_pending args
7.103 + | delta (Hol_const_mapping args) = wrap "hol_const_mapping" hol_const_mapping args
7.104 + | delta (Hol_move args) = wrap "hol_move" hol_move args
7.105 + | delta (Defs args) = wrap "defs" defs args
7.106 + | delta (Hol_theorem args) = wrap "hol_theorem" hol_theorem args
7.107 + | delta (Typedef args) = wrap "typedef" typedef args
7.108 + | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
7.109 + | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
7.110 +
7.111 + fun history_entry (StartReplay args) = wrap "startreplay" entry args
7.112 + | history_entry (StopReplay args) = wrap "stopreplay" entry args
7.113 + | history_entry (AbortReplay args) = wrap "abortreplay" entry args
7.114 + | history_entry (Delta args) = wrap "delta" (list delta) args
7.115 +in
7.116 +
7.117 +val xml_of_history = list history_entry
7.118 +
7.119 +end
7.120 +
7.121 +local
7.122 + open XMLConvInput
7.123 + val consts = list (triple string typ mixfix)
7.124 + val specification = pair (list (triple string string bool)) term
7.125 + val hol_mapping = triple string string string
7.126 + val hol_pending = triple string string term
7.127 + val hol_const_mapping = triple string string string
7.128 + val hol_move = pair string string
7.129 + val defs = pair string term
7.130 + val hol_theorem = triple string string term
7.131 + val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
7.132 + val hol_type_mapping = triple string string string
7.133 + val indexed_theorem = pair int term
7.134 + val entry = pair string string
7.135 +
7.136 + fun delta "consts" = unwrap Consts consts
7.137 + | delta "specification" = unwrap Specification specification
7.138 + | delta "hol_mapping" = unwrap Hol_mapping hol_mapping
7.139 + | delta "hol_pending" = unwrap Hol_pending hol_pending
7.140 + | delta "hol_const_mapping" = unwrap Hol_const_mapping hol_const_mapping
7.141 + | delta "hol_move" = unwrap Hol_move hol_move
7.142 + | delta "defs" = unwrap Defs defs
7.143 + | delta "hol_theorem" = unwrap Hol_theorem hol_theorem
7.144 + | delta "typedef" = unwrap Typedef typedef
7.145 + | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
7.146 + | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
7.147 + | delta _ = raise ParseException "delta"
7.148 +
7.149 + val delta = fn e => delta (name_of_wrap e) e
7.150 +
7.151 + fun history_entry "startreplay" = unwrap StartReplay entry
7.152 + | history_entry "stopreplay" = unwrap StopReplay entry
7.153 + | history_entry "abortreplay" = unwrap AbortReplay entry
7.154 + | history_entry "delta" = unwrap Delta (list delta)
7.155 + | history_entry _ = raise ParseException "history_entry"
7.156 +
7.157 + val history_entry = fn e => history_entry (name_of_wrap e) e
7.158 +in
7.159 +
7.160 +val history_of_xml = list history_entry
7.161 +
7.162 +end
7.163 +
7.164 +fun start_replay_proof thyname thmname = add_replay (StartReplay (thyname, thmname))
7.165 +fun stop_replay_proof thyname thmname = add_replay (StopReplay (thyname, thmname))
7.166 +fun abort_replay_proof thyname thmname = add_replay (AbortReplay (thyname, thmname))
7.167 +fun add_hol_theorem thyname thmname thm = add_delta (Hol_theorem (thyname, thmname, prop_of thm))
7.168 +fun add_hol_mapping thyname thmname isaname = add_delta (Hol_mapping (thyname, thmname, isaname))
7.169 +fun add_consts consts = add_delta (Consts consts)
7.170 +fun add_typedef thmname_opt typ c absrep_opt th = add_delta (Typedef (thmname_opt, typ, c, absrep_opt, prop_of th))
7.171 +fun add_defs thmname eq = add_delta (Defs (thmname, eq))
7.172 +fun add_hol_const_mapping thyname constname fullcname = add_delta (Hol_const_mapping (thyname, constname, fullcname))
7.173 +fun add_hol_move fullname moved_thmname = add_delta (Hol_move (fullname, moved_thmname))
7.174 +fun add_hol_type_mapping thyname tycname fulltyname = add_delta (Hol_type_mapping (thyname, tycname, fulltyname))
7.175 +fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
7.176 +fun add_specification names th = add_delta (Specification (names, prop_of th))
7.177 +fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
7.178 +
7.179 +fun set_skip_import_dir dir = (history_dir := dir)
7.180 +fun get_skip_import_dir () = !history_dir
7.181 +
7.182 +fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (thyname^".history")))
7.183 +
7.184 +fun save_history thyname =
7.185 + if get_skip_import () then
7.186 + XMLConv.write_to_file xml_of_history (get_filename thyname) (!history)
7.187 + else
7.188 + ()
7.189 +
7.190 +fun load_history thyname =
7.191 + if get_skip_import () then
7.192 + let
7.193 + val filename = get_filename thyname
7.194 + val _ = writeln "load_history / before"
7.195 + val _ =
7.196 + if File.exists (Path.unpack filename) then
7.197 + (history := XMLConv.read_from_file history_of_xml (get_filename thyname))
7.198 + else
7.199 + clear_history ()
7.200 + val _ = writeln "load_history / after"
7.201 + in
7.202 + ()
7.203 + end
7.204 + else
7.205 + ()
7.206 +
7.207 +
7.208 +datatype history = History of history_entry list
7.209 + and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
7.210 +
7.211 +exception CONV
7.212 +
7.213 +fun conv_histories ((StartReplay (thyname, thmname))::rest) =
7.214 + let
7.215 + val (hs, rest) = conv_histories rest
7.216 + fun continue thyname' thmname' aborted rest =
7.217 + if thyname = thyname' andalso thmname = thmname' then
7.218 + let
7.219 + val (hs', rest) = conv_histories rest
7.220 + in
7.221 + ((ThmEntry (thyname, thmname, aborted, History hs))::hs', rest)
7.222 + end
7.223 + else
7.224 + raise CONV
7.225 + in
7.226 + case rest of
7.227 + (StopReplay (thyname',thmname'))::rest =>
7.228 + continue thyname' thmname' false rest
7.229 + | (AbortReplay (thyname',thmname'))::rest =>
7.230 + continue thyname' thmname' true rest
7.231 + | [] => (hs, [])
7.232 + | _ => raise CONV
7.233 + end
7.234 + | conv_histories ((Delta ds)::rest) = (conv_histories rest) |>> (fn hs => (DeltaEntry (rev ds))::hs)
7.235 + | conv_histories rest = ([], rest)
7.236 +
7.237 +fun conv es =
7.238 + let
7.239 + val (h, rest) = conv_histories (rev es)
7.240 + in
7.241 + case rest of
7.242 + [] => h
7.243 + | _ => raise CONV
7.244 + end
7.245 +
7.246 +fun get_history () = History (conv (!history))
7.247 +
7.248 +fun reconv (History hs) rs = fold reconv_entry hs rs
7.249 +and reconv_entry (ThmEntry (thyname, thmname, aborted, h)) rs =
7.250 + ((if aborted then AbortReplay else StopReplay) (thyname, thmname)) :: (reconv h ((StartReplay (thyname, thmname))::rs))
7.251 + | reconv_entry (DeltaEntry ds) rs = (Delta (rev ds))::rs
7.252 +
7.253 +fun set_history h = history := reconv h []
7.254 +
7.255 +
7.256 +end
8.1 --- a/src/HOL/Import/lazy_scan.ML Wed Feb 15 21:35:13 2006 +0100
8.2 +++ b/src/HOL/Import/lazy_scan.ML Wed Feb 15 23:57:06 2006 +0100
8.3 @@ -19,7 +19,7 @@
8.4 val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
8.5 val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
8.6 val ^^ : ('a,string) scanner * ('a,string) scanner
8.7 - -> ('a,string) scanner
8.8 + -> ('a,string) scanner
8.9 val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
8.10 val one : ('a -> bool) -> ('a,'a) scanner
8.11 val succeed : 'b -> ('a,'b) scanner
8.12 @@ -30,11 +30,14 @@
8.13 val repeat : ('a,'b) scanner -> ('a,'b list) scanner
8.14 val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
8.15 val ahead : ('a,'b) scanner -> ('a,'b) scanner
8.16 - val unless : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
8.17 + val unless : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
8.18 val $$ : ''a -> (''a,''a) scanner
8.19 val !! : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
8.20 val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
8.21
8.22 + val scan_id : (string, string) scanner
8.23 + val this : ''a list -> (''a, ''a list) scanner
8.24 + val this_string : string -> (string, string) scanner
8.25 end
8.26
8.27 structure LazyScan :> LAZY_SCAN =
8.28 @@ -203,4 +206,11 @@
8.29 LazySeq.make (fn () => F toks)
8.30 end
8.31
8.32 +val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
8.33 +
8.34 +fun this [] = (fn toks => ([], toks))
8.35 + | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
8.36 +
8.37 +fun this_string s = this (explode s) >> K s
8.38 +
8.39 end
9.1 --- a/src/HOL/Import/lazy_seq.ML Wed Feb 15 21:35:13 2006 +0100
9.2 +++ b/src/HOL/Import/lazy_seq.ML Wed Feb 15 23:57:06 2006 +0100
9.3 @@ -21,6 +21,7 @@
9.4 val getItem : 'a seq -> ('a * 'a seq) option
9.5 val nth : 'a seq * int -> 'a
9.6 val take : 'a seq * int -> 'a seq
9.7 + val take_at_most : 'a seq * int -> 'a list
9.8 val drop : 'a seq * int -> 'a seq
9.9 val rev : 'a seq -> 'a seq
9.10 val concat : 'a seq seq -> 'a seq
9.11 @@ -90,7 +91,7 @@
9.12 fun getItem (Seq s) = force s
9.13 fun make f = Seq (delay f)
9.14
9.15 -fun null s = isSome (getItem s)
9.16 +fun null s = is_none (getItem s)
9.17
9.18 local
9.19 fun F n NONE = n
9.20 @@ -148,6 +149,12 @@
9.21 else F' s n
9.22 end
9.23
9.24 +fun take_at_most (s,n) =
9.25 + if n <= 0 then [] else
9.26 + case getItem s of
9.27 + NONE => []
9.28 + | SOME (x,s') => x::(take_at_most (s',n-1))
9.29 +
9.30 local
9.31 fun F s 0 = s
9.32 | F NONE _ = raise Subscript
10.1 --- a/src/HOL/Import/proof_kernel.ML Wed Feb 15 21:35:13 2006 +0100
10.2 +++ b/src/HOL/Import/proof_kernel.ML Wed Feb 15 23:57:06 2006 +0100
10.3 @@ -73,6 +73,7 @@
10.4
10.5 val to_isa_thm : thm -> (term * term) list * Thm.thm
10.6 val to_isa_term: term -> Term.term
10.7 + val to_hol_thm : Thm.thm -> thm
10.8
10.9 val REFL : term -> theory -> theory * thm
10.10 val ASSUME : term -> theory -> theory * thm
10.11 @@ -124,6 +125,7 @@
10.12
10.13 fun hthm2thm (HOLThm (_, th)) = th
10.14
10.15 +fun to_hol_thm th = HOLThm ([], th)
10.16
10.17 datatype proof_info
10.18 = Info of {disk_info: (string * string) option ref}
10.19 @@ -199,6 +201,8 @@
10.20 ct)
10.21 end
10.22
10.23 +exception SMART_STRING
10.24 +
10.25 fun smart_string_of_cterm ct =
10.26 let
10.27 val {sign,t,T,...} = rep_cterm ct
10.28 @@ -207,8 +211,10 @@
10.29 handle TERM _ => ct)
10.30 fun match cu = t aconv (term_of cu)
10.31 fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
10.32 - | G 1 = Library.setmp show_all_types true (G 0)
10.33 - | G _ = error ("ProofKernel.smart_string_of_cterm internal error")
10.34 + | G 1 = Library.setmp show_brackets true (G 0)
10.35 + | G 2 = Library.setmp show_all_types true (G 0)
10.36 + | G 3 = Library.setmp show_brackets true (G 2)
10.37 + | G _ = raise SMART_STRING
10.38 fun F n =
10.39 let
10.40 val str = Library.setmp show_brackets false (G n string_of_cterm) ct
10.41 @@ -219,6 +225,7 @@
10.42 else F (n+1)
10.43 end
10.44 handle ERROR mesg => F (n+1)
10.45 + | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
10.46 in
10.47 Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
10.48 end
10.49 @@ -1041,14 +1048,7 @@
10.50 res
10.51 end
10.52
10.53 -(* rotate left k places, leaving the first j and last l premises alone
10.54 -*)
10.55 -
10.56 -fun permute_prems j k 0 th = Thm.permute_prems j k th
10.57 - | permute_prems j k l th =
10.58 - th |> Thm.permute_prems 0 (~l)
10.59 - |> Thm.permute_prems (j+l) k
10.60 - |> Thm.permute_prems 0 l
10.61 +val permute_prems = Thm.permute_prems
10.62
10.63 fun rearrange sg tm th =
10.64 let
10.65 @@ -1140,7 +1140,7 @@
10.66 val new_name = new_name' "a"
10.67 fun replace_name n' (Free (n, t)) = Free (n', t)
10.68 | replace_name n' _ = ERR "replace_name"
10.69 - (* map: old oder fresh name -> old free,
10.70 + (* map: old or fresh name -> old free,
10.71 invmap: old free which has fresh name assigned to it -> fresh name *)
10.72 fun dis (v, mapping as (map,invmap)) =
10.73 let val n = name_of v in
10.74 @@ -1176,7 +1176,7 @@
10.75 fun if_debug f x = if !debug then f x else ()
10.76 val message = if_debug writeln
10.77
10.78 -val conjE_helper = Thm.permute_prems 0 1 conjE
10.79 +val conjE_helper = permute_prems 0 1 conjE
10.80
10.81 fun get_hol4_thm thyname thmname thy =
10.82 case get_hol4_theorem thyname thmname thy of
10.83 @@ -1286,6 +1286,8 @@
10.84 val hth as HOLThm args = mk_res th
10.85 val thy' = thy |> add_hol4_theorem thyname thmname args
10.86 |> add_hol4_mapping thyname thmname isaname
10.87 + val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
10.88 + val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
10.89 in
10.90 (thy',SOME hth)
10.91 end
10.92 @@ -1351,6 +1353,7 @@
10.93 val rew = rewrite_hol4_term (concl_of th) thy
10.94 val th = equal_elim rew th
10.95 val thy' = add_hol4_pending thyname thmname args thy
10.96 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
10.97 val th = disambiguate_frees th
10.98 val thy2 = if gen_output
10.99 then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
10.100 @@ -1903,34 +1906,45 @@
10.101 val csyn = mk_syn thy constname
10.102 val thy1 = case HOL4DefThy.get thy of
10.103 Replaying _ => thy
10.104 - | _ => Theory.add_consts_i [(constname,ctype,csyn)] thy
10.105 + | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Theory.add_consts_i [(constname,ctype,csyn)] thy)
10.106 val eq = mk_defeq constname rhs' thy1
10.107 val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
10.108 + val _ = ImportRecorder.add_defs thmname eq
10.109 val def_thm = hd thms
10.110 val thm' = def_thm RS meta_eq_to_obj_eq_thm
10.111 val (thy',th) = (thy2, thm')
10.112 val fullcname = Sign.intern_const thy' constname
10.113 val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
10.114 + val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
10.115 val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
10.116 val rew = rewrite_hol4_term eq thy''
10.117 val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
10.118 val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
10.119 then
10.120 - add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
10.121 + let
10.122 + val p1 = quotename constname
10.123 + val p2 = string_of_ctyp (ctyp_of thy'' ctype)
10.124 + val p3 = Syntax.string_of_mixfix csyn
10.125 + val p4 = smart_string_of_cterm crhs
10.126 + in
10.127 + add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
10.128 + end
10.129 else
10.130 - add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
10.131 - "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
10.132 - thy''
10.133 -
10.134 + (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
10.135 + "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
10.136 + thy'')
10.137 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
10.138 - SOME (_,res) => HOLThm(rens_of linfo,res)
10.139 - | NONE => raise ERR "new_definition" "Bad conclusion"
10.140 + SOME (_,res) => HOLThm(rens_of linfo,res)
10.141 + | NONE => raise ERR "new_definition" "Bad conclusion"
10.142 val fullname = Sign.full_name thy22 thmname
10.143 val thy22' = case opt_get_output_thy thy22 of
10.144 - "" => add_hol4_mapping thyname thmname fullname thy22
10.145 + "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
10.146 + add_hol4_mapping thyname thmname fullname thy22)
10.147 | output_thy =>
10.148 let
10.149 val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
10.150 + val _ = ImportRecorder.add_hol_move fullname moved_thmname
10.151 + val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
10.152 in
10.153 thy22 |> add_hol4_move fullname moved_thmname
10.154 |> add_hol4_mapping thyname thmname moved_thmname
10.155 @@ -1981,6 +1995,7 @@
10.156 val str = Library.foldl (fn (acc,(c,T,csyn)) =>
10.157 acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
10.158 val thy' = add_dump str thy
10.159 + val _ = ImportRecorder.add_consts consts
10.160 in
10.161 Theory.add_consts_i consts thy'
10.162 end
10.163 @@ -1988,9 +2003,11 @@
10.164 val thy1 = foldr (fn(name,thy)=>
10.165 snd (get_defname thyname name thy)) thy1 names
10.166 fun new_name name = fst (get_defname thyname name thy1)
10.167 + val names' = map (fn name => (new_name name,name,false)) names
10.168 val (thy',res) = SpecificationPackage.add_specification NONE
10.169 - (map (fn name => (new_name name,name,false)) names)
10.170 + names'
10.171 (thy1,th)
10.172 + val _ = ImportRecorder.add_specification names' th
10.173 val res' = Drule.freeze_all res
10.174 val hth = HOLThm(rens,res')
10.175 val rew = rewrite_hol4_term (concl_of res') thy'
10.176 @@ -2056,17 +2073,20 @@
10.177 val tnames = map fst tfrees
10.178 val tsyn = mk_syn thy tycname
10.179 val typ = (tycname,tnames,tsyn)
10.180 - val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
10.181 + val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
10.182 + val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
10.183
10.184 val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
10.185
10.186 val fulltyname = Sign.intern_type thy' tycname
10.187 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
10.188 + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
10.189
10.190 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
10.191 val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
10.192 else ()
10.193 val thy4 = add_hol4_pending thyname thmname args thy''
10.194 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
10.195
10.196 val rew = rewrite_hol4_term (concl_of td_th) thy4
10.197 val th = equal_elim rew (Thm.transfer thy4 td_th)
10.198 @@ -2146,7 +2166,8 @@
10.199 val tnames = sort string_ord (map fst tfrees)
10.200 val tsyn = mk_syn thy tycname
10.201 val typ = (tycname,tnames,tsyn)
10.202 - val (thy',typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
10.203 + val (thy', typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
10.204 + val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
10.205 val fulltyname = Sign.intern_type thy' tycname
10.206 val aty = Type (fulltyname, map mk_vartype tnames)
10.207 val abs_ty = tT --> aty
10.208 @@ -2161,9 +2182,11 @@
10.209 val _ = if Drule.vars_of th4 = [] then () else raise ERR "type_introduction" "no term variables expected any more"
10.210 val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
10.211 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
10.212 + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
10.213 val _ = message "step 4"
10.214 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
10.215 val thy4 = add_hol4_pending thyname thmname args thy''
10.216 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
10.217
10.218 val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
10.219 val c =
11.1 --- a/src/HOL/Import/replay.ML Wed Feb 15 21:35:13 2006 +0100
11.2 +++ b/src/HOL/Import/replay.ML Wed Feb 15 23:57:06 2006 +0100
11.3 @@ -9,6 +9,7 @@
11.4 structure P = ProofKernel
11.5
11.6 open ProofKernel
11.7 +open ImportRecorder
11.8
11.9 exception REPLAY of string * string
11.10 fun ERR f mesg = REPLAY (f,mesg)
11.11 @@ -16,6 +17,7 @@
11.12
11.13 fun replay_proof int_thms thyname thmname prf thy =
11.14 let
11.15 + val _ = ImportRecorder.start_replay_proof thyname thmname
11.16 fun rp (PRefl tm) thy = P.REFL tm thy
11.17 | rp (PInstT(p,lambda)) thy =
11.18 let
11.19 @@ -270,8 +272,13 @@
11.20 | _ => rp pc thy
11.21 end
11.22 in
11.23 - rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
11.24 - end
11.25 + let
11.26 + val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
11.27 + val _ = ImportRecorder.stop_replay_proof thyname thmname
11.28 + in
11.29 + x
11.30 + end
11.31 + end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
11.32
11.33 fun setup_int_thms thyname thy =
11.34 let
11.35 @@ -312,9 +319,77 @@
11.36 replay_fact (thmname,thy)
11.37 end
11.38
11.39 +fun replay_chached_thm int_thms thyname thmname =
11.40 + let
11.41 + fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
11.42 + fun err msg = raise ERR "replay_cached_thm" msg
11.43 + val _ = writeln ("Replaying (from cache) "^thmname^" ...")
11.44 + fun rps [] thy = thy
11.45 + | rps (t::ts) thy = rps ts (rp t thy)
11.46 + and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy
11.47 + | rp (DeltaEntry ds) thy = fold delta ds thy
11.48 +(* datatype deltastate = Consts of (string * typ * mixfix) list
11.49 + | Specification of (string * string * bool) list * term
11.50 + | Hol_mapping of string * string * string
11.51 + | Hol_pending of string * string * term
11.52 + | Hol_const_mapping of string * string * string
11.53 + | Hol_move of string * string
11.54 + | Defs of string * term
11.55 + | Hol_theorem of string * string * term
11.56 + | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
11.57 + | Hol_type_mapping of string * string * string
11.58 + | Indexed_theorem of int * term
11.59 +*)
11.60 + and delta (Specification (names, th)) thy =
11.61 + fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
11.62 + | delta (Hol_mapping (thyname, thmname, isaname)) thy =
11.63 + add_hol4_mapping thyname thmname isaname thy
11.64 + | delta (Hol_pending (thyname, thmname, th)) thy =
11.65 + add_hol4_pending thyname thmname ([], th_of thy th) thy
11.66 + | delta (Consts cs) thy = Theory.add_consts_i cs thy
11.67 + | delta (Hol_const_mapping (thyname, constname, fullcname)) thy =
11.68 + add_hol4_const_mapping thyname constname true fullcname thy
11.69 + | delta (Hol_move (fullname, moved_thmname)) thy =
11.70 + add_hol4_move fullname moved_thmname thy
11.71 + | delta (Defs (thmname, eq)) thy =
11.72 + snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
11.73 + | delta (Hol_theorem (thyname, thmname, th)) thy =
11.74 + add_hol4_theorem thyname thmname ([], th_of thy th) thy
11.75 + | delta (Typedef (thmname, typ, c, repabs, th)) thy =
11.76 + fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
11.77 + | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
11.78 + add_hol4_type_mapping thyname tycname true fulltyname thy
11.79 + | delta (Indexed_theorem (i, th)) thy =
11.80 + (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)
11.81 + in
11.82 + rps
11.83 + end
11.84 +
11.85 fun import_thms thyname int_thms thmnames thy =
11.86 let
11.87 - fun replay_fact (thy,thmname) =
11.88 + fun zip names [] = ([], names)
11.89 + | zip [] _ = ([], [])
11.90 + | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) =
11.91 + if thyname = thyname' andalso thmname = thmname' then
11.92 + (if aborted then ([], thmname::names) else
11.93 + let
11.94 + val _ = writeln ("theorem is in-sync: "^thmname)
11.95 + val (cached,normal) = zip names ys
11.96 + in
11.97 + (entry::cached, normal)
11.98 + end)
11.99 + else
11.100 + raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
11.101 + | zip (thmname::_) (DeltaEntry _ :: _) =
11.102 + raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
11.103 + fun zip' xs (History ys) =
11.104 + let
11.105 + val _ = writeln ("length of xs: "^(string_of_int (length xs)))
11.106 + val _ = writeln ("length of history: "^(string_of_int (length ys)))
11.107 + in
11.108 + zip xs ys
11.109 + end
11.110 + fun replay_fact thmname thy =
11.111 let
11.112 val prf = mk_proof PDisk
11.113 val _ = set_disk_info_of prf thyname thmname
11.114 @@ -323,7 +398,10 @@
11.115 in
11.116 p
11.117 end
11.118 - val res_thy = Library.foldl replay_fact (thy,thmnames)
11.119 + fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
11.120 + val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
11.121 + val _ = ImportRecorder.set_history (History (map ThmEntry cached))
11.122 + val res_thy = fold replay_fact normal (fold replay_cache cached thy)
11.123 in
11.124 res_thy
11.125 end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/Import/xml.ML Wed Feb 15 23:57:06 2006 +0100
12.3 @@ -0,0 +1,159 @@
12.4 +(* Title: Pure/General/xml.ML
12.5 + ID: $Id$
12.6 + Author: David Aspinall, Stefan Berghofer and Markus Wenzel
12.7 +
12.8 +Basic support for XML.
12.9 +*)
12.10 +
12.11 +signature XML =
12.12 +sig
12.13 + val header: string
12.14 + val text: string -> string
12.15 + val text_charref: string -> string
12.16 + val cdata: string -> string
12.17 + val element: string -> (string * string) list -> string list -> string
12.18 + datatype tree =
12.19 + Elem of string * (string * string) list * tree list
12.20 + | Text of string
12.21 + val string_of_tree: tree -> string
12.22 + val tree_of_string: string -> tree
12.23 +end;
12.24 +
12.25 +structure XML =
12.26 +struct
12.27 +
12.28 +structure Scan = LazyScan
12.29 +open Scan
12.30 +
12.31 +(** string based representation (small scale) **)
12.32 +
12.33 +val header = "<?xml version=\"1.0\"?>\n";
12.34 +
12.35 +
12.36 +(* text and character data *)
12.37 +
12.38 +fun decode "<" = "<"
12.39 + | decode ">" = ">"
12.40 + | decode "&" = "&"
12.41 + | decode "'" = "'"
12.42 + | decode """ = "\""
12.43 + | decode c = c;
12.44 +
12.45 +fun encode "<" = "<"
12.46 + | encode ">" = ">"
12.47 + | encode "&" = "&"
12.48 + | encode "'" = "'"
12.49 + | encode "\"" = """
12.50 + | encode c = c;
12.51 +
12.52 +fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
12.53 +
12.54 +val text = Library.translate_string encode
12.55 +
12.56 +val text_charref = translate_string encode_charref;
12.57 +
12.58 +val cdata = enclose "<![CDATA[" "]]>\n"
12.59 +
12.60 +(* elements *)
12.61 +
12.62 +fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
12.63 +
12.64 +fun element name atts cs =
12.65 + let val elem = space_implode " " (name :: map attribute atts) in
12.66 + if null cs then enclose "<" "/>" elem
12.67 + else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
12.68 + end;
12.69 +
12.70 +(** explicit XML trees **)
12.71 +
12.72 +datatype tree =
12.73 + Elem of string * (string * string) list * tree list
12.74 + | Text of string;
12.75 +
12.76 +fun string_of_tree tree =
12.77 + let
12.78 + fun string_of (Elem (name, atts, ts)) buf =
12.79 + let val buf' =
12.80 + buf |> Buffer.add "<"
12.81 + |> fold Buffer.add (separate " " (name :: map attribute atts))
12.82 + in
12.83 + if null ts then
12.84 + buf' |> Buffer.add "/>"
12.85 + else
12.86 + buf' |> Buffer.add ">"
12.87 + |> fold string_of ts
12.88 + |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
12.89 + end
12.90 + | string_of (Text s) buf = Buffer.add (text s) buf;
12.91 + in Buffer.content (string_of tree Buffer.empty) end;
12.92 +
12.93 +(** XML parsing **)
12.94 +
12.95 +fun beginning n xs = Symbol.beginning n (LazySeq.take_at_most (xs, n))
12.96 +
12.97 +fun err s xs =
12.98 + "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
12.99 +
12.100 +val scan_whspc = Scan.any Symbol.is_blank;
12.101 +
12.102 +val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
12.103 +
12.104 +val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
12.105 + (scan_special || Scan.one Symbol.not_eof)) >> implode;
12.106 +
12.107 +val parse_cdata = Scan.this_string "<![CDATA[" |--
12.108 + (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
12.109 + implode) --| Scan.this_string "]]>";
12.110 +
12.111 +val parse_att =
12.112 + scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
12.113 + (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
12.114 + (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
12.115 +
12.116 +val parse_comment = Scan.this_string "<!--" --
12.117 + Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
12.118 + Scan.this_string "-->";
12.119 +
12.120 +val scan_comment_whspc =
12.121 + (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
12.122 +
12.123 +val parse_pi = Scan.this_string "<?" |--
12.124 + Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
12.125 + Scan.this_string "?>";
12.126 +
12.127 +fun parse_content xs =
12.128 + ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
12.129 + (Scan.repeat ((* scan_whspc |-- *)
12.130 + ( parse_elem >> single
12.131 + || parse_cdata >> (single o Text)
12.132 + || parse_pi >> K []
12.133 + || parse_comment >> K []) --
12.134 + Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
12.135 + >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs
12.136 +
12.137 +and parse_elem xs =
12.138 + ($$ "<" |-- scan_id --
12.139 + Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
12.140 + !! (err "Expected > or />")
12.141 + (Scan.this_string "/>" >> K []
12.142 + || $$ ">" |-- parse_content --|
12.143 + !! (err ("Expected </" ^ s ^ ">"))
12.144 + (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
12.145 + (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
12.146 +
12.147 +val parse_document =
12.148 + Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
12.149 + (Scan.repeat (Scan.unless ($$ ">")
12.150 + (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
12.151 + parse_elem;
12.152 +
12.153 +fun tree_of_string s =
12.154 + let
12.155 + val seq = LazySeq.of_list (Symbol.explode s)
12.156 + val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
12.157 + val (x, toks) = scanner seq
12.158 + in
12.159 + if LazySeq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
12.160 + end
12.161 +
12.162 +end;
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/Import/xmlconv.ML Wed Feb 15 23:57:06 2006 +0100
13.3 @@ -0,0 +1,300 @@
13.4 +signature XML_CONV =
13.5 +sig
13.6 + type 'a input = XML.tree -> 'a
13.7 + type 'a output = 'a -> XML.tree
13.8 +
13.9 + exception ParseException of string
13.10 +
13.11 + val xml_of_typ: typ output
13.12 + val typ_of_xml: typ input
13.13 +
13.14 + val xml_of_term: term output
13.15 + val term_of_xml : term input
13.16 +
13.17 + val xml_of_mixfix: mixfix output
13.18 + val mixfix_of_xml: mixfix input
13.19 +
13.20 + val xml_of_proof: Proofterm.proof output
13.21 +
13.22 + val xml_of_bool: bool output
13.23 + val bool_of_xml: bool input
13.24 +
13.25 + val xml_of_int: int output
13.26 + val int_of_xml: int input
13.27 +
13.28 + val xml_of_string: string output
13.29 + val string_of_xml: string input
13.30 +
13.31 + val xml_of_list: 'a output -> 'a list output
13.32 + val list_of_xml: 'a input -> 'a list input
13.33 +
13.34 + val xml_of_tuple : 'a output -> 'a list output
13.35 + val tuple_of_xml: 'a input -> int -> 'a list input
13.36 +
13.37 + val xml_of_option: 'a output -> 'a option output
13.38 + val option_of_xml: 'a input -> 'a option input
13.39 +
13.40 + val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
13.41 + val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
13.42 +
13.43 + val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
13.44 + val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
13.45 +
13.46 + val xml_of_unit: unit output
13.47 + val unit_of_xml: unit input
13.48 +
13.49 + val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
13.50 + val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
13.51 +
13.52 + val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
13.53 + val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
13.54 +
13.55 + val wrap : string -> 'a output -> 'a output
13.56 + val unwrap : ('a -> 'b) -> 'a input -> 'b input
13.57 + val wrap_empty : string output
13.58 + val unwrap_empty : 'a -> 'a input
13.59 + val name_of_wrap : XML.tree -> string
13.60 +
13.61 + val write_to_file: 'a output -> string -> 'a -> unit
13.62 + val read_from_file: 'a input -> string -> 'a
13.63 +end;
13.64 +
13.65 +structure XMLConv : XML_CONV =
13.66 +struct
13.67 +
13.68 +type 'a input = XML.tree -> 'a
13.69 +type 'a output = 'a -> XML.tree
13.70 +exception ParseException of string
13.71 +
13.72 +fun parse_err s = raise ParseException s
13.73 +
13.74 +fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
13.75 +
13.76 +fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
13.77 + | class_of_xml _ = parse_err "class"
13.78 +
13.79 +fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
13.80 + ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
13.81 + map xml_of_class S)
13.82 + | xml_of_typ (TFree (s, S)) =
13.83 + XML.Elem ("TFree", [("name", s)], map xml_of_class S)
13.84 + | xml_of_typ (Type (s, Ts)) =
13.85 + XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
13.86 +
13.87 +fun intofstr s i =
13.88 + case Int.fromString i of
13.89 + NONE => parse_err (s^", invalid index: "^i)
13.90 + | SOME i => i
13.91 +
13.92 +fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
13.93 + | typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) =
13.94 + TVar ((s, intofstr "TVar" i), map class_of_xml cs)
13.95 + | typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
13.96 + | typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
13.97 + | typ_of_xml _ = parse_err "type"
13.98 +
13.99 +fun xml_of_term (Bound i) =
13.100 + XML.Elem ("Bound", [("index", string_of_int i)], [])
13.101 + | xml_of_term (Free (s, T)) =
13.102 + XML.Elem ("Free", [("name", s)], [xml_of_typ T])
13.103 + | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
13.104 + ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
13.105 + [xml_of_typ T])
13.106 + | xml_of_term (Const (s, T)) =
13.107 + XML.Elem ("Const", [("name", s)], [xml_of_typ T])
13.108 + | xml_of_term (t $ u) =
13.109 + XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
13.110 + | xml_of_term (Abs (s, T, t)) =
13.111 + XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
13.112 +
13.113 +fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
13.114 + | term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
13.115 + | term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
13.116 + | term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
13.117 + | term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
13.118 + | term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
13.119 + | term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
13.120 + | term_of_xml _ = parse_err "term"
13.121 +
13.122 +fun xml_of_opttypes NONE = []
13.123 + | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
13.124 +
13.125 +(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
13.126 +(* it can be looked up in the theorem database. Thus, it could be *)
13.127 +(* omitted from the xml representation. *)
13.128 +
13.129 +fun xml_of_proof (PBound i) =
13.130 + XML.Elem ("PBound", [("index", string_of_int i)], [])
13.131 + | xml_of_proof (Abst (s, optT, prf)) =
13.132 + XML.Elem ("Abst", [("vname", s)],
13.133 + (case optT of NONE => [] | SOME T => [xml_of_typ T]) @
13.134 + [xml_of_proof prf])
13.135 + | xml_of_proof (AbsP (s, optt, prf)) =
13.136 + XML.Elem ("AbsP", [("vname", s)],
13.137 + (case optt of NONE => [] | SOME t => [xml_of_term t]) @
13.138 + [xml_of_proof prf])
13.139 + | xml_of_proof (prf % optt) =
13.140 + XML.Elem ("Appt", [],
13.141 + xml_of_proof prf ::
13.142 + (case optt of NONE => [] | SOME t => [xml_of_term t]))
13.143 + | xml_of_proof (prf %% prf') =
13.144 + XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
13.145 + | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
13.146 + | xml_of_proof (PThm ((s, _), _, t, optTs)) =
13.147 + XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
13.148 + | xml_of_proof (PAxm (s, t, optTs)) =
13.149 + XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
13.150 + | xml_of_proof (Oracle (s, t, optTs)) =
13.151 + XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
13.152 + | xml_of_proof (MinProof _) = XML.Elem ("MinProof", [], []);
13.153 +
13.154 +fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
13.155 +fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
13.156 +fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
13.157 +fun xml_of_unit () = XML.Elem ("unit", [], [])
13.158 +fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
13.159 +fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
13.160 +fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
13.161 +fun wrap s output x = XML.Elem (s, [], [output x])
13.162 +fun wrap_empty s = XML.Elem (s, [], [])
13.163 +fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
13.164 +fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
13.165 +fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) =
13.166 + XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
13.167 +fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) =
13.168 + XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
13.169 +
13.170 +fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
13.171 + | bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
13.172 + | bool_of_xml _ = parse_err "bool"
13.173 +
13.174 +fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
13.175 + | int_of_xml _ = parse_err "int"
13.176 +
13.177 +fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
13.178 + | unit_of_xml _ = parse_err "unit"
13.179 +
13.180 +fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
13.181 + | list_of_xml _ _ = parse_err "list"
13.182 +
13.183 +fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) =
13.184 + if i = length ls then map input ls else parse_err "tuple"
13.185 + | tuple_of_xml _ _ _ = parse_err "tuple"
13.186 +
13.187 +fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
13.188 + | option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
13.189 + | option_of_xml _ _ = parse_err "option"
13.190 +
13.191 +fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
13.192 + | pair_of_xml _ _ _ = parse_err "pair"
13.193 +
13.194 +fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
13.195 + | triple_of_xml _ _ _ _ = parse_err "triple"
13.196 +
13.197 +fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) =
13.198 + (input1 x1, input2 x2, input3 x3, input4 x4)
13.199 + | quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
13.200 +
13.201 +fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) =
13.202 + (input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
13.203 + | quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
13.204 +
13.205 +fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
13.206 + | unwrap _ _ _ = parse_err "unwrap"
13.207 +
13.208 +fun unwrap_empty x (XML.Elem (_, [], [])) = x
13.209 + | unwrap_empty _ _ = parse_err "unwrap_unit"
13.210 +
13.211 +fun name_of_wrap (XML.Elem (name, _, _)) = name
13.212 + | name_of_wrap _ = parse_err "name_of_wrap"
13.213 +
13.214 +fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
13.215 + | string_of_xml _ = parse_err "string"
13.216 +
13.217 +fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
13.218 + | xml_of_mixfix Structure = wrap_empty "structure"
13.219 + | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
13.220 + | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
13.221 + | xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
13.222 + | xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
13.223 + | xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
13.224 + | xml_of_mixfix (Infix i) = wrap "infix" xml_of_int i
13.225 + | xml_of_mixfix (Infixl i) = wrap "infixl" xml_of_int i
13.226 + | xml_of_mixfix (Infixr i) = wrap "infixr" xml_of_int i
13.227 + | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
13.228 +
13.229 +fun mixfix_of_xml e =
13.230 + (case name_of_wrap e of
13.231 + "nosyn" => unwrap_empty NoSyn
13.232 + | "structure" => unwrap_empty Structure
13.233 + | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
13.234 + | "delimfix" => unwrap Delimfix string_of_xml
13.235 + | "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml)
13.236 + | "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)
13.237 + | "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
13.238 + | "infix" => unwrap Infix int_of_xml
13.239 + | "infixl" => unwrap Infixl int_of_xml
13.240 + | "infixr" => unwrap Infixr int_of_xml
13.241 + | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
13.242 + | _ => parse_err "mixfix"
13.243 + ) e
13.244 +
13.245 +
13.246 +fun write_to_file output fname x = File.write (Path.unpack fname) (XML.string_of_tree (output x))
13.247 +
13.248 +fun read_from_file input fname =
13.249 + let
13.250 + val _ = writeln "read_from_file enter"
13.251 + val s = File.read (Path.unpack fname)
13.252 + val _ = writeln "done: read file"
13.253 + val tree = timeit (fn () => XML.tree_of_string s)
13.254 + val _ = writeln "done: tree"
13.255 + val x = timeit (fn () => input tree)
13.256 + val _ = writeln "done: input"
13.257 + in
13.258 + x
13.259 + end
13.260 +
13.261 +end;
13.262 +
13.263 +structure XMLConvOutput =
13.264 +struct
13.265 +open XMLConv
13.266 +
13.267 +val typ = xml_of_typ
13.268 +val term = xml_of_term
13.269 +val mixfix = xml_of_mixfix
13.270 +val proof = xml_of_proof
13.271 +val bool = xml_of_bool
13.272 +val int = xml_of_int
13.273 +val string = xml_of_string
13.274 +val unit = xml_of_unit
13.275 +val list = xml_of_list
13.276 +val pair = xml_of_pair
13.277 +val option = xml_of_option
13.278 +val triple = xml_of_triple
13.279 +val quadruple = xml_of_quadruple
13.280 +val quintuple = xml_of_quintuple
13.281 +
13.282 +end
13.283 +
13.284 +structure XMLConvInput =
13.285 +struct
13.286 +open XMLConv
13.287 +
13.288 +val typ = typ_of_xml
13.289 +val term = term_of_xml
13.290 +val mixfix = mixfix_of_xml
13.291 +val bool = bool_of_xml
13.292 +val int = int_of_xml
13.293 +val string = string_of_xml
13.294 +val unit = unit_of_xml
13.295 +val list = list_of_xml
13.296 +val pair = pair_of_xml
13.297 +val option = option_of_xml
13.298 +val triple = triple_of_xml
13.299 +val quadruple = quadruple_of_xml
13.300 +val quintuple = quintuple_of_xml
13.301 +
13.302 +end
13.303 +