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.
--- a/src/HOL/Import/HOL4Setup.thy Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/Import/HOL4Setup.thy Wed Jul 20 10:11:08 2011 +0200
@@ -2,7 +2,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Setup imports MakeEqual ImportRecorder
+theory HOL4Setup imports MakeEqual
uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import.ML") begin
section {* General Setup *}
--- a/src/HOL/Import/HOLLight/hollight.imp Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Wed Jul 20 10:11:08 2011 +0200
@@ -1273,9 +1273,9 @@
"NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
"NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
"NSUM_0" > "HOLLight.hollight.NSUM_0"
- "NOT_UNIV_PSUBSET" > "Complete_Lattice.complete_lattice_class.not_top_less"
+ "NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
"NOT_SUC" > "Nat.Suc_not_Zero"
- "NOT_PSUBSET_EMPTY" > "Complete_Lattice.complete_lattice_class.not_less_bot"
+ "NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
"NOT_ODD" > "HOLLight.hollight.NOT_ODD"
"NOT_LT" > "Orderings.linorder_class.not_less"
"NOT_LE" > "Orderings.linorder_class.not_le"
@@ -1644,7 +1644,7 @@
"IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
"IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
"IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
- "IMAGE_ID" > "Fun.image_ident"
+ "IMAGE_ID" > "Set.image_ident"
"IMAGE_I" > "Fun.image_id"
"IMAGE_EQ_EMPTY" > "Set.image_is_empty"
"IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
--- a/src/HOL/Import/ImportRecorder.thy Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-theory ImportRecorder imports Main
-uses "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
-begin
-end
\ No newline at end of file
--- a/src/HOL/Import/import_syntax.ML Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/Import/import_syntax.ML Wed Jul 20 10:11:08 2011 +0200
@@ -19,9 +19,6 @@
val const_moves : (theory -> theory) parser
val const_renames : (theory -> theory) parser
- val skip_import_dir : (theory -> theory) parser
- val skip_import : (theory -> theory) parser
-
val setup : unit -> unit
end
@@ -39,13 +36,6 @@
|> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
-fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
-val skip_import_dir = Parse.string >> do_skip_import_dir
-
-val lower = String.map Char.toLower
-fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
-val skip_import = Parse.short_ident >> do_skip_import
-
fun end_import toks =
Scan.succeed
(fn thy =>
@@ -54,16 +44,7 @@
val segname = get_import_segment thy
val (int_thms,facts) = Replay.setup_int_thms thyname thy
val thmnames = filter_out (should_ignore thyname thy) facts
- fun replay thy =
- let
- val _ = ImportRecorder.load_history thyname
- val thy = Replay.import_thms thyname int_thms thmnames thy
- (*handle x => (ImportRecorder.save_history thyname; raise x)*) (* FIXME avoid handle x ?? *)
- val _ = ImportRecorder.save_history thyname
- val _ = ImportRecorder.clear_history ()
- in
- thy
- end
+ fun replay thy = Replay.import_thms thyname int_thms thmnames thy
in
thy |> clear_import_thy
|> set_segment thyname segname
@@ -225,12 +206,6 @@
Outer_Syntax.command "end_import"
"End HOL4 import"
Keyword.thy_decl (end_import >> Toplevel.theory);
- Outer_Syntax.command "skip_import_dir"
- "Sets caching directory for skipping importing"
- Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
- Outer_Syntax.command "skip_import"
- "Switches skipping importing on or off"
- Keyword.thy_decl (skip_import >> Toplevel.theory);
Outer_Syntax.command "setup_theory"
"Setup HOL4 theory replaying"
Keyword.thy_decl (setup_theory >> Toplevel.theory);
--- a/src/HOL/Import/importrecorder.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,265 +0,0 @@
-signature IMPORT_RECORDER =
-sig
-
- datatype deltastate = Consts of (string * typ * mixfix) list
- | Specification of (string * string * bool) list * term
- | Hol_mapping of string * string * string
- | Hol_pending of string * string * term
- | Hol_const_mapping of string * string * string
- | Hol_move of string * string
- | Defs of string * term
- | Hol_theorem of string * string * term
- | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
- | Hol_type_mapping of string * string * string
- | Indexed_theorem of int * term
- | Protect_varname of string * string
- | Dump of string
-
- datatype history = History of history_entry list
- and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
-
- val get_history : unit -> history
- val set_history : history -> unit
- val clear_history : unit -> unit
-
- val start_replay_proof : string -> string -> unit
- val stop_replay_proof : string -> string -> unit
- val abort_replay_proof : string -> string -> unit
-
- val add_consts : (string * typ * mixfix) list -> unit
- val add_specification : (string * string * bool) list -> thm -> unit
- val add_hol_mapping : string -> string -> string -> unit
- val add_hol_pending : string -> string -> thm -> unit
- val add_hol_const_mapping : string -> string -> string -> unit
- val add_hol_move : string -> string -> unit
- val add_defs : string -> term -> unit
- val add_hol_theorem : string -> string -> thm -> unit
- val add_typedef : string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
- val add_hol_type_mapping : string -> string -> string -> unit
- val add_indexed_theorem : int -> thm -> unit
- val protect_varname : string -> string -> unit
- val add_dump : string -> unit
-
- val set_skip_import_dir : string option -> unit
- val get_skip_import_dir : unit -> string option
-
- val set_skip_import : bool -> unit
- val get_skip_import : unit -> bool
-
- val save_history : string -> unit
- val load_history : string -> unit
-end
-
-structure ImportRecorder :> IMPORT_RECORDER =
-struct
-
-datatype deltastate = Consts of (string * typ * mixfix) list
- | Specification of (string * string * bool) list * term
- | Hol_mapping of string * string * string
- | Hol_pending of string * string * term
- | Hol_const_mapping of string * string * string
- | Hol_move of string * string
- | Defs of string * term
- | Hol_theorem of string * string * term
- | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term
- | Hol_type_mapping of string * string * string
- | Indexed_theorem of int * term
- | Protect_varname of string * string
- | Dump of string
-
-datatype history_entry = StartReplay of string*string
- | StopReplay of string*string
- | AbortReplay of string*string
- | Delta of deltastate list
-
-val history = Unsynchronized.ref ([]:history_entry list)
-val history_dir = Unsynchronized.ref (SOME "")
-val skip_imports = Unsynchronized.ref false
-
-fun set_skip_import b = skip_imports := b
-fun get_skip_import () = !skip_imports
-
-fun clear_history () = history := []
-
-fun add_delta d = history := (case !history of (Delta ds)::hs => (Delta (d::ds))::hs | hs => (Delta [d])::hs)
-fun add_replay r = history := (r :: (!history))
-
-local
- open XMLConvOutput
- val consts = list (triple string typ mixfix)
- val specification = pair (list (triple string string bool)) term
- val hol_mapping = triple string string string
- val hol_pending = triple string string term
- val hol_const_mapping = triple string string string
- val hol_move = pair string string
- val defs = pair string term
- val hol_theorem = triple string string term
- val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
- val hol_type_mapping = triple string string string
- val indexed_theorem = pair int term
- val entry = pair string string
-
- fun delta (Consts args) = wrap "consts" consts args
- | delta (Specification args) = wrap "specification" specification args
- | delta (Hol_mapping args) = wrap "hol_mapping" hol_mapping args
- | delta (Hol_pending args) = wrap "hol_pending" hol_pending args
- | delta (Hol_const_mapping args) = wrap "hol_const_mapping" hol_const_mapping args
- | delta (Hol_move args) = wrap "hol_move" hol_move args
- | delta (Defs args) = wrap "defs" defs args
- | delta (Hol_theorem args) = wrap "hol_theorem" hol_theorem args
- | delta (Typedef args) = wrap "typedef" typedef args
- | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
- | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
- | delta (Protect_varname args) = wrap "protect_varname" entry args
- | delta (Dump args) = wrap "dump" string args
-
- fun history_entry (StartReplay args) = wrap "startreplay" entry args
- | history_entry (StopReplay args) = wrap "stopreplay" entry args
- | history_entry (AbortReplay args) = wrap "abortreplay" entry args
- | history_entry (Delta args) = wrap "delta" (list delta) args
-in
-
-val xml_of_history = list history_entry
-
-end
-
-local
- open XMLConvInput
- val consts = list (triple string typ mixfix)
- val specification = pair (list (triple string string bool)) term
- val hol_mapping = triple string string string
- val hol_pending = triple string string term
- val hol_const_mapping = triple string string string
- val hol_move = pair string string
- val defs = pair string term
- val hol_theorem = triple string string term
- val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
- val hol_type_mapping = triple string string string
- val indexed_theorem = pair int term
- val entry = pair string string
-
- fun delta "consts" = unwrap Consts consts
- | delta "specification" = unwrap Specification specification
- | delta "hol_mapping" = unwrap Hol_mapping hol_mapping
- | delta "hol_pending" = unwrap Hol_pending hol_pending
- | delta "hol_const_mapping" = unwrap Hol_const_mapping hol_const_mapping
- | delta "hol_move" = unwrap Hol_move hol_move
- | delta "defs" = unwrap Defs defs
- | delta "hol_theorem" = unwrap Hol_theorem hol_theorem
- | delta "typedef" = unwrap Typedef typedef
- | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
- | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
- | delta "protect_varname" = unwrap Protect_varname entry
- | delta "dump" = unwrap Dump string
- | delta _ = raise ParseException "delta"
-
- val delta = fn e => delta (name_of_wrap e) e
-
- fun history_entry "startreplay" = unwrap StartReplay entry
- | history_entry "stopreplay" = unwrap StopReplay entry
- | history_entry "abortreplay" = unwrap AbortReplay entry
- | history_entry "delta" = unwrap Delta (list delta)
- | history_entry _ = raise ParseException "history_entry"
-
- val history_entry = fn e => history_entry (name_of_wrap e) e
-in
-
-val history_of_xml = list history_entry
-
-end
-
-fun start_replay_proof thyname thmname = add_replay (StartReplay (thyname, thmname))
-fun stop_replay_proof thyname thmname = add_replay (StopReplay (thyname, thmname))
-fun abort_replay_proof thyname thmname = add_replay (AbortReplay (thyname, thmname))
-fun add_hol_theorem thyname thmname thm = add_delta (Hol_theorem (thyname, thmname, prop_of thm))
-fun add_hol_mapping thyname thmname isaname = add_delta (Hol_mapping (thyname, thmname, isaname))
-fun add_consts consts = add_delta (Consts consts)
-fun add_typedef thmname_opt typ c absrep_opt th = add_delta (Typedef (thmname_opt, typ, c, absrep_opt, prop_of th))
-fun add_defs thmname eq = add_delta (Defs (thmname, eq))
-fun add_hol_const_mapping thyname constname fullcname = add_delta (Hol_const_mapping (thyname, constname, fullcname))
-fun add_hol_move fullname moved_thmname = add_delta (Hol_move (fullname, moved_thmname))
-fun add_hol_type_mapping thyname tycname fulltyname = add_delta (Hol_type_mapping (thyname, tycname, fulltyname))
-fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
-fun add_specification names th = add_delta (Specification (names, prop_of th))
-fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
-fun protect_varname s t = add_delta (Protect_varname (s,t))
-fun add_dump s = add_delta (Dump s)
-
-fun set_skip_import_dir dir = (history_dir := dir)
-fun get_skip_import_dir () = !history_dir
-
-fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
-
-fun save_history thyname =
- if get_skip_import () then
- XMLConv.write_to_file xml_of_history (get_filename thyname) (!history)
- else
- ()
-
-fun load_history thyname =
- if get_skip_import () then
- let
- val filename = get_filename thyname
- val _ = writeln "load_history / before"
- val _ =
- if File.exists (Path.explode filename) then
- (history := XMLConv.read_from_file history_of_xml (get_filename thyname))
- else
- clear_history ()
- val _ = writeln "load_history / after"
- in
- ()
- end
- else
- ()
-
-
-datatype history = History of history_entry list
- and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
-
-exception CONV
-
-fun conv_histories ((StartReplay (thyname, thmname))::rest) =
- let
- val (hs, rest) = conv_histories rest
- fun continue thyname' thmname' aborted rest =
- if thyname = thyname' andalso thmname = thmname' then
- let
- val (hs', rest) = conv_histories rest
- in
- ((ThmEntry (thyname, thmname, aborted, History hs))::hs', rest)
- end
- else
- raise CONV
- in
- case rest of
- (StopReplay (thyname',thmname'))::rest =>
- continue thyname' thmname' false rest
- | (AbortReplay (thyname',thmname'))::rest =>
- continue thyname' thmname' true rest
- | [] => (hs, [])
- | _ => raise CONV
- end
- | conv_histories ((Delta ds)::rest) = (conv_histories rest) |>> (fn hs => (DeltaEntry (rev ds))::hs)
- | conv_histories rest = ([], rest)
-
-fun conv es =
- let
- val (h, rest) = conv_histories (rev es)
- in
- case rest of
- [] => h
- | _ => raise CONV
- end
-
-fun get_history () = History (conv (!history))
-
-fun reconv (History hs) rs = fold reconv_entry hs rs
-and reconv_entry (ThmEntry (thyname, thmname, aborted, h)) rs =
- ((if aborted then AbortReplay else StopReplay) (thyname, thmname)) :: (reconv h ((StartReplay (thyname, thmname))::rs))
- | reconv_entry (DeltaEntry ds) rs = (Delta (rev ds))::rs
-
-fun set_history h = history := reconv h []
-
-
-end
--- a/src/HOL/Import/lazy_seq.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,551 +0,0 @@
-(* Title: HOL/Import/lazy_seq.ML
- Author: Sebastian Skalberg, TU Muenchen
-
-Alternative version of lazy sequences.
-*)
-
-signature LAZY_SEQ =
-sig
-
- include EXTENDED_SCANNER_SEQ
-
- (* From LIST *)
-
- val fromString : string -> string seq
- val @ : 'a seq * 'a seq -> 'a seq
- val hd : 'a seq -> 'a
- val tl : 'a seq -> 'a seq
- val last : 'a seq -> 'a
- val getItem : 'a seq -> ('a * 'a seq) option
- val nth : 'a seq * int -> 'a
- val take : 'a seq * int -> 'a seq
- val drop : 'a seq * int -> 'a seq
- val rev : 'a seq -> 'a seq
- val concat : 'a seq seq -> 'a seq
- val revAppend : 'a seq * 'a seq -> 'a seq
- val app : ('a -> unit) -> 'a seq -> unit
- val map : ('a -> 'b) -> 'a seq -> 'b seq
- val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
- val find : ('a -> bool) -> 'a seq -> 'a option
- val filter : ('a -> bool) -> 'a seq -> 'a seq
- val partition : ('a -> bool)
- -> 'a seq -> 'a seq * 'a seq
- val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
- val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
- val exists : ('a -> bool) -> 'a seq -> bool
- val all : ('a -> bool) -> 'a seq -> bool
- val tabulate : int * (int -> 'a) -> 'a seq
- val collate : ('a * 'a -> order)
- -> 'a seq * 'a seq -> order
-
- (* Miscellaneous *)
-
- val cycle : ((unit ->'a seq) -> 'a seq) -> 'a seq
- val iterates : ('a -> 'a) -> 'a -> 'a seq
- val of_function: (unit -> 'a option) -> 'a seq
- val of_string : string -> char seq
- val of_instream: TextIO.instream -> char seq
-
- (* From SEQ *)
-
- val make: (unit -> ('a * 'a seq) option) -> 'a seq
- val empty: 'a -> 'a seq
- val cons: 'a * 'a seq -> 'a seq
- val single: 'a -> 'a seq
- val try: ('a -> 'b) -> 'a -> 'b seq
- val chop: int * 'a seq -> 'a list * 'a seq
- val list_of: 'a seq -> 'a list
- val of_list: 'a list -> 'a seq
- val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
- val interleave: 'a seq * 'a seq -> 'a seq
- val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
- val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
- val commute: 'a seq list -> 'a list seq
- val succeed: 'a -> 'a seq
- val fail: 'a -> 'b seq
- val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
- val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
- val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
- val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
- val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
- val TRY: ('a -> 'a seq) -> 'a -> 'a seq
- val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
- val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
- val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
- val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
-
-end
-
-structure LazySeq :> LAZY_SEQ =
-struct
-
-datatype 'a seq = Seq of ('a * 'a seq) option lazy
-
-exception Empty
-
-fun getItem (Seq s) = Lazy.force s
-val pull = getItem
-fun make f = Seq (Lazy.lazy f)
-
-fun null s = is_none (getItem s)
-
-local
- fun F n NONE = n
- | F n (SOME(_,s)) = F (n+1) (getItem s)
-in
-fun length s = F 0 (getItem s)
-end
-
-fun s1 @ s2 =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(x,F' s1')
- and F' s = make (fn () => F (getItem s))
- in
- F' s1
- end
-
-local
- fun F NONE = raise Empty
- | F (SOME arg) = arg
-in
-fun hd s = #1 (F (getItem s))
-fun tl s = #2 (F (getItem s))
-end
-
-local
- fun F x NONE = x
- | F _ (SOME(x,s)) = F x (getItem s)
- fun G NONE = raise Empty
- | G (SOME(x,s)) = F x (getItem s)
-in
-fun last s = G (getItem s)
-end
-
-local
- fun F NONE _ = raise Subscript
- | F (SOME(x,_)) 0 = x
- | F (SOME(_,s)) n = F (getItem s) (n-1)
-in
-fun nth(s,n) =
- if n < 0
- then raise Subscript
- else F (getItem s) n
-end
-
-local
- fun F NONE _ = raise Subscript
- | F (SOME(x,s)) n = SOME(x,F' s (n-1))
- and F' s 0 = Seq (Lazy.value NONE)
- | F' s n = make (fn () => F (getItem s) n)
-in
-fun take (s,n) =
- if n < 0
- then raise Subscript
- else F' s n
-end
-
-fun take_at_most s n =
- if n <= 0 then [] else
- case getItem s of
- NONE => []
- | SOME (x,s') => x::(take_at_most s' (n-1))
-
-local
- fun F s 0 = s
- | F NONE _ = raise Subscript
- | F (SOME(_,s)) n = F (getItem s) (n-1)
-in
-fun drop (s,0) = s
- | drop (s,n) =
- if n < 0
- then raise Subscript
- else make (fn () => F (getItem s) n)
-end
-
-local
- fun F s NONE = s
- | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
-in
-fun rev s = make (fn () => F NONE (getItem s))
-end
-
-local
- fun F s NONE = getItem s
- | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
-in
-fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
-end
-
-local
- fun F NONE = NONE
- | F (SOME(s1,s2)) =
- let
- fun G NONE = F (getItem s2)
- | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
- in
- G (getItem s1)
- end
-in
-fun concat s = make (fn () => F (getItem s))
-end
-
-fun app f =
- let
- fun F NONE = ()
- | F (SOME(x,s)) =
- (f x;
- F (getItem s))
- in
- F o getItem
- end
-
-fun map f =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) = SOME(f x,F' s)
- and F' s = make (fn() => F (getItem s))
- in
- F'
- end
-
-fun mapPartial f =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- (case f x of
- SOME y => SOME(y,F' s)
- | NONE => F (getItem s))
- and F' s = make (fn()=> F (getItem s))
- in
- F'
- end
-
-fun find P =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- if P x
- then SOME x
- else F (getItem s)
- in
- F o getItem
- end
-
-(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
-
-fun filter P =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- if P x
- then SOME(x,F' s)
- else F (getItem s)
- and F' s = make (fn () => F (getItem s))
- in
- F'
- end
-
-fun partition f s =
- let
- val s' = map (fn x => (x,f x)) s
- in
- (mapPartial (fn (x,true) => SOME x | _ => NONE) s',
- mapPartial (fn (x,false) => SOME x | _ => NONE) s')
- end
-
-fun exists P =
- let
- fun F NONE = false
- | F (SOME(x,s)) = P x orelse F (getItem s)
- in
- F o getItem
- end
-
-fun all P =
- let
- fun F NONE = true
- | F (SOME(x,s)) = P x andalso F (getItem s)
- in
- F o getItem
- end
-
-(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
-
-fun tabulate (n,f) =
- let
- fun F n = make (fn () => SOME(f n,F (n+1)))
- in
- F n
- end
-
-fun collate c (s1,s2) =
- let
- fun F NONE _ = LESS
- | F _ NONE = GREATER
- | F (SOME(x,s1)) (SOME(y,s2)) =
- (case c (x,y) of
- LESS => LESS
- | GREATER => GREATER
- | EQUAL => F' s1 s2)
- and F' s1 s2 = F (getItem s1) (getItem s2)
- in
- F' s1 s2
- end
-
-fun empty _ = Seq (Lazy.value NONE)
-fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
-fun cons a = Seq(Lazy.value (SOME a))
-
-fun cycle seqfn =
- let
- val knot = Unsynchronized.ref (Seq (Lazy.value NONE))
- in
- knot := seqfn (fn () => !knot);
- !knot
- end
-
-fun iterates f =
- let
- fun F x = make (fn() => SOME(x,F (f x)))
- in
- F
- end
-
-fun interleave (s1,s2) =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
- in
- make (fn()=> F (getItem s1))
- end
-
-(* val force_all = app ignore *)
-
-local
- fun F NONE = ()
- | F (SOME(x,s)) = F (getItem s)
-in
-fun force_all s = F (getItem s)
-end
-
-fun of_function f =
- let
- fun F () = case f () of
- SOME x => SOME(x,make F)
- | NONE => NONE
- in
- make F
- end
-
-local
- fun F [] = NONE
- | F (x::xs) = SOME(x,F' xs)
- and F' xs = make (fn () => F xs)
-in
-fun of_list xs = F' xs
-end
-
-val of_string = of_list o String.explode
-
-fun of_instream is =
- let
- val buffer : char list Unsynchronized.ref = Unsynchronized.ref []
- fun get_input () =
- case !buffer of
- (c::cs) => (buffer:=cs;
- SOME c)
- | [] => (case String.explode (TextIO.input is) of
- [] => NONE
- | (c::cs) => (buffer := cs;
- SOME c))
- in
- of_function get_input
- end
-
-local
- fun F k NONE = k []
- | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
-in
-fun list_of s = F (fn x => x) (getItem s)
-end
-
-(* Adapted from seq.ML *)
-
-val succeed = single
-fun fail _ = Seq (Lazy.value NONE)
-
-(* fun op THEN (f, g) x = flat (map g (f x)) *)
-
-fun op THEN (f, g) =
- let
- fun F NONE = NONE
- | F (SOME(x,xs)) =
- let
- fun G NONE = F (getItem xs)
- | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
- in
- G (getItem (g x))
- end
- in
- fn x => make (fn () => F (getItem (f x)))
- end
-
-fun op ORELSE (f, g) x =
- make (fn () =>
- case getItem (f x) of
- NONE => getItem (g x)
- | some => some)
-
-fun op APPEND (f, g) x =
- let
- fun copy s =
- case getItem s of
- NONE => getItem (g x)
- | SOME(x,xs) => SOME(x,make (fn () => copy xs))
- in
- make (fn () => copy (f x))
- end
-
-fun EVERY fs = fold_rev (curry op THEN) fs succeed
-fun FIRST fs = fold_rev (curry op ORELSE) fs fail
-
-fun TRY f x =
- make (fn () =>
- case getItem (f x) of
- NONE => SOME(x,Seq (Lazy.value NONE))
- | some => some)
-
-fun REPEAT f =
- let
- fun rep qs x =
- case getItem (f x) of
- NONE => SOME(x, make (fn () => repq qs))
- | SOME (x', q) => rep (q :: qs) x'
- and repq [] = NONE
- | repq (q :: qs) =
- case getItem q of
- NONE => repq qs
- | SOME (x, q) => rep (q :: qs) x
- in
- fn x => make (fn () => rep [] x)
- end
-
-fun REPEAT1 f = op THEN (f, REPEAT f);
-
-fun INTERVAL f i =
- let
- fun F j =
- if i > j
- then single
- else op THEN (f j, F (j - 1))
- in F end
-
-fun DETERM f x =
- make (fn () =>
- case getItem (f x) of
- NONE => NONE
- | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
-
-(*partial function as procedure*)
-fun try f x =
- make (fn () =>
- case Basics.try f x of
- SOME y => SOME(y,Seq (Lazy.value NONE))
- | NONE => NONE)
-
-(*functional to print a sequence, up to "count" elements;
- the function prelem should print the element number and also the element*)
-fun print prelem count seq =
- let
- fun pr k xq =
- if k > count
- then ()
- else
- case getItem xq of
- NONE => ()
- | SOME (x, xq') =>
- (prelem k x;
- writeln "";
- pr (k + 1) xq')
- in
- pr 1 seq
- end
-
-(*accumulating a function over a sequence; this is lazy*)
-fun it_right f (xq, yq) =
- let
- fun its s =
- make (fn () =>
- case getItem s of
- NONE => getItem yq
- | SOME (a, s') => getItem(f (a, its s')))
- in
- its xq
- end
-
-(*map over a sequence s1, append the sequence s2*)
-fun mapp f s1 s2 =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(f x,F' s1')
- and F' s = make (fn () => F (getItem s))
- in
- F' s1
- end
-
-(*turn a list of sequences into a sequence of lists*)
-local
- fun F [] = SOME([],Seq (Lazy.value NONE))
- | F (xq :: xqs) =
- case getItem xq of
- NONE => NONE
- | SOME (x, xq') =>
- (case F xqs of
- NONE => NONE
- | SOME (xs, xsq) =>
- let
- fun G s =
- make (fn () =>
- case getItem s of
- NONE => F (xq' :: xqs)
- | SOME(ys,ysq) => SOME(x::ys,G ysq))
- in
- SOME (x :: xs, G xsq)
- end)
-in
-fun commute xqs = make (fn () => F xqs)
-end
-
-(*the list of the first n elements, paired with rest of sequence;
- if length of list is less than n, then sequence had less than n elements*)
-fun chop (n, xq) =
- if n <= 0
- then ([], xq)
- else
- case getItem xq of
- NONE => ([], xq)
- | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
-
-fun foldl f e s =
- let
- fun F k NONE = k e
- | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
- in
- F (fn x => x) (getItem s)
- end
-
-fun foldr f e s =
- let
- fun F e NONE = e
- | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
- in
- F e (getItem s)
- end
-
-fun fromString s = of_list (raw_explode s)
-
-end
-
-structure LazyScan = Scanner (structure Seq = LazySeq)
-
--- a/src/HOL/Import/mono_scan.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(* Title: HOL/Import/mono_scan.ML
- Author: Steven Obua, TU Muenchen
-
-Monomorphic scanner combinators for monomorphic sequences.
-*)
-
-signature MONO_SCANNER =
-sig
-
- include MONO_SCANNER_SEQ
-
- exception SyntaxError
-
- type 'a scanner = seq -> 'a * seq
-
- val :-- : 'a scanner * ('a -> 'b scanner)
- -> ('a*'b) scanner
- val -- : 'a scanner * 'b scanner -> ('a * 'b) scanner
- val >> : 'a scanner * ('a -> 'b) -> 'b scanner
- val --| : 'a scanner * 'b scanner -> 'a scanner
- val |-- : 'a scanner * 'b scanner -> 'b scanner
- val ^^ : string scanner * string scanner
- -> string scanner
- val || : 'a scanner * 'a scanner -> 'a scanner
- val one : (item -> bool) -> item scanner
- val anyone : item scanner
- val succeed : 'a -> 'a scanner
- val any : (item -> bool) -> item list scanner
- val any1 : (item -> bool) -> item list scanner
- val optional : 'a scanner -> 'a -> 'a scanner
- val option : 'a scanner -> 'a option scanner
- val repeat : 'a scanner -> 'a list scanner
- val repeat1 : 'a scanner -> 'a list scanner
- val repeat_fixed : int -> 'a scanner -> 'a list scanner
- val ahead : 'a scanner -> 'a scanner
- val unless : 'a scanner -> 'b scanner -> 'b scanner
- val !! : (seq -> string) -> 'a scanner -> 'a scanner
-
-end
-
-signature STRING_SCANNER =
-sig
-
- include MONO_SCANNER where type item = string
-
- val $$ : item -> item scanner
-
- val scan_id : string scanner
- val scan_nat : int scanner
-
- val this : item list -> item list scanner
- val this_string : string -> string scanner
-
-end
-
-functor MonoScanner (structure Seq : MONO_SCANNER_SEQ) : MONO_SCANNER =
-struct
-
-infix 7 |-- --|
-infix 5 :-- -- ^^
-infix 3 >>
-infix 0 ||
-
-exception SyntaxError
-exception Fail of string
-
-type seq = Seq.seq
-type item = Seq.item
-type 'a scanner = seq -> 'a * seq
-
-val pull = Seq.pull
-
-fun (sc1 :-- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 x toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc1 -- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc >> f) toks =
- let
- val (x,toks2) = sc toks
- in
- (f x,toks2)
- end
-
-fun (sc1 --| sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (_,toks3) = sc2 toks2
- in
- (x,toks3)
- end
-
-fun (sc1 |-- sc2) toks =
- let
- val (_,toks2) = sc1 toks
- in
- sc2 toks2
- end
-
-fun (sc1 ^^ sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- (x^y,toks3)
- end
-
-fun (sc1 || sc2) toks =
- (sc1 toks)
- handle SyntaxError => sc2 toks
-
-fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
-
-fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
-
-fun succeed e toks = (e,toks)
-
-fun any p toks =
- case pull toks of
- NONE => ([],toks)
- | SOME(x,toks2) => if p x
- then
- let
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
- else ([],toks)
-
-fun any1 p toks =
- let
- val (x,toks2) = one p toks
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
-
-fun optional sc def = sc || succeed def
-fun option sc = (sc >> SOME) || succeed NONE
-
-(*
-fun repeat sc =
- let
- fun R toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = R toks2
- in
- (x::xs,toks3)
- end
- handle SyntaxError => ([],toks)
- in
- R
- end
-*)
-
-(* A tail-recursive version of repeat. It is (ever so) slightly slower
- * than the above, non-tail-recursive version (due to the garbage generation
- * associated with the reversal of the list). However, this version will be
- * able to process input where the former version must give up (due to stack
- * overflow). The slowdown seems to be around the one percent mark.
- *)
-fun repeat sc =
- let
- fun R xs toks =
- case SOME (sc toks) handle SyntaxError => NONE of
- SOME (x,toks2) => R (x::xs) toks2
- | NONE => (List.rev xs,toks)
- in
- R []
- end
-
-fun repeat1 sc toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = repeat sc toks2
- in
- (x::xs,toks3)
- end
-
-fun repeat_fixed n sc =
- let
- fun R n xs toks =
- if (n <= 0) then (List.rev xs, toks)
- else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
- in
- R n []
- end
-
-fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
-
-fun unless test sc toks =
- let
- val test_failed = (test toks;false) handle SyntaxError => true
- in
- if test_failed
- then sc toks
- else raise SyntaxError
- end
-
-fun !! f sc toks = (sc toks
- handle SyntaxError => raise Fail (f toks))
-
-end
-
-
-structure StringScanner : STRING_SCANNER =
-struct
-
-structure Scan = MonoScanner(structure Seq = StringScannerSeq)
-open Scan
-
-fun $$ arg = one (fn x => x = arg)
-
-val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
-
-val nat_of_list = the o Int.fromString o implode
-
-val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list
-
-fun this [] = (fn toks => ([], toks))
- | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
-
-fun this_string s = this (raw_explode s) >> K s
-
-end
\ No newline at end of file
--- a/src/HOL/Import/mono_seq.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: HOL/Import/mono_seq.ML
- Author: Steven Obua, TU Muenchen
-
-Monomorphic sequences.
-*)
-
-(* The trouble is that signature / structures cannot depend on type variable parameters ... *)
-
-signature MONO_SCANNER_SEQ =
-sig
- type seq
- type item
-
- val pull : seq -> (item * seq) option
-end
-
-signature MONO_EXTENDED_SCANNER_SEQ =
-sig
-
- include MONO_SCANNER_SEQ
-
- val null : seq -> bool
- val length : seq -> int
- val take_at_most : seq -> int -> item list
-
-end
-
-functor MonoExtendScannerSeq (structure Seq : MONO_SCANNER_SEQ) : MONO_EXTENDED_SCANNER_SEQ =
-struct
-
-type seq = Seq.seq
-type item = Seq.item
-val pull = Seq.pull
-
-fun null s = is_none (pull s)
-
-fun take_at_most s n =
- if n <= 0 then [] else
- case pull s of
- NONE => []
- | SOME (x,s') => x::(take_at_most s' (n-1))
-
-fun length' s n =
- case pull s of
- NONE => n
- | SOME (_, s') => length' s' (n+1)
-
-fun length s = length' s 0
-
-end
-
-
-structure StringScannerSeq :
- sig
- include MONO_EXTENDED_SCANNER_SEQ
- val fromString : string -> seq
- end
- =
-struct
-
-structure Incubator : MONO_SCANNER_SEQ =
-struct
-
-type seq = string * int * int
-type item = string
-
-fun pull (s, len, i) = if i >= len then NONE else SOME (String.substring (s, i, 1), (s, len, i+1))
-end
-
-structure Extended = MonoExtendScannerSeq (structure Seq = Incubator)
-open Extended
-
-fun fromString s = (s, String.size s, 0)
-
-end
-
--- a/src/HOL/Import/proof_kernel.ML Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Jul 20 10:11:08 2011 +0200
@@ -129,7 +129,7 @@
fun to_hol_thm th = HOLThm ([], th)
val replay_add_dump = add_dump
-fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
+fun add_dump s thy = replay_add_dump s thy
datatype proof_info
= Info of {disk_info: (string * string) option Unsynchronized.ref}
@@ -303,85 +303,14 @@
handle PK _ => thyname)
val get_name : (string * string) list -> string = Lib.assoc "n"
-local
- open LazyScan
- infix 7 |-- --|
- infix 5 :-- -- ^^
- infix 3 >>
- infix 0 ||
-in
exception XML of string
datatype xml = Elem of string * (string * string) list * xml list
datatype XMLtype = XMLty of xml | FullType of hol_type
datatype XMLterm = XMLtm of xml | FullTerm of term
-fun pair x y = (x,y)
-
-fun scan_id toks =
- let
- val (x,toks2) = one Char.isAlpha toks
- val (xs,toks3) = any Char.isAlphaNum toks2
- in
- (String.implode (x::xs),toks3)
- end
-
-fun scan_string str c =
- let
- fun F [] toks = (c,toks)
- | F (c::cs) toks =
- case LazySeq.getItem toks of
- SOME(c',toks') =>
- if c = c'
- then F cs toks'
- else raise SyntaxError
- | NONE => raise SyntaxError
- in
- F (String.explode str)
- end
-
-local
- val scan_entity =
- (scan_string "amp;" #"&")
- || scan_string "quot;" #"\""
- || scan_string "gt;" #">"
- || scan_string "lt;" #"<"
- || scan_string "apos;" #"'"
-in
-fun scan_nonquote toks =
- case LazySeq.getItem toks of
- SOME (c,toks') =>
- (case c of
- #"\"" => raise SyntaxError
- | #"&" => scan_entity toks'
- | c => (c,toks'))
- | NONE => raise SyntaxError
-end
-
-val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
- String.implode
-
-val scan_attribute = scan_id -- $$ #"=" |-- scan_string
-
-val scan_start_of_tag = $$ #"<" |-- scan_id --
- repeat ($$ #" " |-- scan_attribute)
-
-fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
-
-val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
-
-fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
- (fn (chldr,id') => if id = id'
- then chldr
- else raise XML "Tag mismatch")
-and scan_tag toks =
- let
- val ((id,atts),toks2) = scan_start_of_tag toks
- val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
- in
- (Elem (id,atts,chldr),toks3)
- end
-end
+fun xml_to_import_xml (XML.Elem ((n, l), ts)) = Elem (n, l, map xml_to_import_xml ts)
+ | xml_to_import_xml (XML.Text _) = raise XML "Incorrect proof file: text";
val type_of = Term.type_of
@@ -473,7 +402,6 @@
let
val _ = Unsynchronized.inc invented_isavar
val t = "u_" ^ string_of_int (!invented_isavar)
- val _ = ImportRecorder.protect_varname s t
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
in
t
@@ -927,7 +855,7 @@
fun import_proof_concl thyname thmname thy =
let
val is = TextIO.openIn(proof_file_name thyname thmname thy)
- val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
+ val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
val _ = TextIO.closeIn is
in
case proof_xml of
@@ -948,7 +876,7 @@
fun import_proof thyname thmname thy =
let
val is = TextIO.openIn(proof_file_name thyname thmname thy)
- val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
+ val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
val _ = TextIO.closeIn is
in
case proof_xml of
@@ -1292,8 +1220,6 @@
val hth as HOLThm args = mk_res th
val thy' = thy |> add_hol4_theorem thyname thmname args
|> add_hol4_mapping thyname thmname isaname
- val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
- val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
in
(thy',SOME hth)
end
@@ -1364,7 +1290,6 @@
val rew = rewrite_hol4_term (concl_of th) thy
val th = Thm.equal_elim rew th
val thy' = add_hol4_pending thyname thmname args thy
- val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val th = disambiguate_frees th
val th = Object_Logic.rulify th
val thy2 =
@@ -1920,17 +1845,14 @@
val csyn = mk_syn thy constname
val thy1 = case HOL4DefThy.get thy of
Replaying _ => thy
- | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
- Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
+ | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy
val eq = mk_defeq constname rhs' thy1
val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
- val _ = ImportRecorder.add_defs thmname eq
val def_thm = hd thms
val thm' = def_thm RS meta_eq_to_obj_eq_thm
val (thy',th) = (thy2, thm')
val fullcname = Sign.intern_const thy' constname
val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
- val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
val rew = rewrite_hol4_term eq thy''
val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
@@ -1958,13 +1880,10 @@
| NONE => raise ERR "new_definition" "Bad conclusion"
val fullname = Sign.full_bname thy22 thmname
val thy22' = case opt_get_output_thy thy22 of
- "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
- add_hol4_mapping thyname thmname fullname thy22)
+ "" => add_hol4_mapping thyname thmname fullname thy22
| output_thy =>
let
val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
- val _ = ImportRecorder.add_hol_move fullname moved_thmname
- val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
in
thy22 |> add_hol4_move fullname moved_thmname
|> add_hol4_mapping thyname thmname moved_thmname
@@ -2012,7 +1931,6 @@
acc ^ "\n " ^ quotename c ^ " :: \"" ^
Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
val thy' = add_dump str thy
- val _ = ImportRecorder.add_consts consts
in
Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
end
@@ -2024,7 +1942,6 @@
val (thy',res) = Choice_Specification.add_specification NONE
names'
(thy1,th)
- val _ = ImportRecorder.add_specification names' th
val res' = Thm.unvarify_global res
val hth = HOLThm(rens,res')
val rew = rewrite_hol4_term (concl_of res') thy'
@@ -2092,19 +2009,16 @@
val ((_, typedef_info), thy') =
Typedef.add_typedef_global false (SOME (Binding.name thmname))
(Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
- val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
val fulltyname = Sign.intern_type thy' tycname
val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
- val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
else ()
val thy4 = add_hol4_pending thyname thmname args thy''
- val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val rew = rewrite_hol4_term (concl_of td_th) thy4
val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
@@ -2169,7 +2083,6 @@
Typedef.add_typedef_global false NONE
(Binding.name tycname, map (rpair dummyS) tnames, tsyn) c
(SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
- val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
val fulltyname = Sign.intern_type thy' tycname
val aty = Type (fulltyname, map mk_vartype tnames)
val abs_ty = tT --> aty
@@ -2186,11 +2099,9 @@
raise ERR "type_introduction" "no term variables expected any more"
val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
- val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
val _ = message "step 4"
val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
val thy4 = add_hol4_pending thyname thmname args thy''
- val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
val c =
--- a/src/HOL/Import/replay.ML Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/Import/replay.ML Wed Jul 20 10:11:08 2011 +0200
@@ -6,7 +6,6 @@
struct
open ProofKernel
-open ImportRecorder
exception REPLAY of string * string
fun ERR f mesg = REPLAY (f,mesg)
@@ -14,7 +13,6 @@
fun replay_proof int_thms thyname thmname prf thy =
let
- val _ = ImportRecorder.start_replay_proof thyname thmname
fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
| rp (PInstT(p,lambda)) thy =
let
@@ -269,13 +267,8 @@
| _ => rp pc thy
end
in
- let
- val x = rp' prf thy
- val _ = ImportRecorder.stop_replay_proof thyname thmname
- in
- x
- end
- end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x) (* FIXME avoid handle x ?? *)
+ rp' prf thy
+ end
fun setup_int_thms thyname thy =
let
@@ -316,74 +309,8 @@
replay_fact (thmname,thy)
end
-fun replay_chached_thm int_thms thyname thmname =
- let
- fun th_of thy = Skip_Proof.make_thm thy
- fun err msg = raise ERR "replay_cached_thm" msg
- val _ = writeln ("Replaying (from cache) "^thmname^" ...")
- fun rps [] thy = thy
- | rps (t::ts) thy = rps ts (rp t thy)
- and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy
- | rp (DeltaEntry ds) thy = fold delta ds thy
- and delta (Specification (names, th)) thy =
- fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
- | delta (Hol_mapping (thyname, thmname, isaname)) thy =
- add_hol4_mapping thyname thmname isaname thy
- | delta (Hol_pending (thyname, thmname, th)) thy =
- add_hol4_pending thyname thmname ([], th_of thy th) thy
- | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
- | delta (Hol_const_mapping (thyname, constname, fullcname)) thy =
- add_hol4_const_mapping thyname constname true fullcname thy
- | delta (Hol_move (fullname, moved_thmname)) thy =
- add_hol4_move fullname moved_thmname thy
- | delta (Defs (thmname, eq)) thy =
- snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
- | delta (Hol_theorem (thyname, thmname, th)) thy =
- add_hol4_theorem thyname thmname ([], th_of thy th) thy
- | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =
- snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
- (Binding.name t, map (rpair dummyS) vs, mx) c
- (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
- | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
- add_hol4_type_mapping thyname tycname true fulltyname thy
- | delta (Indexed_theorem (i, th)) thy =
- (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)
- | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
- | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
- in
- rps
- end
-
fun import_thms thyname int_thms thmnames thy =
let
- fun zip names [] = ([], names)
- | zip [] _ = ([], [])
- | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) =
- if thyname = thyname' andalso thmname = thmname' then
- (if aborted then ([], thmname::names) else
- let
- val _ = writeln ("theorem is in-sync: "^thmname)
- val (cached,normal) = zip names ys
- in
- (entry::cached, normal)
- end)
- else
- let
- val _ = writeln ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
- val _ = writeln ("proceeding with next uncached theorem...")
- in
- ([], thmname::names)
- end
- (* raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
- | zip (thmname::_) (DeltaEntry _ :: _) =
- raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
- fun zip' xs (History ys) =
- let
- val _ = writeln ("length of xs: "^(string_of_int (length xs)))
- val _ = writeln ("length of history: "^(string_of_int (length ys)))
- in
- zip xs ys
- end
fun replay_fact thmname thy =
let
val prf = mk_proof PDisk
@@ -393,10 +320,7 @@
in
p
end
- fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
- val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
- val _ = ImportRecorder.set_history (History (map ThmEntry cached))
- val res_thy = fold replay_fact normal (fold replay_cache cached thy)
+ val res_thy = fold replay_fact thmnames thy
in
res_thy
end
--- a/src/HOL/Import/scan.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,219 +0,0 @@
-(* Title: HOL/Import/scan.ML
- Author: Sebastian Skalberg, TU Muenchen / Steven Obua, TU Muenchen
-
-Scanner combinators for sequences.
-*)
-
-signature SCANNER =
-sig
-
- include SCANNER_SEQ
-
- exception SyntaxError
-
- type ('a,'b) scanner = 'a seq -> 'b * 'a seq
-
- val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner)
- -> ('a,'b*'c) scanner
- val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
- val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
- val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
- val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
- val ^^ : ('a,string) scanner * ('a,string) scanner
- -> ('a,string) scanner
- val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
- val one : ('a -> bool) -> ('a,'a) scanner
- val anyone : ('a,'a) scanner
- val succeed : 'b -> ('a,'b) scanner
- val any : ('a -> bool) -> ('a,'a list) scanner
- val any1 : ('a -> bool) -> ('a,'a list) scanner
- val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
- val option : ('a,'b) scanner -> ('a,'b option) scanner
- val repeat : ('a,'b) scanner -> ('a,'b list) scanner
- val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
- val repeat_fixed : int -> ('a, 'b) scanner -> ('a, 'b list) scanner
- val ahead : ('a,'b) scanner -> ('a,'b) scanner
- val unless : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
- val $$ : ''a -> (''a,''a) scanner
- val !! : ('a seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
-
- val scan_id : (string, string) scanner
- val scan_nat : (string, int) scanner
-
- val this : ''a list -> (''a, ''a list) scanner
- val this_string : string -> (string, string) scanner
-end
-
-functor Scanner (structure Seq : SCANNER_SEQ) : SCANNER =
-struct
-
-infix 7 |-- --|
-infix 5 :-- -- ^^
-infix 3 >>
-infix 0 ||
-
-exception SyntaxError
-exception Fail of string
-
-type 'a seq = 'a Seq.seq
-type ('a,'b) scanner = 'a seq -> 'b * 'a seq
-
-val pull = Seq.pull
-
-fun (sc1 :-- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 x toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc1 -- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc >> f) toks =
- let
- val (x,toks2) = sc toks
- in
- (f x,toks2)
- end
-
-fun (sc1 --| sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (_,toks3) = sc2 toks2
- in
- (x,toks3)
- end
-
-fun (sc1 |-- sc2) toks =
- let
- val (_,toks2) = sc1 toks
- in
- sc2 toks2
- end
-
-fun (sc1 ^^ sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- (x^y,toks3)
- end
-
-fun (sc1 || sc2) toks =
- (sc1 toks)
- handle SyntaxError => sc2 toks
-
-fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
-
-fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
-
-fun succeed e toks = (e,toks)
-
-fun any p toks =
- case pull toks of
- NONE => ([],toks)
- | SOME(x,toks2) => if p x
- then
- let
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
- else ([],toks)
-
-fun any1 p toks =
- let
- val (x,toks2) = one p toks
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
-
-fun optional sc def = sc || succeed def
-fun option sc = (sc >> SOME) || succeed NONE
-
-(*
-fun repeat sc =
- let
- fun R toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = R toks2
- in
- (x::xs,toks3)
- end
- handle SyntaxError => ([],toks)
- in
- R
- end
-*)
-
-(* A tail-recursive version of repeat. It is (ever so) slightly slower
- * than the above, non-tail-recursive version (due to the garbage generation
- * associated with the reversal of the list). However, this version will be
- * able to process input where the former version must give up (due to stack
- * overflow). The slowdown seems to be around the one percent mark.
- *)
-fun repeat sc =
- let
- fun R xs toks =
- case SOME (sc toks) handle SyntaxError => NONE of
- SOME (x,toks2) => R (x::xs) toks2
- | NONE => (List.rev xs,toks)
- in
- R []
- end
-
-fun repeat1 sc toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = repeat sc toks2
- in
- (x::xs,toks3)
- end
-
-fun repeat_fixed n sc =
- let
- fun R n xs toks =
- if (n <= 0) then (List.rev xs, toks)
- else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
- in
- R n []
- end
-
-fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
-
-fun unless test sc toks =
- let
- val test_failed = (test toks;false) handle SyntaxError => true
- in
- if test_failed
- then sc toks
- else raise SyntaxError
- end
-
-fun $$ arg = one (fn x => x = arg)
-
-fun !! f sc toks = (sc toks
- handle SyntaxError => raise Fail (f toks))
-
-val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
-
-val nat_of_list = the o Int.fromString o implode
-
-val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list
-
-fun this [] = (fn toks => ([], toks))
- | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
-
-fun this_string s = this (raw_explode s) >> K s
-
-end
-
--- a/src/HOL/Import/seq.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-signature SCANNER_SEQ =
-sig
- type 'a seq
-
- val pull : 'a seq -> ('a * 'a seq) option
-end
-
-signature EXTENDED_SCANNER_SEQ =
-sig
-
- include SCANNER_SEQ
-
- val null : 'a seq -> bool
- val length : 'a seq -> int
- val take_at_most : 'a seq -> int -> 'a list
-
-end
-
-functor ExtendScannerSeq (structure Seq : SCANNER_SEQ) : EXTENDED_SCANNER_SEQ =
-struct
-
-type 'a seq = 'a Seq.seq
-
-val pull = Seq.pull
-
-fun null s = is_none (pull s)
-
-fun take_at_most s n =
- if n <= 0 then [] else
- case pull s of
- NONE => []
- | SOME (x,s') => x::(take_at_most s' (n-1))
-
-fun length' s n =
- case pull s of
- NONE => n
- | SOME (_, s') => length' s' (n+1)
-
-fun length s = length' s 0
-
-end
-
-signature VECTOR_SCANNER_SEQ =
-sig
- include EXTENDED_SCANNER_SEQ
-
- val fromString : string -> string seq
- val fromVector : 'a Vector.vector -> 'a seq
-end
-
-structure VectorScannerSeq :> VECTOR_SCANNER_SEQ =
-struct
-
-structure Incubator : SCANNER_SEQ =
-struct
-
-type 'a seq = 'a Vector.vector * int * int
-fun pull (v, len, i) = if i >= len then NONE else SOME (Vector.sub (v, i), (v, len, i+1))
-
-end
-
-structure Extended = ExtendScannerSeq (structure Seq = Incubator)
-
-open Extended
-
-fun fromVector v = (v, Vector.length v, 0)
-fun vector_from_string s = Vector.tabulate (String.size s, fn i => String.str (String.sub (s, i)))
-fun fromString s = fromVector (vector_from_string s)
-
-end
-
-signature LIST_SCANNER_SEQ =
-sig
- include EXTENDED_SCANNER_SEQ
-
- val fromString : string -> string seq
- val fromList : 'a list -> 'a seq
-end
-
-structure ListScannerSeq :> LIST_SCANNER_SEQ =
-struct
-
-structure Incubator : SCANNER_SEQ =
-struct
-
-type 'a seq = 'a list
-fun pull [] = NONE
- | pull (x::xs) = SOME (x, xs)
-
-end
-
-structure Extended = ExtendScannerSeq (structure Seq = Incubator)
-
-open Extended
-
-val fromList = I
-val fromString = raw_explode
-
-end
--- a/src/HOL/Import/xml.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,199 +0,0 @@
-(* Title: HOL/Import/xml.ML
-
-Yet another version of XML support.
-*)
-
-signature XML =
-sig
- val header: string
- val text: string -> string
- val text_charref: string -> string
- val cdata: string -> string
- val element: string -> (string * string) list -> string list -> string
-
- datatype tree =
- Elem of string * (string * string) list * tree list
- | Text of string
-
- val string_of_tree: tree -> string
- val tree_of_string: string -> tree
-
- val encoded_string_of_tree : tree -> string
- val tree_of_encoded_string : string -> tree
-end;
-
-structure XML :> XML =
-struct
-
-(*structure Seq = VectorScannerSeq
-structure Scan = Scanner (structure Seq = Seq)*)
-structure Seq = StringScannerSeq
-structure Scan = StringScanner
-
-
-open Scan
-
-(** string based representation (small scale) **)
-
-val header = "<?xml version=\"1.0\"?>\n";
-
-(* text and character data *)
-
-fun decode "<" = "<"
- | decode ">" = ">"
- | decode "&" = "&"
- | decode "'" = "'"
- | decode """ = "\""
- | decode c = c;
-
-fun encode "<" = "<"
- | encode ">" = ">"
- | encode "&" = "&"
- | encode "'" = "'"
- | encode "\"" = """
- | encode c = c;
-
-fun encode_charref c = "&#" ^ string_of_int (ord c) ^ ";"
-
-val text = Library.translate_string encode
-
-val text_charref = translate_string encode_charref;
-
-val cdata = enclose "<![CDATA[" "]]>\n"
-
-(* elements *)
-
-fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
-
-fun element name atts cs =
- let val elem = space_implode " " (name :: map attribute atts) in
- if null cs then enclose "<" "/>" elem
- else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
- end;
-
-(** explicit XML trees **)
-
-datatype tree =
- Elem of string * (string * string) list * tree list
- | Text of string;
-
-fun string_of_tree tree =
- let
- fun string_of (Elem (name, atts, ts)) buf =
- let val buf' =
- buf |> Buffer.add "<"
- |> fold Buffer.add (separate " " (name :: map attribute atts))
- in
- if null ts then
- buf' |> Buffer.add "/>"
- else
- buf' |> Buffer.add ">"
- |> fold string_of ts
- |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
- end
- | string_of (Text s) buf = Buffer.add (text s) buf;
- in Buffer.content (string_of tree Buffer.empty) end;
-
-(** XML parsing **)
-
-fun beginning n xs = Symbol.beginning n (Seq.take_at_most xs n)
-
-fun err s xs =
- "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
-
-val scan_whspc = Scan.any Symbol.is_blank;
-
-val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
-
-val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
- (scan_special || Scan.one Symbol.is_regular)) >> implode;
-
-val parse_cdata = Scan.this_string "<![CDATA[" |--
- (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
- implode) --| Scan.this_string "]]>";
-
-val parse_att =
- scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
- (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
- (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
-
-val parse_comment = Scan.this_string "<!--" --
- Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
- Scan.this_string "-->";
-
-val scan_comment_whspc =
- (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
-
-val parse_pi = Scan.this_string "<?" |--
- Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
- Scan.this_string "?>";
-
-fun parse_content xs =
- ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
- (Scan.repeat ((* scan_whspc |-- *)
- ( parse_elem >> single
- || parse_cdata >> (single o Text)
- || parse_pi >> K []
- || parse_comment >> K []) --
- Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
- >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
-
-and parse_elem xs =
- ($$ "<" |-- scan_id --
- Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
- !! (err "Expected > or />")
- (Scan.this_string "/>" >> K []
- || $$ ">" |-- parse_content --|
- !! (err ("Expected </" ^ s ^ ">"))
- (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
- (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
-
-val parse_document =
- Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
- (Scan.repeat (Scan.unless ($$ ">")
- (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
- parse_elem;
-
-fun tree_of_string s =
- let
- val seq = Seq.fromString s
- val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
- val (x, toks) = scanner seq
- in
- if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
- end
-
-(* More efficient saving and loading of xml trees employing a proprietary external format *)
-
-fun write_lstring s buf = buf |> Buffer.add (string_of_int (size s)) |> Buffer.add " " |> Buffer.add s
-fun parse_lstring toks = (scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i (one (K true))) >> snd >> implode) toks
-
-fun write_list w l buf = buf |> Buffer.add (string_of_int (length l)) |> Buffer.add " " |> fold w l
-fun parse_list sc = scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i sc) >> snd
-
-fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
- | write_tree (Elem (name, attrs, children)) buf =
- buf |> Buffer.add "E"
- |> write_lstring name
- |> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs
- |> write_list write_tree children
-
-fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
-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
-
-fun encoded_string_of_tree tree = Buffer.content (write_tree tree Buffer.empty)
-
-fun tree_of_encoded_string s =
- let
- fun print (a,b) = writeln (a^" "^(string_of_int b))
- val _ = print ("length of encoded string: ", size s)
- val _ = writeln "Seq.fromString..."
- val seq = timeit (fn () => Seq.fromString s)
- val _ = print ("length of sequence", timeit (fn () => Seq.length seq))
- val scanner = !! (err "Malformed encoded xml") parse_tree
- val (x, toks) = scanner seq
- in
- if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
- end
-
-end;
--- a/src/HOL/Import/xmlconv.ML Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,303 +0,0 @@
-signature XML_CONV =
-sig
- type 'a input = XML.tree -> 'a
- type 'a output = 'a -> XML.tree
-
- exception ParseException of string
-
- val xml_of_typ: typ output
- val typ_of_xml: typ input
-
- val xml_of_term: term output
- val term_of_xml : term input
-
- val xml_of_mixfix: mixfix output
- val mixfix_of_xml: mixfix input
-
- val xml_of_proof: Proofterm.proof output
-
- val xml_of_bool: bool output
- val bool_of_xml: bool input
-
- val xml_of_int: int output
- val int_of_xml: int input
-
- val xml_of_string: string output
- val string_of_xml: string input
-
- val xml_of_list: 'a output -> 'a list output
- val list_of_xml: 'a input -> 'a list input
-
- val xml_of_tuple : 'a output -> 'a list output
- val tuple_of_xml: 'a input -> int -> 'a list input
-
- val xml_of_option: 'a output -> 'a option output
- val option_of_xml: 'a input -> 'a option input
-
- val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
- val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
-
- val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
- val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
-
- val xml_of_unit: unit output
- val unit_of_xml: unit input
-
- val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
- val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
-
- val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
- val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
-
- val wrap : string -> 'a output -> 'a output
- val unwrap : ('a -> 'b) -> 'a input -> 'b input
- val wrap_empty : string output
- val unwrap_empty : 'a -> 'a input
- val name_of_wrap : XML.tree -> string
-
- val write_to_file: 'a output -> string -> 'a -> unit
- val read_from_file: 'a input -> string -> 'a
-
- val serialize_to_file : 'a output -> string -> 'a -> unit
- val deserialize_from_file : 'a input -> string -> 'a
-end;
-
-structure XMLConv : XML_CONV =
-struct
-
-type 'a input = XML.tree -> 'a
-type 'a output = 'a -> XML.tree
-exception ParseException of string
-
-fun parse_err s = raise ParseException s
-
-fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
-
-fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
- | class_of_xml _ = parse_err "class"
-
-fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
- ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
- map xml_of_class S)
- | xml_of_typ (TFree (s, S)) =
- XML.Elem ("TFree", [("name", s)], map xml_of_class S)
- | xml_of_typ (Type (s, Ts)) =
- XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
-
-fun intofstr s i =
- case Int.fromString i of
- NONE => parse_err (s^", invalid index: "^i)
- | SOME i => i
-
-fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
- | typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) =
- TVar ((s, intofstr "TVar" i), map class_of_xml cs)
- | typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
- | typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
- | typ_of_xml _ = parse_err "type"
-
-fun xml_of_term (Bound i) =
- XML.Elem ("Bound", [("index", string_of_int i)], [])
- | xml_of_term (Free (s, T)) =
- XML.Elem ("Free", [("name", s)], [xml_of_typ T])
- | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
- ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
- [xml_of_typ T])
- | xml_of_term (Const (s, T)) =
- XML.Elem ("Const", [("name", s)], [xml_of_typ T])
- | xml_of_term (t $ u) =
- XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
- | xml_of_term (Abs (s, T, t)) =
- XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
-
-fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
- | term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
- | term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
- | term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
- | term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
- | term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
- | term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
- | term_of_xml _ = parse_err "term"
-
-fun xml_of_opttypes NONE = []
- | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
-
-(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
-(* it can be looked up in the theorem database. Thus, it could be *)
-(* omitted from the xml representation. *)
-
-fun xml_of_proof (PBound i) =
- XML.Elem ("PBound", [("index", string_of_int i)], [])
- | xml_of_proof (Abst (s, optT, prf)) =
- XML.Elem ("Abst", [("vname", s)],
- (case optT of NONE => [] | SOME T => [xml_of_typ T]) @
- [xml_of_proof prf])
- | xml_of_proof (AbsP (s, optt, prf)) =
- XML.Elem ("AbsP", [("vname", s)],
- (case optt of NONE => [] | SOME t => [xml_of_term t]) @
- [xml_of_proof prf])
- | xml_of_proof (prf % optt) =
- XML.Elem ("Appt", [],
- xml_of_proof prf ::
- (case optt of NONE => [] | SOME t => [xml_of_term t]))
- | xml_of_proof (prf %% prf') =
- XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
- | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
- | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
- XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (PAxm (s, t, optTs)) =
- XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (Oracle (s, t, optTs)) =
- XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
-
-fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
-fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
-fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
-fun xml_of_unit () = XML.Elem ("unit", [], [])
-fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
-fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
-fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
-fun wrap s output x = XML.Elem (s, [], [output x])
-fun wrap_empty s = XML.Elem (s, [], [])
-fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
-fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
-fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) =
- XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
-fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) =
- XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
-
-fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
- | bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
- | bool_of_xml _ = parse_err "bool"
-
-fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
- | int_of_xml _ = parse_err "int"
-
-fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
- | unit_of_xml _ = parse_err "unit"
-
-fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
- | list_of_xml _ _ = parse_err "list"
-
-fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) =
- if i = length ls then map input ls else parse_err "tuple"
- | tuple_of_xml _ _ _ = parse_err "tuple"
-
-fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
- | option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
- | option_of_xml _ _ = parse_err "option"
-
-fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
- | pair_of_xml _ _ _ = parse_err "pair"
-
-fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
- | triple_of_xml _ _ _ _ = parse_err "triple"
-
-fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) =
- (input1 x1, input2 x2, input3 x3, input4 x4)
- | quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
-
-fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) =
- (input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
- | quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
-
-fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
- | unwrap _ _ _ = parse_err "unwrap"
-
-fun unwrap_empty x (XML.Elem (_, [], [])) = x
- | unwrap_empty _ _ = parse_err "unwrap_unit"
-
-fun name_of_wrap (XML.Elem (name, _, _)) = name
- | name_of_wrap _ = parse_err "name_of_wrap"
-
-fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
- | string_of_xml _ = parse_err "string"
-
-fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
- | xml_of_mixfix Structure = wrap_empty "structure"
- | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
- | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
- | xml_of_mixfix (Infix args) = wrap "infix" (xml_of_pair xml_of_string xml_of_int) args
- | xml_of_mixfix (Infixl args) = wrap "infixl" (xml_of_pair xml_of_string xml_of_int) args
- | xml_of_mixfix (Infixr args) = wrap "infixr" (xml_of_pair xml_of_string xml_of_int) args
- | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
-
-fun mixfix_of_xml e =
- (case name_of_wrap e of
- "nosyn" => unwrap_empty NoSyn
- | "structure" => unwrap_empty Structure
- | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
- | "delimfix" => unwrap Delimfix string_of_xml
- | "infix" => unwrap Infix (pair_of_xml string_of_xml int_of_xml)
- | "infixl" => unwrap Infixl (pair_of_xml string_of_xml int_of_xml)
- | "infixr" => unwrap Infixr (pair_of_xml string_of_xml int_of_xml)
- | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
- | _ => parse_err "mixfix"
- ) e
-
-
-fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
-
-fun from_file f input fname =
- let
- val _ = writeln "read_from_file enter"
- val s = File.read (Path.explode fname)
- val _ = writeln "done: read file"
- val tree = timeit (fn () => f s)
- val _ = writeln "done: tree"
- val x = timeit (fn () => input tree)
- val _ = writeln "done: input"
- in
- x
- end
-
-fun write_to_file x = to_file XML.string_of_tree x
-fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
-
-fun serialize_to_file x = to_file XML.encoded_string_of_tree x
-fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
-
-end;
-
-structure XMLConvOutput =
-struct
-open XMLConv
-
-val typ = xml_of_typ
-val term = xml_of_term
-val mixfix = xml_of_mixfix
-val proof = xml_of_proof
-val bool = xml_of_bool
-val int = xml_of_int
-val string = xml_of_string
-val unit = xml_of_unit
-val list = xml_of_list
-val pair = xml_of_pair
-val option = xml_of_option
-val triple = xml_of_triple
-val quadruple = xml_of_quadruple
-val quintuple = xml_of_quintuple
-
-end
-
-structure XMLConvInput =
-struct
-open XMLConv
-
-val typ = typ_of_xml
-val term = term_of_xml
-val mixfix = mixfix_of_xml
-val bool = bool_of_xml
-val int = int_of_xml
-val string = string_of_xml
-val unit = unit_of_xml
-val list = list_of_xml
-val pair = pair_of_xml
-val option = option_of_xml
-val triple = triple_of_xml
-val quadruple = quadruple_of_xml
-val quintuple = quintuple_of_xml
-
-end
-
--- a/src/HOL/IsaMakefile Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 20 10:11:08 2011 +0200
@@ -555,13 +555,11 @@
## HOL-Import
IMPORTER_FILES = \
- Import/ImportRecorder.thy Import/HOL4Compat.thy \
+ Import/HOL4Compat.thy \
Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \
Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \
- Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \
- Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \
- Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \
- Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \
+ Import/import.ML Import/import_syntax.ML \
+ Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \
Library/ContNotDenum.thy Old_Number_Theory/Primes.thy
HOL-Import: HOL $(LOG)/HOL-Import.gz