HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
1.1 --- a/src/HOL/Import/HOL4Setup.thy Wed Jul 20 08:46:17 2011 +0200
1.2 +++ b/src/HOL/Import/HOL4Setup.thy Wed Jul 20 10:11:08 2011 +0200
1.3 @@ -2,7 +2,7 @@
1.4 Author: Sebastian Skalberg (TU Muenchen)
1.5 *)
1.6
1.7 -theory HOL4Setup imports MakeEqual ImportRecorder
1.8 +theory HOL4Setup imports MakeEqual
1.9 uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import.ML") begin
1.10
1.11 section {* General Setup *}
2.1 --- a/src/HOL/Import/HOLLight/hollight.imp Wed Jul 20 08:46:17 2011 +0200
2.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Wed Jul 20 10:11:08 2011 +0200
2.3 @@ -1273,9 +1273,9 @@
2.4 "NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
2.5 "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
2.6 "NSUM_0" > "HOLLight.hollight.NSUM_0"
2.7 - "NOT_UNIV_PSUBSET" > "Complete_Lattice.complete_lattice_class.not_top_less"
2.8 + "NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
2.9 "NOT_SUC" > "Nat.Suc_not_Zero"
2.10 - "NOT_PSUBSET_EMPTY" > "Complete_Lattice.complete_lattice_class.not_less_bot"
2.11 + "NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
2.12 "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
2.13 "NOT_LT" > "Orderings.linorder_class.not_less"
2.14 "NOT_LE" > "Orderings.linorder_class.not_le"
2.15 @@ -1644,7 +1644,7 @@
2.16 "IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
2.17 "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
2.18 "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
2.19 - "IMAGE_ID" > "Fun.image_ident"
2.20 + "IMAGE_ID" > "Set.image_ident"
2.21 "IMAGE_I" > "Fun.image_id"
2.22 "IMAGE_EQ_EMPTY" > "Set.image_is_empty"
2.23 "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
3.1 --- a/src/HOL/Import/ImportRecorder.thy Wed Jul 20 08:46:17 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,4 +0,0 @@
3.4 -theory ImportRecorder imports Main
3.5 -uses "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
3.6 -begin
3.7 -end
3.8 \ No newline at end of file
4.1 --- a/src/HOL/Import/import_syntax.ML Wed Jul 20 08:46:17 2011 +0200
4.2 +++ b/src/HOL/Import/import_syntax.ML Wed Jul 20 10:11:08 2011 +0200
4.3 @@ -19,9 +19,6 @@
4.4 val const_moves : (theory -> theory) parser
4.5 val const_renames : (theory -> theory) parser
4.6
4.7 - val skip_import_dir : (theory -> theory) parser
4.8 - val skip_import : (theory -> theory) parser
4.9 -
4.10 val setup : unit -> unit
4.11 end
4.12
4.13 @@ -39,13 +36,6 @@
4.14 |> Sign.add_path thyname
4.15 |> add_dump (";setup_theory " ^ thyname))
4.16
4.17 -fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
4.18 -val skip_import_dir = Parse.string >> do_skip_import_dir
4.19 -
4.20 -val lower = String.map Char.toLower
4.21 -fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
4.22 -val skip_import = Parse.short_ident >> do_skip_import
4.23 -
4.24 fun end_import toks =
4.25 Scan.succeed
4.26 (fn thy =>
4.27 @@ -54,16 +44,7 @@
4.28 val segname = get_import_segment thy
4.29 val (int_thms,facts) = Replay.setup_int_thms thyname thy
4.30 val thmnames = filter_out (should_ignore thyname thy) facts
4.31 - fun replay thy =
4.32 - let
4.33 - val _ = ImportRecorder.load_history thyname
4.34 - val thy = Replay.import_thms thyname int_thms thmnames thy
4.35 - (*handle x => (ImportRecorder.save_history thyname; raise x)*) (* FIXME avoid handle x ?? *)
4.36 - val _ = ImportRecorder.save_history thyname
4.37 - val _ = ImportRecorder.clear_history ()
4.38 - in
4.39 - thy
4.40 - end
4.41 + fun replay thy = Replay.import_thms thyname int_thms thmnames thy
4.42 in
4.43 thy |> clear_import_thy
4.44 |> set_segment thyname segname
4.45 @@ -225,12 +206,6 @@
4.46 Outer_Syntax.command "end_import"
4.47 "End HOL4 import"
4.48 Keyword.thy_decl (end_import >> Toplevel.theory);
4.49 - Outer_Syntax.command "skip_import_dir"
4.50 - "Sets caching directory for skipping importing"
4.51 - Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
4.52 - Outer_Syntax.command "skip_import"
4.53 - "Switches skipping importing on or off"
4.54 - Keyword.thy_decl (skip_import >> Toplevel.theory);
4.55 Outer_Syntax.command "setup_theory"
4.56 "Setup HOL4 theory replaying"
4.57 Keyword.thy_decl (setup_theory >> Toplevel.theory);
5.1 --- a/src/HOL/Import/importrecorder.ML Wed Jul 20 08:46:17 2011 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,265 +0,0 @@
5.4 -signature IMPORT_RECORDER =
5.5 -sig
5.6 -
5.7 - datatype deltastate = Consts of (string * typ * mixfix) list
5.8 - | Specification of (string * string * bool) list * term
5.9 - | Hol_mapping of string * string * string
5.10 - | Hol_pending of string * string * term
5.11 - | Hol_const_mapping of string * string * string
5.12 - | Hol_move of string * string
5.13 - | Defs of string * term
5.14 - | Hol_theorem of string * string * term
5.15 - | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
5.16 - | Hol_type_mapping of string * string * string
5.17 - | Indexed_theorem of int * term
5.18 - | Protect_varname of string * string
5.19 - | Dump of string
5.20 -
5.21 - datatype history = History of history_entry list
5.22 - and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
5.23 -
5.24 - val get_history : unit -> history
5.25 - val set_history : history -> unit
5.26 - val clear_history : unit -> unit
5.27 -
5.28 - val start_replay_proof : string -> string -> unit
5.29 - val stop_replay_proof : string -> string -> unit
5.30 - val abort_replay_proof : string -> string -> unit
5.31 -
5.32 - val add_consts : (string * typ * mixfix) list -> unit
5.33 - val add_specification : (string * string * bool) list -> thm -> unit
5.34 - val add_hol_mapping : string -> string -> string -> unit
5.35 - val add_hol_pending : string -> string -> thm -> unit
5.36 - val add_hol_const_mapping : string -> string -> string -> unit
5.37 - val add_hol_move : string -> string -> unit
5.38 - val add_defs : string -> term -> unit
5.39 - val add_hol_theorem : string -> string -> thm -> unit
5.40 - val add_typedef : string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
5.41 - val add_hol_type_mapping : string -> string -> string -> unit
5.42 - val add_indexed_theorem : int -> thm -> unit
5.43 - val protect_varname : string -> string -> unit
5.44 - val add_dump : string -> unit
5.45 -
5.46 - val set_skip_import_dir : string option -> unit
5.47 - val get_skip_import_dir : unit -> string option
5.48 -
5.49 - val set_skip_import : bool -> unit
5.50 - val get_skip_import : unit -> bool
5.51 -
5.52 - val save_history : string -> unit
5.53 - val load_history : string -> unit
5.54 -end
5.55 -
5.56 -structure ImportRecorder :> IMPORT_RECORDER =
5.57 -struct
5.58 -
5.59 -datatype deltastate = Consts of (string * typ * mixfix) list
5.60 - | Specification of (string * string * bool) list * term
5.61 - | Hol_mapping of string * string * string
5.62 - | Hol_pending of string * string * term
5.63 - | Hol_const_mapping of string * string * string
5.64 - | Hol_move of string * string
5.65 - | Defs of string * term
5.66 - | Hol_theorem of string * string * term
5.67 - | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
5.68 - | Hol_type_mapping of string * string * string
5.69 - | Indexed_theorem of int * term
5.70 - | Protect_varname of string * string
5.71 - | Dump of string
5.72 -
5.73 -datatype history_entry = StartReplay of string*string
5.74 - | StopReplay of string*string
5.75 - | AbortReplay of string*string
5.76 - | Delta of deltastate list
5.77 -
5.78 -val history = Unsynchronized.ref ([]:history_entry list)
5.79 -val history_dir = Unsynchronized.ref (SOME "")
5.80 -val skip_imports = Unsynchronized.ref false
5.81 -
5.82 -fun set_skip_import b = skip_imports := b
5.83 -fun get_skip_import () = !skip_imports
5.84 -
5.85 -fun clear_history () = history := []
5.86 -
5.87 -fun add_delta d = history := (case !history of (Delta ds)::hs => (Delta (d::ds))::hs | hs => (Delta [d])::hs)
5.88 -fun add_replay r = history := (r :: (!history))
5.89 -
5.90 -local
5.91 - open XMLConvOutput
5.92 - val consts = list (triple string typ mixfix)
5.93 - val specification = pair (list (triple string string bool)) term
5.94 - val hol_mapping = triple string string string
5.95 - val hol_pending = triple string string term
5.96 - val hol_const_mapping = triple string string string
5.97 - val hol_move = pair string string
5.98 - val defs = pair string term
5.99 - val hol_theorem = triple string string term
5.100 - val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
5.101 - val hol_type_mapping = triple string string string
5.102 - val indexed_theorem = pair int term
5.103 - val entry = pair string string
5.104 -
5.105 - fun delta (Consts args) = wrap "consts" consts args
5.106 - | delta (Specification args) = wrap "specification" specification args
5.107 - | delta (Hol_mapping args) = wrap "hol_mapping" hol_mapping args
5.108 - | delta (Hol_pending args) = wrap "hol_pending" hol_pending args
5.109 - | delta (Hol_const_mapping args) = wrap "hol_const_mapping" hol_const_mapping args
5.110 - | delta (Hol_move args) = wrap "hol_move" hol_move args
5.111 - | delta (Defs args) = wrap "defs" defs args
5.112 - | delta (Hol_theorem args) = wrap "hol_theorem" hol_theorem args
5.113 - | delta (Typedef args) = wrap "typedef" typedef args
5.114 - | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
5.115 - | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
5.116 - | delta (Protect_varname args) = wrap "protect_varname" entry args
5.117 - | delta (Dump args) = wrap "dump" string args
5.118 -
5.119 - fun history_entry (StartReplay args) = wrap "startreplay" entry args
5.120 - | history_entry (StopReplay args) = wrap "stopreplay" entry args
5.121 - | history_entry (AbortReplay args) = wrap "abortreplay" entry args
5.122 - | history_entry (Delta args) = wrap "delta" (list delta) args
5.123 -in
5.124 -
5.125 -val xml_of_history = list history_entry
5.126 -
5.127 -end
5.128 -
5.129 -local
5.130 - open XMLConvInput
5.131 - val consts = list (triple string typ mixfix)
5.132 - val specification = pair (list (triple string string bool)) term
5.133 - val hol_mapping = triple string string string
5.134 - val hol_pending = triple string string term
5.135 - val hol_const_mapping = triple string string string
5.136 - val hol_move = pair string string
5.137 - val defs = pair string term
5.138 - val hol_theorem = triple string string term
5.139 - val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
5.140 - val hol_type_mapping = triple string string string
5.141 - val indexed_theorem = pair int term
5.142 - val entry = pair string string
5.143 -
5.144 - fun delta "consts" = unwrap Consts consts
5.145 - | delta "specification" = unwrap Specification specification
5.146 - | delta "hol_mapping" = unwrap Hol_mapping hol_mapping
5.147 - | delta "hol_pending" = unwrap Hol_pending hol_pending
5.148 - | delta "hol_const_mapping" = unwrap Hol_const_mapping hol_const_mapping
5.149 - | delta "hol_move" = unwrap Hol_move hol_move
5.150 - | delta "defs" = unwrap Defs defs
5.151 - | delta "hol_theorem" = unwrap Hol_theorem hol_theorem
5.152 - | delta "typedef" = unwrap Typedef typedef
5.153 - | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
5.154 - | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
5.155 - | delta "protect_varname" = unwrap Protect_varname entry
5.156 - | delta "dump" = unwrap Dump string
5.157 - | delta _ = raise ParseException "delta"
5.158 -
5.159 - val delta = fn e => delta (name_of_wrap e) e
5.160 -
5.161 - fun history_entry "startreplay" = unwrap StartReplay entry
5.162 - | history_entry "stopreplay" = unwrap StopReplay entry
5.163 - | history_entry "abortreplay" = unwrap AbortReplay entry
5.164 - | history_entry "delta" = unwrap Delta (list delta)
5.165 - | history_entry _ = raise ParseException "history_entry"
5.166 -
5.167 - val history_entry = fn e => history_entry (name_of_wrap e) e
5.168 -in
5.169 -
5.170 -val history_of_xml = list history_entry
5.171 -
5.172 -end
5.173 -
5.174 -fun start_replay_proof thyname thmname = add_replay (StartReplay (thyname, thmname))
5.175 -fun stop_replay_proof thyname thmname = add_replay (StopReplay (thyname, thmname))
5.176 -fun abort_replay_proof thyname thmname = add_replay (AbortReplay (thyname, thmname))
5.177 -fun add_hol_theorem thyname thmname thm = add_delta (Hol_theorem (thyname, thmname, prop_of thm))
5.178 -fun add_hol_mapping thyname thmname isaname = add_delta (Hol_mapping (thyname, thmname, isaname))
5.179 -fun add_consts consts = add_delta (Consts consts)
5.180 -fun add_typedef thmname_opt typ c absrep_opt th = add_delta (Typedef (thmname_opt, typ, c, absrep_opt, prop_of th))
5.181 -fun add_defs thmname eq = add_delta (Defs (thmname, eq))
5.182 -fun add_hol_const_mapping thyname constname fullcname = add_delta (Hol_const_mapping (thyname, constname, fullcname))
5.183 -fun add_hol_move fullname moved_thmname = add_delta (Hol_move (fullname, moved_thmname))
5.184 -fun add_hol_type_mapping thyname tycname fulltyname = add_delta (Hol_type_mapping (thyname, tycname, fulltyname))
5.185 -fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
5.186 -fun add_specification names th = add_delta (Specification (names, prop_of th))
5.187 -fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
5.188 -fun protect_varname s t = add_delta (Protect_varname (s,t))
5.189 -fun add_dump s = add_delta (Dump s)
5.190 -
5.191 -fun set_skip_import_dir dir = (history_dir := dir)
5.192 -fun get_skip_import_dir () = !history_dir
5.193 -
5.194 -fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
5.195 -
5.196 -fun save_history thyname =
5.197 - if get_skip_import () then
5.198 - XMLConv.write_to_file xml_of_history (get_filename thyname) (!history)
5.199 - else
5.200 - ()
5.201 -
5.202 -fun load_history thyname =
5.203 - if get_skip_import () then
5.204 - let
5.205 - val filename = get_filename thyname
5.206 - val _ = writeln "load_history / before"
5.207 - val _ =
5.208 - if File.exists (Path.explode filename) then
5.209 - (history := XMLConv.read_from_file history_of_xml (get_filename thyname))
5.210 - else
5.211 - clear_history ()
5.212 - val _ = writeln "load_history / after"
5.213 - in
5.214 - ()
5.215 - end
5.216 - else
5.217 - ()
5.218 -
5.219 -
5.220 -datatype history = History of history_entry list
5.221 - and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
5.222 -
5.223 -exception CONV
5.224 -
5.225 -fun conv_histories ((StartReplay (thyname, thmname))::rest) =
5.226 - let
5.227 - val (hs, rest) = conv_histories rest
5.228 - fun continue thyname' thmname' aborted rest =
5.229 - if thyname = thyname' andalso thmname = thmname' then
5.230 - let
5.231 - val (hs', rest) = conv_histories rest
5.232 - in
5.233 - ((ThmEntry (thyname, thmname, aborted, History hs))::hs', rest)
5.234 - end
5.235 - else
5.236 - raise CONV
5.237 - in
5.238 - case rest of
5.239 - (StopReplay (thyname',thmname'))::rest =>
5.240 - continue thyname' thmname' false rest
5.241 - | (AbortReplay (thyname',thmname'))::rest =>
5.242 - continue thyname' thmname' true rest
5.243 - | [] => (hs, [])
5.244 - | _ => raise CONV
5.245 - end
5.246 - | conv_histories ((Delta ds)::rest) = (conv_histories rest) |>> (fn hs => (DeltaEntry (rev ds))::hs)
5.247 - | conv_histories rest = ([], rest)
5.248 -
5.249 -fun conv es =
5.250 - let
5.251 - val (h, rest) = conv_histories (rev es)
5.252 - in
5.253 - case rest of
5.254 - [] => h
5.255 - | _ => raise CONV
5.256 - end
5.257 -
5.258 -fun get_history () = History (conv (!history))
5.259 -
5.260 -fun reconv (History hs) rs = fold reconv_entry hs rs
5.261 -and reconv_entry (ThmEntry (thyname, thmname, aborted, h)) rs =
5.262 - ((if aborted then AbortReplay else StopReplay) (thyname, thmname)) :: (reconv h ((StartReplay (thyname, thmname))::rs))
5.263 - | reconv_entry (DeltaEntry ds) rs = (Delta (rev ds))::rs
5.264 -
5.265 -fun set_history h = history := reconv h []
5.266 -
5.267 -
5.268 -end
6.1 --- a/src/HOL/Import/lazy_seq.ML Wed Jul 20 08:46:17 2011 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,551 +0,0 @@
6.4 -(* Title: HOL/Import/lazy_seq.ML
6.5 - Author: Sebastian Skalberg, TU Muenchen
6.6 -
6.7 -Alternative version of lazy sequences.
6.8 -*)
6.9 -
6.10 -signature LAZY_SEQ =
6.11 -sig
6.12 -
6.13 - include EXTENDED_SCANNER_SEQ
6.14 -
6.15 - (* From LIST *)
6.16 -
6.17 - val fromString : string -> string seq
6.18 - val @ : 'a seq * 'a seq -> 'a seq
6.19 - val hd : 'a seq -> 'a
6.20 - val tl : 'a seq -> 'a seq
6.21 - val last : 'a seq -> 'a
6.22 - val getItem : 'a seq -> ('a * 'a seq) option
6.23 - val nth : 'a seq * int -> 'a
6.24 - val take : 'a seq * int -> 'a seq
6.25 - val drop : 'a seq * int -> 'a seq
6.26 - val rev : 'a seq -> 'a seq
6.27 - val concat : 'a seq seq -> 'a seq
6.28 - val revAppend : 'a seq * 'a seq -> 'a seq
6.29 - val app : ('a -> unit) -> 'a seq -> unit
6.30 - val map : ('a -> 'b) -> 'a seq -> 'b seq
6.31 - val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
6.32 - val find : ('a -> bool) -> 'a seq -> 'a option
6.33 - val filter : ('a -> bool) -> 'a seq -> 'a seq
6.34 - val partition : ('a -> bool)
6.35 - -> 'a seq -> 'a seq * 'a seq
6.36 - val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
6.37 - val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
6.38 - val exists : ('a -> bool) -> 'a seq -> bool
6.39 - val all : ('a -> bool) -> 'a seq -> bool
6.40 - val tabulate : int * (int -> 'a) -> 'a seq
6.41 - val collate : ('a * 'a -> order)
6.42 - -> 'a seq * 'a seq -> order
6.43 -
6.44 - (* Miscellaneous *)
6.45 -
6.46 - val cycle : ((unit ->'a seq) -> 'a seq) -> 'a seq
6.47 - val iterates : ('a -> 'a) -> 'a -> 'a seq
6.48 - val of_function: (unit -> 'a option) -> 'a seq
6.49 - val of_string : string -> char seq
6.50 - val of_instream: TextIO.instream -> char seq
6.51 -
6.52 - (* From SEQ *)
6.53 -
6.54 - val make: (unit -> ('a * 'a seq) option) -> 'a seq
6.55 - val empty: 'a -> 'a seq
6.56 - val cons: 'a * 'a seq -> 'a seq
6.57 - val single: 'a -> 'a seq
6.58 - val try: ('a -> 'b) -> 'a -> 'b seq
6.59 - val chop: int * 'a seq -> 'a list * 'a seq
6.60 - val list_of: 'a seq -> 'a list
6.61 - val of_list: 'a list -> 'a seq
6.62 - val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
6.63 - val interleave: 'a seq * 'a seq -> 'a seq
6.64 - val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
6.65 - val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
6.66 - val commute: 'a seq list -> 'a list seq
6.67 - val succeed: 'a -> 'a seq
6.68 - val fail: 'a -> 'b seq
6.69 - val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
6.70 - val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
6.71 - val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
6.72 - val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
6.73 - val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
6.74 - val TRY: ('a -> 'a seq) -> 'a -> 'a seq
6.75 - val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
6.76 - val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
6.77 - val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
6.78 - val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
6.79 -
6.80 -end
6.81 -
6.82 -structure LazySeq :> LAZY_SEQ =
6.83 -struct
6.84 -
6.85 -datatype 'a seq = Seq of ('a * 'a seq) option lazy
6.86 -
6.87 -exception Empty
6.88 -
6.89 -fun getItem (Seq s) = Lazy.force s
6.90 -val pull = getItem
6.91 -fun make f = Seq (Lazy.lazy f)
6.92 -
6.93 -fun null s = is_none (getItem s)
6.94 -
6.95 -local
6.96 - fun F n NONE = n
6.97 - | F n (SOME(_,s)) = F (n+1) (getItem s)
6.98 -in
6.99 -fun length s = F 0 (getItem s)
6.100 -end
6.101 -
6.102 -fun s1 @ s2 =
6.103 - let
6.104 - fun F NONE = getItem s2
6.105 - | F (SOME(x,s1')) = SOME(x,F' s1')
6.106 - and F' s = make (fn () => F (getItem s))
6.107 - in
6.108 - F' s1
6.109 - end
6.110 -
6.111 -local
6.112 - fun F NONE = raise Empty
6.113 - | F (SOME arg) = arg
6.114 -in
6.115 -fun hd s = #1 (F (getItem s))
6.116 -fun tl s = #2 (F (getItem s))
6.117 -end
6.118 -
6.119 -local
6.120 - fun F x NONE = x
6.121 - | F _ (SOME(x,s)) = F x (getItem s)
6.122 - fun G NONE = raise Empty
6.123 - | G (SOME(x,s)) = F x (getItem s)
6.124 -in
6.125 -fun last s = G (getItem s)
6.126 -end
6.127 -
6.128 -local
6.129 - fun F NONE _ = raise Subscript
6.130 - | F (SOME(x,_)) 0 = x
6.131 - | F (SOME(_,s)) n = F (getItem s) (n-1)
6.132 -in
6.133 -fun nth(s,n) =
6.134 - if n < 0
6.135 - then raise Subscript
6.136 - else F (getItem s) n
6.137 -end
6.138 -
6.139 -local
6.140 - fun F NONE _ = raise Subscript
6.141 - | F (SOME(x,s)) n = SOME(x,F' s (n-1))
6.142 - and F' s 0 = Seq (Lazy.value NONE)
6.143 - | F' s n = make (fn () => F (getItem s) n)
6.144 -in
6.145 -fun take (s,n) =
6.146 - if n < 0
6.147 - then raise Subscript
6.148 - else F' s n
6.149 -end
6.150 -
6.151 -fun take_at_most s n =
6.152 - if n <= 0 then [] else
6.153 - case getItem s of
6.154 - NONE => []
6.155 - | SOME (x,s') => x::(take_at_most s' (n-1))
6.156 -
6.157 -local
6.158 - fun F s 0 = s
6.159 - | F NONE _ = raise Subscript
6.160 - | F (SOME(_,s)) n = F (getItem s) (n-1)
6.161 -in
6.162 -fun drop (s,0) = s
6.163 - | drop (s,n) =
6.164 - if n < 0
6.165 - then raise Subscript
6.166 - else make (fn () => F (getItem s) n)
6.167 -end
6.168 -
6.169 -local
6.170 - fun F s NONE = s
6.171 - | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
6.172 -in
6.173 -fun rev s = make (fn () => F NONE (getItem s))
6.174 -end
6.175 -
6.176 -local
6.177 - fun F s NONE = getItem s
6.178 - | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
6.179 -in
6.180 -fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
6.181 -end
6.182 -
6.183 -local
6.184 - fun F NONE = NONE
6.185 - | F (SOME(s1,s2)) =
6.186 - let
6.187 - fun G NONE = F (getItem s2)
6.188 - | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
6.189 - in
6.190 - G (getItem s1)
6.191 - end
6.192 -in
6.193 -fun concat s = make (fn () => F (getItem s))
6.194 -end
6.195 -
6.196 -fun app f =
6.197 - let
6.198 - fun F NONE = ()
6.199 - | F (SOME(x,s)) =
6.200 - (f x;
6.201 - F (getItem s))
6.202 - in
6.203 - F o getItem
6.204 - end
6.205 -
6.206 -fun map f =
6.207 - let
6.208 - fun F NONE = NONE
6.209 - | F (SOME(x,s)) = SOME(f x,F' s)
6.210 - and F' s = make (fn() => F (getItem s))
6.211 - in
6.212 - F'
6.213 - end
6.214 -
6.215 -fun mapPartial f =
6.216 - let
6.217 - fun F NONE = NONE
6.218 - | F (SOME(x,s)) =
6.219 - (case f x of
6.220 - SOME y => SOME(y,F' s)
6.221 - | NONE => F (getItem s))
6.222 - and F' s = make (fn()=> F (getItem s))
6.223 - in
6.224 - F'
6.225 - end
6.226 -
6.227 -fun find P =
6.228 - let
6.229 - fun F NONE = NONE
6.230 - | F (SOME(x,s)) =
6.231 - if P x
6.232 - then SOME x
6.233 - else F (getItem s)
6.234 - in
6.235 - F o getItem
6.236 - end
6.237 -
6.238 -(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
6.239 -
6.240 -fun filter P =
6.241 - let
6.242 - fun F NONE = NONE
6.243 - | F (SOME(x,s)) =
6.244 - if P x
6.245 - then SOME(x,F' s)
6.246 - else F (getItem s)
6.247 - and F' s = make (fn () => F (getItem s))
6.248 - in
6.249 - F'
6.250 - end
6.251 -
6.252 -fun partition f s =
6.253 - let
6.254 - val s' = map (fn x => (x,f x)) s
6.255 - in
6.256 - (mapPartial (fn (x,true) => SOME x | _ => NONE) s',
6.257 - mapPartial (fn (x,false) => SOME x | _ => NONE) s')
6.258 - end
6.259 -
6.260 -fun exists P =
6.261 - let
6.262 - fun F NONE = false
6.263 - | F (SOME(x,s)) = P x orelse F (getItem s)
6.264 - in
6.265 - F o getItem
6.266 - end
6.267 -
6.268 -fun all P =
6.269 - let
6.270 - fun F NONE = true
6.271 - | F (SOME(x,s)) = P x andalso F (getItem s)
6.272 - in
6.273 - F o getItem
6.274 - end
6.275 -
6.276 -(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
6.277 -
6.278 -fun tabulate (n,f) =
6.279 - let
6.280 - fun F n = make (fn () => SOME(f n,F (n+1)))
6.281 - in
6.282 - F n
6.283 - end
6.284 -
6.285 -fun collate c (s1,s2) =
6.286 - let
6.287 - fun F NONE _ = LESS
6.288 - | F _ NONE = GREATER
6.289 - | F (SOME(x,s1)) (SOME(y,s2)) =
6.290 - (case c (x,y) of
6.291 - LESS => LESS
6.292 - | GREATER => GREATER
6.293 - | EQUAL => F' s1 s2)
6.294 - and F' s1 s2 = F (getItem s1) (getItem s2)
6.295 - in
6.296 - F' s1 s2
6.297 - end
6.298 -
6.299 -fun empty _ = Seq (Lazy.value NONE)
6.300 -fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
6.301 -fun cons a = Seq(Lazy.value (SOME a))
6.302 -
6.303 -fun cycle seqfn =
6.304 - let
6.305 - val knot = Unsynchronized.ref (Seq (Lazy.value NONE))
6.306 - in
6.307 - knot := seqfn (fn () => !knot);
6.308 - !knot
6.309 - end
6.310 -
6.311 -fun iterates f =
6.312 - let
6.313 - fun F x = make (fn() => SOME(x,F (f x)))
6.314 - in
6.315 - F
6.316 - end
6.317 -
6.318 -fun interleave (s1,s2) =
6.319 - let
6.320 - fun F NONE = getItem s2
6.321 - | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
6.322 - in
6.323 - make (fn()=> F (getItem s1))
6.324 - end
6.325 -
6.326 -(* val force_all = app ignore *)
6.327 -
6.328 -local
6.329 - fun F NONE = ()
6.330 - | F (SOME(x,s)) = F (getItem s)
6.331 -in
6.332 -fun force_all s = F (getItem s)
6.333 -end
6.334 -
6.335 -fun of_function f =
6.336 - let
6.337 - fun F () = case f () of
6.338 - SOME x => SOME(x,make F)
6.339 - | NONE => NONE
6.340 - in
6.341 - make F
6.342 - end
6.343 -
6.344 -local
6.345 - fun F [] = NONE
6.346 - | F (x::xs) = SOME(x,F' xs)
6.347 - and F' xs = make (fn () => F xs)
6.348 -in
6.349 -fun of_list xs = F' xs
6.350 -end
6.351 -
6.352 -val of_string = of_list o String.explode
6.353 -
6.354 -fun of_instream is =
6.355 - let
6.356 - val buffer : char list Unsynchronized.ref = Unsynchronized.ref []
6.357 - fun get_input () =
6.358 - case !buffer of
6.359 - (c::cs) => (buffer:=cs;
6.360 - SOME c)
6.361 - | [] => (case String.explode (TextIO.input is) of
6.362 - [] => NONE
6.363 - | (c::cs) => (buffer := cs;
6.364 - SOME c))
6.365 - in
6.366 - of_function get_input
6.367 - end
6.368 -
6.369 -local
6.370 - fun F k NONE = k []
6.371 - | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
6.372 -in
6.373 -fun list_of s = F (fn x => x) (getItem s)
6.374 -end
6.375 -
6.376 -(* Adapted from seq.ML *)
6.377 -
6.378 -val succeed = single
6.379 -fun fail _ = Seq (Lazy.value NONE)
6.380 -
6.381 -(* fun op THEN (f, g) x = flat (map g (f x)) *)
6.382 -
6.383 -fun op THEN (f, g) =
6.384 - let
6.385 - fun F NONE = NONE
6.386 - | F (SOME(x,xs)) =
6.387 - let
6.388 - fun G NONE = F (getItem xs)
6.389 - | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
6.390 - in
6.391 - G (getItem (g x))
6.392 - end
6.393 - in
6.394 - fn x => make (fn () => F (getItem (f x)))
6.395 - end
6.396 -
6.397 -fun op ORELSE (f, g) x =
6.398 - make (fn () =>
6.399 - case getItem (f x) of
6.400 - NONE => getItem (g x)
6.401 - | some => some)
6.402 -
6.403 -fun op APPEND (f, g) x =
6.404 - let
6.405 - fun copy s =
6.406 - case getItem s of
6.407 - NONE => getItem (g x)
6.408 - | SOME(x,xs) => SOME(x,make (fn () => copy xs))
6.409 - in
6.410 - make (fn () => copy (f x))
6.411 - end
6.412 -
6.413 -fun EVERY fs = fold_rev (curry op THEN) fs succeed
6.414 -fun FIRST fs = fold_rev (curry op ORELSE) fs fail
6.415 -
6.416 -fun TRY f x =
6.417 - make (fn () =>
6.418 - case getItem (f x) of
6.419 - NONE => SOME(x,Seq (Lazy.value NONE))
6.420 - | some => some)
6.421 -
6.422 -fun REPEAT f =
6.423 - let
6.424 - fun rep qs x =
6.425 - case getItem (f x) of
6.426 - NONE => SOME(x, make (fn () => repq qs))
6.427 - | SOME (x', q) => rep (q :: qs) x'
6.428 - and repq [] = NONE
6.429 - | repq (q :: qs) =
6.430 - case getItem q of
6.431 - NONE => repq qs
6.432 - | SOME (x, q) => rep (q :: qs) x
6.433 - in
6.434 - fn x => make (fn () => rep [] x)
6.435 - end
6.436 -
6.437 -fun REPEAT1 f = op THEN (f, REPEAT f);
6.438 -
6.439 -fun INTERVAL f i =
6.440 - let
6.441 - fun F j =
6.442 - if i > j
6.443 - then single
6.444 - else op THEN (f j, F (j - 1))
6.445 - in F end
6.446 -
6.447 -fun DETERM f x =
6.448 - make (fn () =>
6.449 - case getItem (f x) of
6.450 - NONE => NONE
6.451 - | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
6.452 -
6.453 -(*partial function as procedure*)
6.454 -fun try f x =
6.455 - make (fn () =>
6.456 - case Basics.try f x of
6.457 - SOME y => SOME(y,Seq (Lazy.value NONE))
6.458 - | NONE => NONE)
6.459 -
6.460 -(*functional to print a sequence, up to "count" elements;
6.461 - the function prelem should print the element number and also the element*)
6.462 -fun print prelem count seq =
6.463 - let
6.464 - fun pr k xq =
6.465 - if k > count
6.466 - then ()
6.467 - else
6.468 - case getItem xq of
6.469 - NONE => ()
6.470 - | SOME (x, xq') =>
6.471 - (prelem k x;
6.472 - writeln "";
6.473 - pr (k + 1) xq')
6.474 - in
6.475 - pr 1 seq
6.476 - end
6.477 -
6.478 -(*accumulating a function over a sequence; this is lazy*)
6.479 -fun it_right f (xq, yq) =
6.480 - let
6.481 - fun its s =
6.482 - make (fn () =>
6.483 - case getItem s of
6.484 - NONE => getItem yq
6.485 - | SOME (a, s') => getItem(f (a, its s')))
6.486 - in
6.487 - its xq
6.488 - end
6.489 -
6.490 -(*map over a sequence s1, append the sequence s2*)
6.491 -fun mapp f s1 s2 =
6.492 - let
6.493 - fun F NONE = getItem s2
6.494 - | F (SOME(x,s1')) = SOME(f x,F' s1')
6.495 - and F' s = make (fn () => F (getItem s))
6.496 - in
6.497 - F' s1
6.498 - end
6.499 -
6.500 -(*turn a list of sequences into a sequence of lists*)
6.501 -local
6.502 - fun F [] = SOME([],Seq (Lazy.value NONE))
6.503 - | F (xq :: xqs) =
6.504 - case getItem xq of
6.505 - NONE => NONE
6.506 - | SOME (x, xq') =>
6.507 - (case F xqs of
6.508 - NONE => NONE
6.509 - | SOME (xs, xsq) =>
6.510 - let
6.511 - fun G s =
6.512 - make (fn () =>
6.513 - case getItem s of
6.514 - NONE => F (xq' :: xqs)
6.515 - | SOME(ys,ysq) => SOME(x::ys,G ysq))
6.516 - in
6.517 - SOME (x :: xs, G xsq)
6.518 - end)
6.519 -in
6.520 -fun commute xqs = make (fn () => F xqs)
6.521 -end
6.522 -
6.523 -(*the list of the first n elements, paired with rest of sequence;
6.524 - if length of list is less than n, then sequence had less than n elements*)
6.525 -fun chop (n, xq) =
6.526 - if n <= 0
6.527 - then ([], xq)
6.528 - else
6.529 - case getItem xq of
6.530 - NONE => ([], xq)
6.531 - | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
6.532 -
6.533 -fun foldl f e s =
6.534 - let
6.535 - fun F k NONE = k e
6.536 - | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
6.537 - in
6.538 - F (fn x => x) (getItem s)
6.539 - end
6.540 -
6.541 -fun foldr f e s =
6.542 - let
6.543 - fun F e NONE = e
6.544 - | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
6.545 - in
6.546 - F e (getItem s)
6.547 - end
6.548 -
6.549 -fun fromString s = of_list (raw_explode s)
6.550 -
6.551 -end
6.552 -
6.553 -structure LazyScan = Scanner (structure Seq = LazySeq)
6.554 -
7.1 --- a/src/HOL/Import/mono_scan.ML Wed Jul 20 08:46:17 2011 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,237 +0,0 @@
7.4 -(* Title: HOL/Import/mono_scan.ML
7.5 - Author: Steven Obua, TU Muenchen
7.6 -
7.7 -Monomorphic scanner combinators for monomorphic sequences.
7.8 -*)
7.9 -
7.10 -signature MONO_SCANNER =
7.11 -sig
7.12 -
7.13 - include MONO_SCANNER_SEQ
7.14 -
7.15 - exception SyntaxError
7.16 -
7.17 - type 'a scanner = seq -> 'a * seq
7.18 -
7.19 - val :-- : 'a scanner * ('a -> 'b scanner)
7.20 - -> ('a*'b) scanner
7.21 - val -- : 'a scanner * 'b scanner -> ('a * 'b) scanner
7.22 - val >> : 'a scanner * ('a -> 'b) -> 'b scanner
7.23 - val --| : 'a scanner * 'b scanner -> 'a scanner
7.24 - val |-- : 'a scanner * 'b scanner -> 'b scanner
7.25 - val ^^ : string scanner * string scanner
7.26 - -> string scanner
7.27 - val || : 'a scanner * 'a scanner -> 'a scanner
7.28 - val one : (item -> bool) -> item scanner
7.29 - val anyone : item scanner
7.30 - val succeed : 'a -> 'a scanner
7.31 - val any : (item -> bool) -> item list scanner
7.32 - val any1 : (item -> bool) -> item list scanner
7.33 - val optional : 'a scanner -> 'a -> 'a scanner
7.34 - val option : 'a scanner -> 'a option scanner
7.35 - val repeat : 'a scanner -> 'a list scanner
7.36 - val repeat1 : 'a scanner -> 'a list scanner
7.37 - val repeat_fixed : int -> 'a scanner -> 'a list scanner
7.38 - val ahead : 'a scanner -> 'a scanner
7.39 - val unless : 'a scanner -> 'b scanner -> 'b scanner
7.40 - val !! : (seq -> string) -> 'a scanner -> 'a scanner
7.41 -
7.42 -end
7.43 -
7.44 -signature STRING_SCANNER =
7.45 -sig
7.46 -
7.47 - include MONO_SCANNER where type item = string
7.48 -
7.49 - val $$ : item -> item scanner
7.50 -
7.51 - val scan_id : string scanner
7.52 - val scan_nat : int scanner
7.53 -
7.54 - val this : item list -> item list scanner
7.55 - val this_string : string -> string scanner
7.56 -
7.57 -end
7.58 -
7.59 -functor MonoScanner (structure Seq : MONO_SCANNER_SEQ) : MONO_SCANNER =
7.60 -struct
7.61 -
7.62 -infix 7 |-- --|
7.63 -infix 5 :-- -- ^^
7.64 -infix 3 >>
7.65 -infix 0 ||
7.66 -
7.67 -exception SyntaxError
7.68 -exception Fail of string
7.69 -
7.70 -type seq = Seq.seq
7.71 -type item = Seq.item
7.72 -type 'a scanner = seq -> 'a * seq
7.73 -
7.74 -val pull = Seq.pull
7.75 -
7.76 -fun (sc1 :-- sc2) toks =
7.77 - let
7.78 - val (x,toks2) = sc1 toks
7.79 - val (y,toks3) = sc2 x toks2
7.80 - in
7.81 - ((x,y),toks3)
7.82 - end
7.83 -
7.84 -fun (sc1 -- sc2) toks =
7.85 - let
7.86 - val (x,toks2) = sc1 toks
7.87 - val (y,toks3) = sc2 toks2
7.88 - in
7.89 - ((x,y),toks3)
7.90 - end
7.91 -
7.92 -fun (sc >> f) toks =
7.93 - let
7.94 - val (x,toks2) = sc toks
7.95 - in
7.96 - (f x,toks2)
7.97 - end
7.98 -
7.99 -fun (sc1 --| sc2) toks =
7.100 - let
7.101 - val (x,toks2) = sc1 toks
7.102 - val (_,toks3) = sc2 toks2
7.103 - in
7.104 - (x,toks3)
7.105 - end
7.106 -
7.107 -fun (sc1 |-- sc2) toks =
7.108 - let
7.109 - val (_,toks2) = sc1 toks
7.110 - in
7.111 - sc2 toks2
7.112 - end
7.113 -
7.114 -fun (sc1 ^^ sc2) toks =
7.115 - let
7.116 - val (x,toks2) = sc1 toks
7.117 - val (y,toks3) = sc2 toks2
7.118 - in
7.119 - (x^y,toks3)
7.120 - end
7.121 -
7.122 -fun (sc1 || sc2) toks =
7.123 - (sc1 toks)
7.124 - handle SyntaxError => sc2 toks
7.125 -
7.126 -fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
7.127 -
7.128 -fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
7.129 -
7.130 -fun succeed e toks = (e,toks)
7.131 -
7.132 -fun any p toks =
7.133 - case pull toks of
7.134 - NONE => ([],toks)
7.135 - | SOME(x,toks2) => if p x
7.136 - then
7.137 - let
7.138 - val (xs,toks3) = any p toks2
7.139 - in
7.140 - (x::xs,toks3)
7.141 - end
7.142 - else ([],toks)
7.143 -
7.144 -fun any1 p toks =
7.145 - let
7.146 - val (x,toks2) = one p toks
7.147 - val (xs,toks3) = any p toks2
7.148 - in
7.149 - (x::xs,toks3)
7.150 - end
7.151 -
7.152 -fun optional sc def = sc || succeed def
7.153 -fun option sc = (sc >> SOME) || succeed NONE
7.154 -
7.155 -(*
7.156 -fun repeat sc =
7.157 - let
7.158 - fun R toks =
7.159 - let
7.160 - val (x,toks2) = sc toks
7.161 - val (xs,toks3) = R toks2
7.162 - in
7.163 - (x::xs,toks3)
7.164 - end
7.165 - handle SyntaxError => ([],toks)
7.166 - in
7.167 - R
7.168 - end
7.169 -*)
7.170 -
7.171 -(* A tail-recursive version of repeat. It is (ever so) slightly slower
7.172 - * than the above, non-tail-recursive version (due to the garbage generation
7.173 - * associated with the reversal of the list). However, this version will be
7.174 - * able to process input where the former version must give up (due to stack
7.175 - * overflow). The slowdown seems to be around the one percent mark.
7.176 - *)
7.177 -fun repeat sc =
7.178 - let
7.179 - fun R xs toks =
7.180 - case SOME (sc toks) handle SyntaxError => NONE of
7.181 - SOME (x,toks2) => R (x::xs) toks2
7.182 - | NONE => (List.rev xs,toks)
7.183 - in
7.184 - R []
7.185 - end
7.186 -
7.187 -fun repeat1 sc toks =
7.188 - let
7.189 - val (x,toks2) = sc toks
7.190 - val (xs,toks3) = repeat sc toks2
7.191 - in
7.192 - (x::xs,toks3)
7.193 - end
7.194 -
7.195 -fun repeat_fixed n sc =
7.196 - let
7.197 - fun R n xs toks =
7.198 - if (n <= 0) then (List.rev xs, toks)
7.199 - else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
7.200 - in
7.201 - R n []
7.202 - end
7.203 -
7.204 -fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
7.205 -
7.206 -fun unless test sc toks =
7.207 - let
7.208 - val test_failed = (test toks;false) handle SyntaxError => true
7.209 - in
7.210 - if test_failed
7.211 - then sc toks
7.212 - else raise SyntaxError
7.213 - end
7.214 -
7.215 -fun !! f sc toks = (sc toks
7.216 - handle SyntaxError => raise Fail (f toks))
7.217 -
7.218 -end
7.219 -
7.220 -
7.221 -structure StringScanner : STRING_SCANNER =
7.222 -struct
7.223 -
7.224 -structure Scan = MonoScanner(structure Seq = StringScannerSeq)
7.225 -open Scan
7.226 -
7.227 -fun $$ arg = one (fn x => x = arg)
7.228 -
7.229 -val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
7.230 -
7.231 -val nat_of_list = the o Int.fromString o implode
7.232 -
7.233 -val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list
7.234 -
7.235 -fun this [] = (fn toks => ([], toks))
7.236 - | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
7.237 -
7.238 -fun this_string s = this (raw_explode s) >> K s
7.239 -
7.240 -end
7.241 \ No newline at end of file
8.1 --- a/src/HOL/Import/mono_seq.ML Wed Jul 20 08:46:17 2011 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,76 +0,0 @@
8.4 -(* Title: HOL/Import/mono_seq.ML
8.5 - Author: Steven Obua, TU Muenchen
8.6 -
8.7 -Monomorphic sequences.
8.8 -*)
8.9 -
8.10 -(* The trouble is that signature / structures cannot depend on type variable parameters ... *)
8.11 -
8.12 -signature MONO_SCANNER_SEQ =
8.13 -sig
8.14 - type seq
8.15 - type item
8.16 -
8.17 - val pull : seq -> (item * seq) option
8.18 -end
8.19 -
8.20 -signature MONO_EXTENDED_SCANNER_SEQ =
8.21 -sig
8.22 -
8.23 - include MONO_SCANNER_SEQ
8.24 -
8.25 - val null : seq -> bool
8.26 - val length : seq -> int
8.27 - val take_at_most : seq -> int -> item list
8.28 -
8.29 -end
8.30 -
8.31 -functor MonoExtendScannerSeq (structure Seq : MONO_SCANNER_SEQ) : MONO_EXTENDED_SCANNER_SEQ =
8.32 -struct
8.33 -
8.34 -type seq = Seq.seq
8.35 -type item = Seq.item
8.36 -val pull = Seq.pull
8.37 -
8.38 -fun null s = is_none (pull s)
8.39 -
8.40 -fun take_at_most s n =
8.41 - if n <= 0 then [] else
8.42 - case pull s of
8.43 - NONE => []
8.44 - | SOME (x,s') => x::(take_at_most s' (n-1))
8.45 -
8.46 -fun length' s n =
8.47 - case pull s of
8.48 - NONE => n
8.49 - | SOME (_, s') => length' s' (n+1)
8.50 -
8.51 -fun length s = length' s 0
8.52 -
8.53 -end
8.54 -
8.55 -
8.56 -structure StringScannerSeq :
8.57 - sig
8.58 - include MONO_EXTENDED_SCANNER_SEQ
8.59 - val fromString : string -> seq
8.60 - end
8.61 - =
8.62 -struct
8.63 -
8.64 -structure Incubator : MONO_SCANNER_SEQ =
8.65 -struct
8.66 -
8.67 -type seq = string * int * int
8.68 -type item = string
8.69 -
8.70 -fun pull (s, len, i) = if i >= len then NONE else SOME (String.substring (s, i, 1), (s, len, i+1))
8.71 -end
8.72 -
8.73 -structure Extended = MonoExtendScannerSeq (structure Seq = Incubator)
8.74 -open Extended
8.75 -
8.76 -fun fromString s = (s, String.size s, 0)
8.77 -
8.78 -end
8.79 -
9.1 --- a/src/HOL/Import/proof_kernel.ML Wed Jul 20 08:46:17 2011 +0200
9.2 +++ b/src/HOL/Import/proof_kernel.ML Wed Jul 20 10:11:08 2011 +0200
9.3 @@ -129,7 +129,7 @@
9.4 fun to_hol_thm th = HOLThm ([], th)
9.5
9.6 val replay_add_dump = add_dump
9.7 -fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
9.8 +fun add_dump s thy = replay_add_dump s thy
9.9
9.10 datatype proof_info
9.11 = Info of {disk_info: (string * string) option Unsynchronized.ref}
9.12 @@ -303,85 +303,14 @@
9.13 handle PK _ => thyname)
9.14 val get_name : (string * string) list -> string = Lib.assoc "n"
9.15
9.16 -local
9.17 - open LazyScan
9.18 - infix 7 |-- --|
9.19 - infix 5 :-- -- ^^
9.20 - infix 3 >>
9.21 - infix 0 ||
9.22 -in
9.23 exception XML of string
9.24
9.25 datatype xml = Elem of string * (string * string) list * xml list
9.26 datatype XMLtype = XMLty of xml | FullType of hol_type
9.27 datatype XMLterm = XMLtm of xml | FullTerm of term
9.28
9.29 -fun pair x y = (x,y)
9.30 -
9.31 -fun scan_id toks =
9.32 - let
9.33 - val (x,toks2) = one Char.isAlpha toks
9.34 - val (xs,toks3) = any Char.isAlphaNum toks2
9.35 - in
9.36 - (String.implode (x::xs),toks3)
9.37 - end
9.38 -
9.39 -fun scan_string str c =
9.40 - let
9.41 - fun F [] toks = (c,toks)
9.42 - | F (c::cs) toks =
9.43 - case LazySeq.getItem toks of
9.44 - SOME(c',toks') =>
9.45 - if c = c'
9.46 - then F cs toks'
9.47 - else raise SyntaxError
9.48 - | NONE => raise SyntaxError
9.49 - in
9.50 - F (String.explode str)
9.51 - end
9.52 -
9.53 -local
9.54 - val scan_entity =
9.55 - (scan_string "amp;" #"&")
9.56 - || scan_string "quot;" #"\""
9.57 - || scan_string "gt;" #">"
9.58 - || scan_string "lt;" #"<"
9.59 - || scan_string "apos;" #"'"
9.60 -in
9.61 -fun scan_nonquote toks =
9.62 - case LazySeq.getItem toks of
9.63 - SOME (c,toks') =>
9.64 - (case c of
9.65 - #"\"" => raise SyntaxError
9.66 - | #"&" => scan_entity toks'
9.67 - | c => (c,toks'))
9.68 - | NONE => raise SyntaxError
9.69 -end
9.70 -
9.71 -val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
9.72 - String.implode
9.73 -
9.74 -val scan_attribute = scan_id -- $$ #"=" |-- scan_string
9.75 -
9.76 -val scan_start_of_tag = $$ #"<" |-- scan_id --
9.77 - repeat ($$ #" " |-- scan_attribute)
9.78 -
9.79 -fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
9.80 -
9.81 -val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
9.82 -
9.83 -fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
9.84 - (fn (chldr,id') => if id = id'
9.85 - then chldr
9.86 - else raise XML "Tag mismatch")
9.87 -and scan_tag toks =
9.88 - let
9.89 - val ((id,atts),toks2) = scan_start_of_tag toks
9.90 - val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
9.91 - in
9.92 - (Elem (id,atts,chldr),toks3)
9.93 - end
9.94 -end
9.95 +fun xml_to_import_xml (XML.Elem ((n, l), ts)) = Elem (n, l, map xml_to_import_xml ts)
9.96 + | xml_to_import_xml (XML.Text _) = raise XML "Incorrect proof file: text";
9.97
9.98 val type_of = Term.type_of
9.99
9.100 @@ -473,7 +402,6 @@
9.101 let
9.102 val _ = Unsynchronized.inc invented_isavar
9.103 val t = "u_" ^ string_of_int (!invented_isavar)
9.104 - val _ = ImportRecorder.protect_varname s t
9.105 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
9.106 in
9.107 t
9.108 @@ -927,7 +855,7 @@
9.109 fun import_proof_concl thyname thmname thy =
9.110 let
9.111 val is = TextIO.openIn(proof_file_name thyname thmname thy)
9.112 - val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
9.113 + val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
9.114 val _ = TextIO.closeIn is
9.115 in
9.116 case proof_xml of
9.117 @@ -948,7 +876,7 @@
9.118 fun import_proof thyname thmname thy =
9.119 let
9.120 val is = TextIO.openIn(proof_file_name thyname thmname thy)
9.121 - val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
9.122 + val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
9.123 val _ = TextIO.closeIn is
9.124 in
9.125 case proof_xml of
9.126 @@ -1292,8 +1220,6 @@
9.127 val hth as HOLThm args = mk_res th
9.128 val thy' = thy |> add_hol4_theorem thyname thmname args
9.129 |> add_hol4_mapping thyname thmname isaname
9.130 - val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
9.131 - val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
9.132 in
9.133 (thy',SOME hth)
9.134 end
9.135 @@ -1364,7 +1290,6 @@
9.136 val rew = rewrite_hol4_term (concl_of th) thy
9.137 val th = Thm.equal_elim rew th
9.138 val thy' = add_hol4_pending thyname thmname args thy
9.139 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
9.140 val th = disambiguate_frees th
9.141 val th = Object_Logic.rulify th
9.142 val thy2 =
9.143 @@ -1920,17 +1845,14 @@
9.144 val csyn = mk_syn thy constname
9.145 val thy1 = case HOL4DefThy.get thy of
9.146 Replaying _ => thy
9.147 - | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
9.148 - Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
9.149 + | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy
9.150 val eq = mk_defeq constname rhs' thy1
9.151 val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
9.152 - val _ = ImportRecorder.add_defs thmname eq
9.153 val def_thm = hd thms
9.154 val thm' = def_thm RS meta_eq_to_obj_eq_thm
9.155 val (thy',th) = (thy2, thm')
9.156 val fullcname = Sign.intern_const thy' constname
9.157 val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
9.158 - val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
9.159 val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
9.160 val rew = rewrite_hol4_term eq thy''
9.161 val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
9.162 @@ -1958,13 +1880,10 @@
9.163 | NONE => raise ERR "new_definition" "Bad conclusion"
9.164 val fullname = Sign.full_bname thy22 thmname
9.165 val thy22' = case opt_get_output_thy thy22 of
9.166 - "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
9.167 - add_hol4_mapping thyname thmname fullname thy22)
9.168 + "" => add_hol4_mapping thyname thmname fullname thy22
9.169 | output_thy =>
9.170 let
9.171 val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
9.172 - val _ = ImportRecorder.add_hol_move fullname moved_thmname
9.173 - val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
9.174 in
9.175 thy22 |> add_hol4_move fullname moved_thmname
9.176 |> add_hol4_mapping thyname thmname moved_thmname
9.177 @@ -2012,7 +1931,6 @@
9.178 acc ^ "\n " ^ quotename c ^ " :: \"" ^
9.179 Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
9.180 val thy' = add_dump str thy
9.181 - val _ = ImportRecorder.add_consts consts
9.182 in
9.183 Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
9.184 end
9.185 @@ -2024,7 +1942,6 @@
9.186 val (thy',res) = Choice_Specification.add_specification NONE
9.187 names'
9.188 (thy1,th)
9.189 - val _ = ImportRecorder.add_specification names' th
9.190 val res' = Thm.unvarify_global res
9.191 val hth = HOLThm(rens,res')
9.192 val rew = rewrite_hol4_term (concl_of res') thy'
9.193 @@ -2092,19 +2009,16 @@
9.194 val ((_, typedef_info), thy') =
9.195 Typedef.add_typedef_global false (SOME (Binding.name thmname))
9.196 (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
9.197 - val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
9.198
9.199 val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
9.200
9.201 val fulltyname = Sign.intern_type thy' tycname
9.202 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
9.203 - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
9.204
9.205 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
9.206 val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
9.207 else ()
9.208 val thy4 = add_hol4_pending thyname thmname args thy''
9.209 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
9.210
9.211 val rew = rewrite_hol4_term (concl_of td_th) thy4
9.212 val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
9.213 @@ -2169,7 +2083,6 @@
9.214 Typedef.add_typedef_global false NONE
9.215 (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c
9.216 (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
9.217 - val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
9.218 val fulltyname = Sign.intern_type thy' tycname
9.219 val aty = Type (fulltyname, map mk_vartype tnames)
9.220 val abs_ty = tT --> aty
9.221 @@ -2186,11 +2099,9 @@
9.222 raise ERR "type_introduction" "no term variables expected any more"
9.223 val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
9.224 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
9.225 - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
9.226 val _ = message "step 4"
9.227 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
9.228 val thy4 = add_hol4_pending thyname thmname args thy''
9.229 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
9.230
9.231 val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
9.232 val c =
10.1 --- a/src/HOL/Import/replay.ML Wed Jul 20 08:46:17 2011 +0200
10.2 +++ b/src/HOL/Import/replay.ML Wed Jul 20 10:11:08 2011 +0200
10.3 @@ -6,7 +6,6 @@
10.4 struct
10.5
10.6 open ProofKernel
10.7 -open ImportRecorder
10.8
10.9 exception REPLAY of string * string
10.10 fun ERR f mesg = REPLAY (f,mesg)
10.11 @@ -14,7 +13,6 @@
10.12
10.13 fun replay_proof int_thms thyname thmname prf thy =
10.14 let
10.15 - val _ = ImportRecorder.start_replay_proof thyname thmname
10.16 fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
10.17 | rp (PInstT(p,lambda)) thy =
10.18 let
10.19 @@ -269,13 +267,8 @@
10.20 | _ => rp pc thy
10.21 end
10.22 in
10.23 - let
10.24 - val x = rp' prf thy
10.25 - val _ = ImportRecorder.stop_replay_proof thyname thmname
10.26 - in
10.27 - x
10.28 - end
10.29 - end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x) (* FIXME avoid handle x ?? *)
10.30 + rp' prf thy
10.31 + end
10.32
10.33 fun setup_int_thms thyname thy =
10.34 let
10.35 @@ -316,74 +309,8 @@
10.36 replay_fact (thmname,thy)
10.37 end
10.38
10.39 -fun replay_chached_thm int_thms thyname thmname =
10.40 - let
10.41 - fun th_of thy = Skip_Proof.make_thm thy
10.42 - fun err msg = raise ERR "replay_cached_thm" msg
10.43 - val _ = writeln ("Replaying (from cache) "^thmname^" ...")
10.44 - fun rps [] thy = thy
10.45 - | rps (t::ts) thy = rps ts (rp t thy)
10.46 - and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy
10.47 - | rp (DeltaEntry ds) thy = fold delta ds thy
10.48 - and delta (Specification (names, th)) thy =
10.49 - fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
10.50 - | delta (Hol_mapping (thyname, thmname, isaname)) thy =
10.51 - add_hol4_mapping thyname thmname isaname thy
10.52 - | delta (Hol_pending (thyname, thmname, th)) thy =
10.53 - add_hol4_pending thyname thmname ([], th_of thy th) thy
10.54 - | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
10.55 - | delta (Hol_const_mapping (thyname, constname, fullcname)) thy =
10.56 - add_hol4_const_mapping thyname constname true fullcname thy
10.57 - | delta (Hol_move (fullname, moved_thmname)) thy =
10.58 - add_hol4_move fullname moved_thmname thy
10.59 - | delta (Defs (thmname, eq)) thy =
10.60 - snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
10.61 - | delta (Hol_theorem (thyname, thmname, th)) thy =
10.62 - add_hol4_theorem thyname thmname ([], th_of thy th) thy
10.63 - | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =
10.64 - snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
10.65 - (Binding.name t, map (rpair dummyS) vs, mx) c
10.66 - (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
10.67 - | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
10.68 - add_hol4_type_mapping thyname tycname true fulltyname thy
10.69 - | delta (Indexed_theorem (i, th)) thy =
10.70 - (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)
10.71 - | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
10.72 - | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
10.73 - in
10.74 - rps
10.75 - end
10.76 -
10.77 fun import_thms thyname int_thms thmnames thy =
10.78 let
10.79 - fun zip names [] = ([], names)
10.80 - | zip [] _ = ([], [])
10.81 - | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) =
10.82 - if thyname = thyname' andalso thmname = thmname' then
10.83 - (if aborted then ([], thmname::names) else
10.84 - let
10.85 - val _ = writeln ("theorem is in-sync: "^thmname)
10.86 - val (cached,normal) = zip names ys
10.87 - in
10.88 - (entry::cached, normal)
10.89 - end)
10.90 - else
10.91 - let
10.92 - val _ = writeln ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
10.93 - val _ = writeln ("proceeding with next uncached theorem...")
10.94 - in
10.95 - ([], thmname::names)
10.96 - end
10.97 - (* raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
10.98 - | zip (thmname::_) (DeltaEntry _ :: _) =
10.99 - raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
10.100 - fun zip' xs (History ys) =
10.101 - let
10.102 - val _ = writeln ("length of xs: "^(string_of_int (length xs)))
10.103 - val _ = writeln ("length of history: "^(string_of_int (length ys)))
10.104 - in
10.105 - zip xs ys
10.106 - end
10.107 fun replay_fact thmname thy =
10.108 let
10.109 val prf = mk_proof PDisk
10.110 @@ -393,10 +320,7 @@
10.111 in
10.112 p
10.113 end
10.114 - fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
10.115 - val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
10.116 - val _ = ImportRecorder.set_history (History (map ThmEntry cached))
10.117 - val res_thy = fold replay_fact normal (fold replay_cache cached thy)
10.118 + val res_thy = fold replay_fact thmnames thy
10.119 in
10.120 res_thy
10.121 end
11.1 --- a/src/HOL/Import/scan.ML Wed Jul 20 08:46:17 2011 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,219 +0,0 @@
11.4 -(* Title: HOL/Import/scan.ML
11.5 - Author: Sebastian Skalberg, TU Muenchen / Steven Obua, TU Muenchen
11.6 -
11.7 -Scanner combinators for sequences.
11.8 -*)
11.9 -
11.10 -signature SCANNER =
11.11 -sig
11.12 -
11.13 - include SCANNER_SEQ
11.14 -
11.15 - exception SyntaxError
11.16 -
11.17 - type ('a,'b) scanner = 'a seq -> 'b * 'a seq
11.18 -
11.19 - val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner)
11.20 - -> ('a,'b*'c) scanner
11.21 - val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
11.22 - val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
11.23 - val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
11.24 - val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
11.25 - val ^^ : ('a,string) scanner * ('a,string) scanner
11.26 - -> ('a,string) scanner
11.27 - val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
11.28 - val one : ('a -> bool) -> ('a,'a) scanner
11.29 - val anyone : ('a,'a) scanner
11.30 - val succeed : 'b -> ('a,'b) scanner
11.31 - val any : ('a -> bool) -> ('a,'a list) scanner
11.32 - val any1 : ('a -> bool) -> ('a,'a list) scanner
11.33 - val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
11.34 - val option : ('a,'b) scanner -> ('a,'b option) scanner
11.35 - val repeat : ('a,'b) scanner -> ('a,'b list) scanner
11.36 - val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
11.37 - val repeat_fixed : int -> ('a, 'b) scanner -> ('a, 'b list) scanner
11.38 - val ahead : ('a,'b) scanner -> ('a,'b) scanner
11.39 - val unless : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
11.40 - val $$ : ''a -> (''a,''a) scanner
11.41 - val !! : ('a seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
11.42 -
11.43 - val scan_id : (string, string) scanner
11.44 - val scan_nat : (string, int) scanner
11.45 -
11.46 - val this : ''a list -> (''a, ''a list) scanner
11.47 - val this_string : string -> (string, string) scanner
11.48 -end
11.49 -
11.50 -functor Scanner (structure Seq : SCANNER_SEQ) : SCANNER =
11.51 -struct
11.52 -
11.53 -infix 7 |-- --|
11.54 -infix 5 :-- -- ^^
11.55 -infix 3 >>
11.56 -infix 0 ||
11.57 -
11.58 -exception SyntaxError
11.59 -exception Fail of string
11.60 -
11.61 -type 'a seq = 'a Seq.seq
11.62 -type ('a,'b) scanner = 'a seq -> 'b * 'a seq
11.63 -
11.64 -val pull = Seq.pull
11.65 -
11.66 -fun (sc1 :-- sc2) toks =
11.67 - let
11.68 - val (x,toks2) = sc1 toks
11.69 - val (y,toks3) = sc2 x toks2
11.70 - in
11.71 - ((x,y),toks3)
11.72 - end
11.73 -
11.74 -fun (sc1 -- sc2) toks =
11.75 - let
11.76 - val (x,toks2) = sc1 toks
11.77 - val (y,toks3) = sc2 toks2
11.78 - in
11.79 - ((x,y),toks3)
11.80 - end
11.81 -
11.82 -fun (sc >> f) toks =
11.83 - let
11.84 - val (x,toks2) = sc toks
11.85 - in
11.86 - (f x,toks2)
11.87 - end
11.88 -
11.89 -fun (sc1 --| sc2) toks =
11.90 - let
11.91 - val (x,toks2) = sc1 toks
11.92 - val (_,toks3) = sc2 toks2
11.93 - in
11.94 - (x,toks3)
11.95 - end
11.96 -
11.97 -fun (sc1 |-- sc2) toks =
11.98 - let
11.99 - val (_,toks2) = sc1 toks
11.100 - in
11.101 - sc2 toks2
11.102 - end
11.103 -
11.104 -fun (sc1 ^^ sc2) toks =
11.105 - let
11.106 - val (x,toks2) = sc1 toks
11.107 - val (y,toks3) = sc2 toks2
11.108 - in
11.109 - (x^y,toks3)
11.110 - end
11.111 -
11.112 -fun (sc1 || sc2) toks =
11.113 - (sc1 toks)
11.114 - handle SyntaxError => sc2 toks
11.115 -
11.116 -fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
11.117 -
11.118 -fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
11.119 -
11.120 -fun succeed e toks = (e,toks)
11.121 -
11.122 -fun any p toks =
11.123 - case pull toks of
11.124 - NONE => ([],toks)
11.125 - | SOME(x,toks2) => if p x
11.126 - then
11.127 - let
11.128 - val (xs,toks3) = any p toks2
11.129 - in
11.130 - (x::xs,toks3)
11.131 - end
11.132 - else ([],toks)
11.133 -
11.134 -fun any1 p toks =
11.135 - let
11.136 - val (x,toks2) = one p toks
11.137 - val (xs,toks3) = any p toks2
11.138 - in
11.139 - (x::xs,toks3)
11.140 - end
11.141 -
11.142 -fun optional sc def = sc || succeed def
11.143 -fun option sc = (sc >> SOME) || succeed NONE
11.144 -
11.145 -(*
11.146 -fun repeat sc =
11.147 - let
11.148 - fun R toks =
11.149 - let
11.150 - val (x,toks2) = sc toks
11.151 - val (xs,toks3) = R toks2
11.152 - in
11.153 - (x::xs,toks3)
11.154 - end
11.155 - handle SyntaxError => ([],toks)
11.156 - in
11.157 - R
11.158 - end
11.159 -*)
11.160 -
11.161 -(* A tail-recursive version of repeat. It is (ever so) slightly slower
11.162 - * than the above, non-tail-recursive version (due to the garbage generation
11.163 - * associated with the reversal of the list). However, this version will be
11.164 - * able to process input where the former version must give up (due to stack
11.165 - * overflow). The slowdown seems to be around the one percent mark.
11.166 - *)
11.167 -fun repeat sc =
11.168 - let
11.169 - fun R xs toks =
11.170 - case SOME (sc toks) handle SyntaxError => NONE of
11.171 - SOME (x,toks2) => R (x::xs) toks2
11.172 - | NONE => (List.rev xs,toks)
11.173 - in
11.174 - R []
11.175 - end
11.176 -
11.177 -fun repeat1 sc toks =
11.178 - let
11.179 - val (x,toks2) = sc toks
11.180 - val (xs,toks3) = repeat sc toks2
11.181 - in
11.182 - (x::xs,toks3)
11.183 - end
11.184 -
11.185 -fun repeat_fixed n sc =
11.186 - let
11.187 - fun R n xs toks =
11.188 - if (n <= 0) then (List.rev xs, toks)
11.189 - else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
11.190 - in
11.191 - R n []
11.192 - end
11.193 -
11.194 -fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
11.195 -
11.196 -fun unless test sc toks =
11.197 - let
11.198 - val test_failed = (test toks;false) handle SyntaxError => true
11.199 - in
11.200 - if test_failed
11.201 - then sc toks
11.202 - else raise SyntaxError
11.203 - end
11.204 -
11.205 -fun $$ arg = one (fn x => x = arg)
11.206 -
11.207 -fun !! f sc toks = (sc toks
11.208 - handle SyntaxError => raise Fail (f toks))
11.209 -
11.210 -val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
11.211 -
11.212 -val nat_of_list = the o Int.fromString o implode
11.213 -
11.214 -val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list
11.215 -
11.216 -fun this [] = (fn toks => ([], toks))
11.217 - | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
11.218 -
11.219 -fun this_string s = this (raw_explode s) >> K s
11.220 -
11.221 -end
11.222 -
12.1 --- a/src/HOL/Import/seq.ML Wed Jul 20 08:46:17 2011 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,99 +0,0 @@
12.4 -signature SCANNER_SEQ =
12.5 -sig
12.6 - type 'a seq
12.7 -
12.8 - val pull : 'a seq -> ('a * 'a seq) option
12.9 -end
12.10 -
12.11 -signature EXTENDED_SCANNER_SEQ =
12.12 -sig
12.13 -
12.14 - include SCANNER_SEQ
12.15 -
12.16 - val null : 'a seq -> bool
12.17 - val length : 'a seq -> int
12.18 - val take_at_most : 'a seq -> int -> 'a list
12.19 -
12.20 -end
12.21 -
12.22 -functor ExtendScannerSeq (structure Seq : SCANNER_SEQ) : EXTENDED_SCANNER_SEQ =
12.23 -struct
12.24 -
12.25 -type 'a seq = 'a Seq.seq
12.26 -
12.27 -val pull = Seq.pull
12.28 -
12.29 -fun null s = is_none (pull s)
12.30 -
12.31 -fun take_at_most s n =
12.32 - if n <= 0 then [] else
12.33 - case pull s of
12.34 - NONE => []
12.35 - | SOME (x,s') => x::(take_at_most s' (n-1))
12.36 -
12.37 -fun length' s n =
12.38 - case pull s of
12.39 - NONE => n
12.40 - | SOME (_, s') => length' s' (n+1)
12.41 -
12.42 -fun length s = length' s 0
12.43 -
12.44 -end
12.45 -
12.46 -signature VECTOR_SCANNER_SEQ =
12.47 -sig
12.48 - include EXTENDED_SCANNER_SEQ
12.49 -
12.50 - val fromString : string -> string seq
12.51 - val fromVector : 'a Vector.vector -> 'a seq
12.52 -end
12.53 -
12.54 -structure VectorScannerSeq :> VECTOR_SCANNER_SEQ =
12.55 -struct
12.56 -
12.57 -structure Incubator : SCANNER_SEQ =
12.58 -struct
12.59 -
12.60 -type 'a seq = 'a Vector.vector * int * int
12.61 -fun pull (v, len, i) = if i >= len then NONE else SOME (Vector.sub (v, i), (v, len, i+1))
12.62 -
12.63 -end
12.64 -
12.65 -structure Extended = ExtendScannerSeq (structure Seq = Incubator)
12.66 -
12.67 -open Extended
12.68 -
12.69 -fun fromVector v = (v, Vector.length v, 0)
12.70 -fun vector_from_string s = Vector.tabulate (String.size s, fn i => String.str (String.sub (s, i)))
12.71 -fun fromString s = fromVector (vector_from_string s)
12.72 -
12.73 -end
12.74 -
12.75 -signature LIST_SCANNER_SEQ =
12.76 -sig
12.77 - include EXTENDED_SCANNER_SEQ
12.78 -
12.79 - val fromString : string -> string seq
12.80 - val fromList : 'a list -> 'a seq
12.81 -end
12.82 -
12.83 -structure ListScannerSeq :> LIST_SCANNER_SEQ =
12.84 -struct
12.85 -
12.86 -structure Incubator : SCANNER_SEQ =
12.87 -struct
12.88 -
12.89 -type 'a seq = 'a list
12.90 -fun pull [] = NONE
12.91 - | pull (x::xs) = SOME (x, xs)
12.92 -
12.93 -end
12.94 -
12.95 -structure Extended = ExtendScannerSeq (structure Seq = Incubator)
12.96 -
12.97 -open Extended
12.98 -
12.99 -val fromList = I
12.100 -val fromString = raw_explode
12.101 -
12.102 -end
13.1 --- a/src/HOL/Import/xml.ML Wed Jul 20 08:46:17 2011 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,199 +0,0 @@
13.4 -(* Title: HOL/Import/xml.ML
13.5 -
13.6 -Yet another version of XML support.
13.7 -*)
13.8 -
13.9 -signature XML =
13.10 -sig
13.11 - val header: string
13.12 - val text: string -> string
13.13 - val text_charref: string -> string
13.14 - val cdata: string -> string
13.15 - val element: string -> (string * string) list -> string list -> string
13.16 -
13.17 - datatype tree =
13.18 - Elem of string * (string * string) list * tree list
13.19 - | Text of string
13.20 -
13.21 - val string_of_tree: tree -> string
13.22 - val tree_of_string: string -> tree
13.23 -
13.24 - val encoded_string_of_tree : tree -> string
13.25 - val tree_of_encoded_string : string -> tree
13.26 -end;
13.27 -
13.28 -structure XML :> XML =
13.29 -struct
13.30 -
13.31 -(*structure Seq = VectorScannerSeq
13.32 -structure Scan = Scanner (structure Seq = Seq)*)
13.33 -structure Seq = StringScannerSeq
13.34 -structure Scan = StringScanner
13.35 -
13.36 -
13.37 -open Scan
13.38 -
13.39 -(** string based representation (small scale) **)
13.40 -
13.41 -val header = "<?xml version=\"1.0\"?>\n";
13.42 -
13.43 -(* text and character data *)
13.44 -
13.45 -fun decode "<" = "<"
13.46 - | decode ">" = ">"
13.47 - | decode "&" = "&"
13.48 - | decode "'" = "'"
13.49 - | decode """ = "\""
13.50 - | decode c = c;
13.51 -
13.52 -fun encode "<" = "<"
13.53 - | encode ">" = ">"
13.54 - | encode "&" = "&"
13.55 - | encode "'" = "'"
13.56 - | encode "\"" = """
13.57 - | encode c = c;
13.58 -
13.59 -fun encode_charref c = "&#" ^ string_of_int (ord c) ^ ";"
13.60 -
13.61 -val text = Library.translate_string encode
13.62 -
13.63 -val text_charref = translate_string encode_charref;
13.64 -
13.65 -val cdata = enclose "<![CDATA[" "]]>\n"
13.66 -
13.67 -(* elements *)
13.68 -
13.69 -fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
13.70 -
13.71 -fun element name atts cs =
13.72 - let val elem = space_implode " " (name :: map attribute atts) in
13.73 - if null cs then enclose "<" "/>" elem
13.74 - else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
13.75 - end;
13.76 -
13.77 -(** explicit XML trees **)
13.78 -
13.79 -datatype tree =
13.80 - Elem of string * (string * string) list * tree list
13.81 - | Text of string;
13.82 -
13.83 -fun string_of_tree tree =
13.84 - let
13.85 - fun string_of (Elem (name, atts, ts)) buf =
13.86 - let val buf' =
13.87 - buf |> Buffer.add "<"
13.88 - |> fold Buffer.add (separate " " (name :: map attribute atts))
13.89 - in
13.90 - if null ts then
13.91 - buf' |> Buffer.add "/>"
13.92 - else
13.93 - buf' |> Buffer.add ">"
13.94 - |> fold string_of ts
13.95 - |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
13.96 - end
13.97 - | string_of (Text s) buf = Buffer.add (text s) buf;
13.98 - in Buffer.content (string_of tree Buffer.empty) end;
13.99 -
13.100 -(** XML parsing **)
13.101 -
13.102 -fun beginning n xs = Symbol.beginning n (Seq.take_at_most xs n)
13.103 -
13.104 -fun err s xs =
13.105 - "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
13.106 -
13.107 -val scan_whspc = Scan.any Symbol.is_blank;
13.108 -
13.109 -val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
13.110 -
13.111 -val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
13.112 - (scan_special || Scan.one Symbol.is_regular)) >> implode;
13.113 -
13.114 -val parse_cdata = Scan.this_string "<![CDATA[" |--
13.115 - (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
13.116 - implode) --| Scan.this_string "]]>";
13.117 -
13.118 -val parse_att =
13.119 - scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
13.120 - (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
13.121 - (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
13.122 -
13.123 -val parse_comment = Scan.this_string "<!--" --
13.124 - Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
13.125 - Scan.this_string "-->";
13.126 -
13.127 -val scan_comment_whspc =
13.128 - (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
13.129 -
13.130 -val parse_pi = Scan.this_string "<?" |--
13.131 - Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
13.132 - Scan.this_string "?>";
13.133 -
13.134 -fun parse_content xs =
13.135 - ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
13.136 - (Scan.repeat ((* scan_whspc |-- *)
13.137 - ( parse_elem >> single
13.138 - || parse_cdata >> (single o Text)
13.139 - || parse_pi >> K []
13.140 - || parse_comment >> K []) --
13.141 - Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
13.142 - >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
13.143 -
13.144 -and parse_elem xs =
13.145 - ($$ "<" |-- scan_id --
13.146 - Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
13.147 - !! (err "Expected > or />")
13.148 - (Scan.this_string "/>" >> K []
13.149 - || $$ ">" |-- parse_content --|
13.150 - !! (err ("Expected </" ^ s ^ ">"))
13.151 - (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
13.152 - (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
13.153 -
13.154 -val parse_document =
13.155 - Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
13.156 - (Scan.repeat (Scan.unless ($$ ">")
13.157 - (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
13.158 - parse_elem;
13.159 -
13.160 -fun tree_of_string s =
13.161 - let
13.162 - val seq = Seq.fromString s
13.163 - val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
13.164 - val (x, toks) = scanner seq
13.165 - in
13.166 - if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
13.167 - end
13.168 -
13.169 -(* More efficient saving and loading of xml trees employing a proprietary external format *)
13.170 -
13.171 -fun write_lstring s buf = buf |> Buffer.add (string_of_int (size s)) |> Buffer.add " " |> Buffer.add s
13.172 -fun parse_lstring toks = (scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i (one (K true))) >> snd >> implode) toks
13.173 -
13.174 -fun write_list w l buf = buf |> Buffer.add (string_of_int (length l)) |> Buffer.add " " |> fold w l
13.175 -fun parse_list sc = scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i sc) >> snd
13.176 -
13.177 -fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
13.178 - | write_tree (Elem (name, attrs, children)) buf =
13.179 - buf |> Buffer.add "E"
13.180 - |> write_lstring name
13.181 - |> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs
13.182 - |> write_list write_tree children
13.183 -
13.184 -fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
13.185 -and parse_elem toks = (parse_lstring -- parse_list (parse_lstring -- parse_lstring) -- parse_list parse_tree >> (fn ((n, a), c) => Elem (n,a,c))) toks
13.186 -
13.187 -fun encoded_string_of_tree tree = Buffer.content (write_tree tree Buffer.empty)
13.188 -
13.189 -fun tree_of_encoded_string s =
13.190 - let
13.191 - fun print (a,b) = writeln (a^" "^(string_of_int b))
13.192 - val _ = print ("length of encoded string: ", size s)
13.193 - val _ = writeln "Seq.fromString..."
13.194 - val seq = timeit (fn () => Seq.fromString s)
13.195 - val _ = print ("length of sequence", timeit (fn () => Seq.length seq))
13.196 - val scanner = !! (err "Malformed encoded xml") parse_tree
13.197 - val (x, toks) = scanner seq
13.198 - in
13.199 - if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
13.200 - end
13.201 -
13.202 -end;
14.1 --- a/src/HOL/Import/xmlconv.ML Wed Jul 20 08:46:17 2011 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,303 +0,0 @@
14.4 -signature XML_CONV =
14.5 -sig
14.6 - type 'a input = XML.tree -> 'a
14.7 - type 'a output = 'a -> XML.tree
14.8 -
14.9 - exception ParseException of string
14.10 -
14.11 - val xml_of_typ: typ output
14.12 - val typ_of_xml: typ input
14.13 -
14.14 - val xml_of_term: term output
14.15 - val term_of_xml : term input
14.16 -
14.17 - val xml_of_mixfix: mixfix output
14.18 - val mixfix_of_xml: mixfix input
14.19 -
14.20 - val xml_of_proof: Proofterm.proof output
14.21 -
14.22 - val xml_of_bool: bool output
14.23 - val bool_of_xml: bool input
14.24 -
14.25 - val xml_of_int: int output
14.26 - val int_of_xml: int input
14.27 -
14.28 - val xml_of_string: string output
14.29 - val string_of_xml: string input
14.30 -
14.31 - val xml_of_list: 'a output -> 'a list output
14.32 - val list_of_xml: 'a input -> 'a list input
14.33 -
14.34 - val xml_of_tuple : 'a output -> 'a list output
14.35 - val tuple_of_xml: 'a input -> int -> 'a list input
14.36 -
14.37 - val xml_of_option: 'a output -> 'a option output
14.38 - val option_of_xml: 'a input -> 'a option input
14.39 -
14.40 - val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
14.41 - val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
14.42 -
14.43 - val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
14.44 - val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
14.45 -
14.46 - val xml_of_unit: unit output
14.47 - val unit_of_xml: unit input
14.48 -
14.49 - val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
14.50 - val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
14.51 -
14.52 - val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
14.53 - val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
14.54 -
14.55 - val wrap : string -> 'a output -> 'a output
14.56 - val unwrap : ('a -> 'b) -> 'a input -> 'b input
14.57 - val wrap_empty : string output
14.58 - val unwrap_empty : 'a -> 'a input
14.59 - val name_of_wrap : XML.tree -> string
14.60 -
14.61 - val write_to_file: 'a output -> string -> 'a -> unit
14.62 - val read_from_file: 'a input -> string -> 'a
14.63 -
14.64 - val serialize_to_file : 'a output -> string -> 'a -> unit
14.65 - val deserialize_from_file : 'a input -> string -> 'a
14.66 -end;
14.67 -
14.68 -structure XMLConv : XML_CONV =
14.69 -struct
14.70 -
14.71 -type 'a input = XML.tree -> 'a
14.72 -type 'a output = 'a -> XML.tree
14.73 -exception ParseException of string
14.74 -
14.75 -fun parse_err s = raise ParseException s
14.76 -
14.77 -fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
14.78 -
14.79 -fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
14.80 - | class_of_xml _ = parse_err "class"
14.81 -
14.82 -fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
14.83 - ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
14.84 - map xml_of_class S)
14.85 - | xml_of_typ (TFree (s, S)) =
14.86 - XML.Elem ("TFree", [("name", s)], map xml_of_class S)
14.87 - | xml_of_typ (Type (s, Ts)) =
14.88 - XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
14.89 -
14.90 -fun intofstr s i =
14.91 - case Int.fromString i of
14.92 - NONE => parse_err (s^", invalid index: "^i)
14.93 - | SOME i => i
14.94 -
14.95 -fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
14.96 - | typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) =
14.97 - TVar ((s, intofstr "TVar" i), map class_of_xml cs)
14.98 - | typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
14.99 - | typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
14.100 - | typ_of_xml _ = parse_err "type"
14.101 -
14.102 -fun xml_of_term (Bound i) =
14.103 - XML.Elem ("Bound", [("index", string_of_int i)], [])
14.104 - | xml_of_term (Free (s, T)) =
14.105 - XML.Elem ("Free", [("name", s)], [xml_of_typ T])
14.106 - | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
14.107 - ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
14.108 - [xml_of_typ T])
14.109 - | xml_of_term (Const (s, T)) =
14.110 - XML.Elem ("Const", [("name", s)], [xml_of_typ T])
14.111 - | xml_of_term (t $ u) =
14.112 - XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
14.113 - | xml_of_term (Abs (s, T, t)) =
14.114 - XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
14.115 -
14.116 -fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
14.117 - | term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
14.118 - | term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
14.119 - | term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
14.120 - | term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
14.121 - | term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
14.122 - | term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
14.123 - | term_of_xml _ = parse_err "term"
14.124 -
14.125 -fun xml_of_opttypes NONE = []
14.126 - | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
14.127 -
14.128 -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
14.129 -(* it can be looked up in the theorem database. Thus, it could be *)
14.130 -(* omitted from the xml representation. *)
14.131 -
14.132 -fun xml_of_proof (PBound i) =
14.133 - XML.Elem ("PBound", [("index", string_of_int i)], [])
14.134 - | xml_of_proof (Abst (s, optT, prf)) =
14.135 - XML.Elem ("Abst", [("vname", s)],
14.136 - (case optT of NONE => [] | SOME T => [xml_of_typ T]) @
14.137 - [xml_of_proof prf])
14.138 - | xml_of_proof (AbsP (s, optt, prf)) =
14.139 - XML.Elem ("AbsP", [("vname", s)],
14.140 - (case optt of NONE => [] | SOME t => [xml_of_term t]) @
14.141 - [xml_of_proof prf])
14.142 - | xml_of_proof (prf % optt) =
14.143 - XML.Elem ("Appt", [],
14.144 - xml_of_proof prf ::
14.145 - (case optt of NONE => [] | SOME t => [xml_of_term t]))
14.146 - | xml_of_proof (prf %% prf') =
14.147 - XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
14.148 - | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
14.149 - | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
14.150 - XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
14.151 - | xml_of_proof (PAxm (s, t, optTs)) =
14.152 - XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
14.153 - | xml_of_proof (Oracle (s, t, optTs)) =
14.154 - XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
14.155 - | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
14.156 -
14.157 -fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
14.158 -fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
14.159 -fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
14.160 -fun xml_of_unit () = XML.Elem ("unit", [], [])
14.161 -fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
14.162 -fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
14.163 -fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
14.164 -fun wrap s output x = XML.Elem (s, [], [output x])
14.165 -fun wrap_empty s = XML.Elem (s, [], [])
14.166 -fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
14.167 -fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
14.168 -fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) =
14.169 - XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
14.170 -fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) =
14.171 - XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
14.172 -
14.173 -fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
14.174 - | bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
14.175 - | bool_of_xml _ = parse_err "bool"
14.176 -
14.177 -fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
14.178 - | int_of_xml _ = parse_err "int"
14.179 -
14.180 -fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
14.181 - | unit_of_xml _ = parse_err "unit"
14.182 -
14.183 -fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
14.184 - | list_of_xml _ _ = parse_err "list"
14.185 -
14.186 -fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) =
14.187 - if i = length ls then map input ls else parse_err "tuple"
14.188 - | tuple_of_xml _ _ _ = parse_err "tuple"
14.189 -
14.190 -fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
14.191 - | option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
14.192 - | option_of_xml _ _ = parse_err "option"
14.193 -
14.194 -fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
14.195 - | pair_of_xml _ _ _ = parse_err "pair"
14.196 -
14.197 -fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
14.198 - | triple_of_xml _ _ _ _ = parse_err "triple"
14.199 -
14.200 -fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) =
14.201 - (input1 x1, input2 x2, input3 x3, input4 x4)
14.202 - | quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
14.203 -
14.204 -fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) =
14.205 - (input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
14.206 - | quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
14.207 -
14.208 -fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
14.209 - | unwrap _ _ _ = parse_err "unwrap"
14.210 -
14.211 -fun unwrap_empty x (XML.Elem (_, [], [])) = x
14.212 - | unwrap_empty _ _ = parse_err "unwrap_unit"
14.213 -
14.214 -fun name_of_wrap (XML.Elem (name, _, _)) = name
14.215 - | name_of_wrap _ = parse_err "name_of_wrap"
14.216 -
14.217 -fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
14.218 - | string_of_xml _ = parse_err "string"
14.219 -
14.220 -fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
14.221 - | xml_of_mixfix Structure = wrap_empty "structure"
14.222 - | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
14.223 - | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
14.224 - | xml_of_mixfix (Infix args) = wrap "infix" (xml_of_pair xml_of_string xml_of_int) args
14.225 - | xml_of_mixfix (Infixl args) = wrap "infixl" (xml_of_pair xml_of_string xml_of_int) args
14.226 - | xml_of_mixfix (Infixr args) = wrap "infixr" (xml_of_pair xml_of_string xml_of_int) args
14.227 - | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
14.228 -
14.229 -fun mixfix_of_xml e =
14.230 - (case name_of_wrap e of
14.231 - "nosyn" => unwrap_empty NoSyn
14.232 - | "structure" => unwrap_empty Structure
14.233 - | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
14.234 - | "delimfix" => unwrap Delimfix string_of_xml
14.235 - | "infix" => unwrap Infix (pair_of_xml string_of_xml int_of_xml)
14.236 - | "infixl" => unwrap Infixl (pair_of_xml string_of_xml int_of_xml)
14.237 - | "infixr" => unwrap Infixr (pair_of_xml string_of_xml int_of_xml)
14.238 - | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
14.239 - | _ => parse_err "mixfix"
14.240 - ) e
14.241 -
14.242 -
14.243 -fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
14.244 -
14.245 -fun from_file f input fname =
14.246 - let
14.247 - val _ = writeln "read_from_file enter"
14.248 - val s = File.read (Path.explode fname)
14.249 - val _ = writeln "done: read file"
14.250 - val tree = timeit (fn () => f s)
14.251 - val _ = writeln "done: tree"
14.252 - val x = timeit (fn () => input tree)
14.253 - val _ = writeln "done: input"
14.254 - in
14.255 - x
14.256 - end
14.257 -
14.258 -fun write_to_file x = to_file XML.string_of_tree x
14.259 -fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
14.260 -
14.261 -fun serialize_to_file x = to_file XML.encoded_string_of_tree x
14.262 -fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
14.263 -
14.264 -end;
14.265 -
14.266 -structure XMLConvOutput =
14.267 -struct
14.268 -open XMLConv
14.269 -
14.270 -val typ = xml_of_typ
14.271 -val term = xml_of_term
14.272 -val mixfix = xml_of_mixfix
14.273 -val proof = xml_of_proof
14.274 -val bool = xml_of_bool
14.275 -val int = xml_of_int
14.276 -val string = xml_of_string
14.277 -val unit = xml_of_unit
14.278 -val list = xml_of_list
14.279 -val pair = xml_of_pair
14.280 -val option = xml_of_option
14.281 -val triple = xml_of_triple
14.282 -val quadruple = xml_of_quadruple
14.283 -val quintuple = xml_of_quintuple
14.284 -
14.285 -end
14.286 -
14.287 -structure XMLConvInput =
14.288 -struct
14.289 -open XMLConv
14.290 -
14.291 -val typ = typ_of_xml
14.292 -val term = term_of_xml
14.293 -val mixfix = mixfix_of_xml
14.294 -val bool = bool_of_xml
14.295 -val int = int_of_xml
14.296 -val string = string_of_xml
14.297 -val unit = unit_of_xml
14.298 -val list = list_of_xml
14.299 -val pair = pair_of_xml
14.300 -val option = option_of_xml
14.301 -val triple = triple_of_xml
14.302 -val quadruple = quadruple_of_xml
14.303 -val quintuple = quintuple_of_xml
14.304 -
14.305 -end
14.306 -
15.1 --- a/src/HOL/IsaMakefile Wed Jul 20 08:46:17 2011 +0200
15.2 +++ b/src/HOL/IsaMakefile Wed Jul 20 10:11:08 2011 +0200
15.3 @@ -555,13 +555,11 @@
15.4 ## HOL-Import
15.5
15.6 IMPORTER_FILES = \
15.7 - Import/ImportRecorder.thy Import/HOL4Compat.thy \
15.8 + Import/HOL4Compat.thy \
15.9 Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \
15.10 Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \
15.11 - Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \
15.12 - Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \
15.13 - Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \
15.14 - Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \
15.15 + Import/import.ML Import/import_syntax.ML \
15.16 + Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \
15.17 Library/ContNotDenum.thy Old_Number_Theory/Primes.thy
15.18
15.19 HOL-Import: HOL $(LOG)/HOL-Import.gz