--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Wed Feb 15 23:57:06 2006 +0100
@@ -5,6 +5,10 @@
theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
+;skip_import_dir "/home/obua/tmp/cache"
+
+;skip_import on
+
;import_segment "hollight";
setup_dump "../HOLLight" "HOLLight";
@@ -24,9 +28,9 @@
DEF_IND_SUC
DEF_IND_0
DEF_NUM_REP
- (* TYDEF_sum
+ TYDEF_sum
DEF_INL
- DEF_INR*);
+ DEF_INR;
type_maps
ind > Nat.ind
@@ -34,8 +38,8 @@
fun > fun
N_1 > Product_Type.unit
prod > "*"
- num > nat;
- (* sum > "+";*)
+ num > nat
+ sum > "+";
const_renames
"==" > "eqeq"
@@ -74,10 +78,10 @@
"*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
"-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
BIT0 > HOLLightCompat.NUMERAL_BIT0
- BIT1 > HOL4Compat.NUMERAL_BIT1;
- (* INL > Sum_Type.Inl
- INR > Sum_Type.Inr
- HAS_SIZE > HOLLightCompat.HAS_SIZE*)
+ BIT1 > HOL4Compat.NUMERAL_BIT1
+ INL > Sum_Type.Inl
+ INR > Sum_Type.Inr;
+ (* HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
(*import_until "TYDEF_sum"
--- a/src/HOL/Import/HOL4Compat.thy Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Wed Feb 15 23:57:06 2006 +0100
@@ -3,7 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Compat imports HOL4Setup Divides Primes Real begin
+theory HOL4Compat imports HOL4Setup Divides Primes Real
+begin
lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
by auto
--- a/src/HOL/Import/HOL4Setup.thy Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/HOL4Setup.thy Wed Feb 15 23:57:06 2006 +0100
@@ -3,9 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Setup imports MakeEqual
- uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
- ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
+theory HOL4Setup imports MakeEqual ImportRecorder
+ uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
section {* General Setup *}
--- a/src/HOL/Import/HOLLightCompat.thy Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy Wed Feb 15 23:57:06 2006 +0100
@@ -91,6 +91,16 @@
lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
by (simp add: NUMERAL_BIT1_def)
+consts
+ sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
+primrec
+ "sumlift f g (Inl a) = f a"
+ "sumlift f g (Inr b) = g b"
+
+lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
+ apply (rule exI[where x="sumlift Inl' Inr'"])
+ apply auto
+ done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/ImportRecorder.thy Wed Feb 15 23:57:06 2006 +0100
@@ -0,0 +1,4 @@
+theory ImportRecorder imports Main
+uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
+begin
+end
\ No newline at end of file
--- a/src/HOL/Import/import_syntax.ML Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/import_syntax.ML Wed Feb 15 23:57:06 2006 +0100
@@ -6,6 +6,7 @@
signature HOL4_IMPORT_SYNTAX =
sig
type token = OuterSyntax.token
+ type command = token list -> (theory -> theory) * token list
val import_segment: token list -> (theory -> theory) * token list
val import_theory : token list -> (theory -> theory) * token list
@@ -22,6 +23,9 @@
val const_moves : token list -> (theory -> theory) * token list
val const_renames : token list -> (theory -> theory) * token list
+ val skip_import_dir : token list -> (theory -> theory) * token list
+ val skip_import : token list -> (theory -> theory) * token list
+
val setup : unit -> unit
end
@@ -29,6 +33,7 @@
struct
type token = OuterSyntax.token
+type command = token list -> (theory -> theory) * token list
local structure P = OuterParse and K = OuterKeyword in
@@ -36,12 +41,20 @@
val import_segment = P.name >> set_import_segment
+
val import_theory = P.name >> (fn thyname =>
fn thy =>
thy |> set_generating_thy thyname
|> Theory.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
+fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
+val skip_import_dir : command = P.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)
+val skip_import : command = P.short_ident >> do_skip_import
+
fun end_import toks =
Scan.succeed
(fn thy =>
@@ -50,13 +63,21 @@
val segname = get_import_segment thy
val (int_thms,facts) = Replay.setup_int_thms thyname thy
val thmnames = List.filter (not o should_ignore thyname thy) facts
- (* val _ = set show_types
- val _ = set show_sorts*)
+ 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)
+ val _ = ImportRecorder.save_history thyname
+ val _ = ImportRecorder.clear_history ()
+ in
+ thy
+ end
in
thy |> clear_import_thy
|> set_segment thyname segname
|> set_used_names facts
- |> Replay.import_thms thyname int_thms thmnames
+ |> replay
|> clear_used_names
|> export_hol4_pending
|> Theory.parent_path
@@ -211,6 +232,12 @@
OuterSyntax.command "end_import"
"End HOL4 import"
K.thy_decl (end_import >> Toplevel.theory),
+ OuterSyntax.command "skip_import_dir"
+ "Sets caching directory for skipping importing"
+ K.thy_decl (skip_import_dir >> Toplevel.theory),
+ OuterSyntax.command "skip_import"
+ "Switches skipping importing on or off"
+ K.thy_decl (skip_import >> Toplevel.theory),
OuterSyntax.command "setup_theory"
"Setup HOL4 theory replaying"
K.thy_decl (setup_theory >> Toplevel.theory),
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/importrecorder.ML Wed Feb 15 23:57:06 2006 +0100
@@ -0,0 +1,253 @@
+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
+
+ 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 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
+
+datatype history_entry = StartReplay of string*string
+ | StopReplay of string*string
+ | AbortReplay of string*string
+ | Delta of deltastate list
+
+val history = ref ([]:history_entry list)
+val history_dir = ref (SOME "")
+val skip_imports = 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
+
+ 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 _ = 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 set_skip_import_dir dir = (history_dir := dir)
+fun get_skip_import_dir () = !history_dir
+
+fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (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.unpack 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_scan.ML Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/lazy_scan.ML Wed Feb 15 23:57:06 2006 +0100
@@ -19,7 +19,7 @@
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
+ -> ('a,string) scanner
val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
val one : ('a -> bool) -> ('a,'a) scanner
val succeed : 'b -> ('a,'b) scanner
@@ -30,11 +30,14 @@
val repeat : ('a,'b) scanner -> ('a,'b list) scanner
val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
val ahead : ('a,'b) scanner -> ('a,'b) scanner
- val unless : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
+ val unless : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
val $$ : ''a -> (''a,''a) scanner
val !! : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
+ val scan_id : (string, string) scanner
+ val this : ''a list -> (''a, ''a list) scanner
+ val this_string : string -> (string, string) scanner
end
structure LazyScan :> LAZY_SCAN =
@@ -203,4 +206,11 @@
LazySeq.make (fn () => F toks)
end
+val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
+
+fun this [] = (fn toks => ([], toks))
+ | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
+
+fun this_string s = this (explode s) >> K s
+
end
--- a/src/HOL/Import/lazy_seq.ML Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/lazy_seq.ML Wed Feb 15 23:57:06 2006 +0100
@@ -21,6 +21,7 @@
val getItem : 'a seq -> ('a * 'a seq) option
val nth : 'a seq * int -> 'a
val take : 'a seq * int -> 'a seq
+ val take_at_most : 'a seq * int -> 'a list
val drop : 'a seq * int -> 'a seq
val rev : 'a seq -> 'a seq
val concat : 'a seq seq -> 'a seq
@@ -90,7 +91,7 @@
fun getItem (Seq s) = force s
fun make f = Seq (delay f)
-fun null s = isSome (getItem s)
+fun null s = is_none (getItem s)
local
fun F n NONE = n
@@ -148,6 +149,12 @@
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
--- a/src/HOL/Import/proof_kernel.ML Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML Wed Feb 15 23:57:06 2006 +0100
@@ -73,6 +73,7 @@
val to_isa_thm : thm -> (term * term) list * Thm.thm
val to_isa_term: term -> Term.term
+ val to_hol_thm : Thm.thm -> thm
val REFL : term -> theory -> theory * thm
val ASSUME : term -> theory -> theory * thm
@@ -124,6 +125,7 @@
fun hthm2thm (HOLThm (_, th)) = th
+fun to_hol_thm th = HOLThm ([], th)
datatype proof_info
= Info of {disk_info: (string * string) option ref}
@@ -199,6 +201,8 @@
ct)
end
+exception SMART_STRING
+
fun smart_string_of_cterm ct =
let
val {sign,t,T,...} = rep_cterm ct
@@ -207,8 +211,10 @@
handle TERM _ => ct)
fun match cu = t aconv (term_of cu)
fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
- | G 1 = Library.setmp show_all_types true (G 0)
- | G _ = error ("ProofKernel.smart_string_of_cterm internal error")
+ | G 1 = Library.setmp show_brackets true (G 0)
+ | G 2 = Library.setmp show_all_types true (G 0)
+ | G 3 = Library.setmp show_brackets true (G 2)
+ | G _ = raise SMART_STRING
fun F n =
let
val str = Library.setmp show_brackets false (G n string_of_cterm) ct
@@ -219,6 +225,7 @@
else F (n+1)
end
handle ERROR mesg => F (n+1)
+ | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
in
Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
@@ -1041,14 +1048,7 @@
res
end
-(* rotate left k places, leaving the first j and last l premises alone
-*)
-
-fun permute_prems j k 0 th = Thm.permute_prems j k th
- | permute_prems j k l th =
- th |> Thm.permute_prems 0 (~l)
- |> Thm.permute_prems (j+l) k
- |> Thm.permute_prems 0 l
+val permute_prems = Thm.permute_prems
fun rearrange sg tm th =
let
@@ -1140,7 +1140,7 @@
val new_name = new_name' "a"
fun replace_name n' (Free (n, t)) = Free (n', t)
| replace_name n' _ = ERR "replace_name"
- (* map: old oder fresh name -> old free,
+ (* map: old or fresh name -> old free,
invmap: old free which has fresh name assigned to it -> fresh name *)
fun dis (v, mapping as (map,invmap)) =
let val n = name_of v in
@@ -1176,7 +1176,7 @@
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
-val conjE_helper = Thm.permute_prems 0 1 conjE
+val conjE_helper = permute_prems 0 1 conjE
fun get_hol4_thm thyname thmname thy =
case get_hol4_theorem thyname thmname thy of
@@ -1286,6 +1286,8 @@
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
@@ -1351,6 +1353,7 @@
val rew = rewrite_hol4_term (concl_of th) thy
val th = 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 thy2 = if gen_output
then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
@@ -1903,34 +1906,45 @@
val csyn = mk_syn thy constname
val thy1 = case HOL4DefThy.get thy of
Replaying _ => thy
- | _ => Theory.add_consts_i [(constname,ctype,csyn)] thy
+ | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Theory.add_consts_i [(constname,ctype,csyn)] thy)
val eq = mk_defeq constname rhs' thy1
val (thms, thy2) = PureThy.add_defs_i false [((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)))
val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
then
- add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
+ let
+ val p1 = quotename constname
+ val p2 = string_of_ctyp (ctyp_of thy'' ctype)
+ val p3 = Syntax.string_of_mixfix csyn
+ val p4 = smart_string_of_cterm crhs
+ in
+ add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
+ end
else
- add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
- "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
- thy''
-
+ (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
+ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
+ thy'')
val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
- SOME (_,res) => HOLThm(rens_of linfo,res)
- | NONE => raise ERR "new_definition" "Bad conclusion"
+ SOME (_,res) => HOLThm(rens_of linfo,res)
+ | NONE => raise ERR "new_definition" "Bad conclusion"
val fullname = Sign.full_name thy22 thmname
val thy22' = case opt_get_output_thy thy22 of
- "" => add_hol4_mapping thyname thmname fullname thy22
+ "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
+ 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
@@ -1981,6 +1995,7 @@
val str = Library.foldl (fn (acc,(c,T,csyn)) =>
acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
val thy' = add_dump str thy
+ val _ = ImportRecorder.add_consts consts
in
Theory.add_consts_i consts thy'
end
@@ -1988,9 +2003,11 @@
val thy1 = foldr (fn(name,thy)=>
snd (get_defname thyname name thy)) thy1 names
fun new_name name = fst (get_defname thyname name thy1)
+ val names' = map (fn name => (new_name name,name,false)) names
val (thy',res) = SpecificationPackage.add_specification NONE
- (map (fn name => (new_name name,name,false)) names)
+ names'
(thy1,th)
+ val _ = ImportRecorder.add_specification names' th
val res' = Drule.freeze_all res
val hth = HOLThm(rens,res')
val rew = rewrite_hol4_term (concl_of res') thy'
@@ -2056,17 +2073,20 @@
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
+ val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
+ val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
val th3 = (#type_definition 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 = equal_elim rew (Thm.transfer thy4 td_th)
@@ -2146,7 +2166,8 @@
val tnames = sort string_ord (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val (thy',typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
+ val (thy', typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_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
@@ -2161,9 +2182,11 @@
val _ = if Drule.vars_of th4 = [] then () else 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 Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/replay.ML Wed Feb 15 23:57:06 2006 +0100
@@ -9,6 +9,7 @@
structure P = ProofKernel
open ProofKernel
+open ImportRecorder
exception REPLAY of string * string
fun ERR f mesg = REPLAY (f,mesg)
@@ -16,6 +17,7 @@
fun replay_proof int_thms thyname thmname prf thy =
let
+ val _ = ImportRecorder.start_replay_proof thyname thmname
fun rp (PRefl tm) thy = P.REFL tm thy
| rp (PInstT(p,lambda)) thy =
let
@@ -270,8 +272,13 @@
| _ => rp pc thy
end
in
- rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
- end
+ let
+ val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
+ val _ = ImportRecorder.stop_replay_proof thyname thmname
+ in
+ x
+ end
+ end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
fun setup_int_thms thyname thy =
let
@@ -312,9 +319,77 @@
replay_fact (thmname,thy)
end
+fun replay_chached_thm int_thms thyname thmname =
+ let
+ fun th_of thy = setmp quick_and_dirty true (SkipProof.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
+(* 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
+*)
+ and delta (Specification (names, th)) thy =
+ fst (SpecificationPackage.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 = Theory.add_consts_i 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 (PureThy.add_defs_i false [((thmname, eq), [])] thy)
+ | delta (Hol_theorem (thyname, thmname, th)) thy =
+ add_hol4_theorem thyname thmname ([], th_of thy th) thy
+ | delta (Typedef (thmname, typ, c, repabs, th)) thy =
+ fst(TypedefPackage.add_typedef_i false thmname typ c 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 (P.to_hol_thm (th_of thy th))); thy)
+ in
+ rps
+ end
+
fun import_thms thyname int_thms thmnames thy =
let
- fun replay_fact (thy,thmname) =
+ 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
+ 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
val _ = set_disk_info_of prf thyname thmname
@@ -323,7 +398,10 @@
in
p
end
- val res_thy = Library.foldl replay_fact (thy,thmnames)
+ 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)
in
res_thy
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/xml.ML Wed Feb 15 23:57:06 2006 +0100
@@ -0,0 +1,159 @@
+(* Title: Pure/General/xml.ML
+ ID: $Id$
+ Author: David Aspinall, Stefan Berghofer and Markus Wenzel
+
+Basic support for XML.
+*)
+
+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
+end;
+
+structure XML =
+struct
+
+structure Scan = LazyScan
+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 = "&#" ^ Int.toString (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 (LazySeq.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.not_eof)) >> implode;
+
+val parse_cdata = Scan.this_string "<![CDATA[" |--
+ (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
+ 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.not_eof)) >> implode) --| $$ s) >> snd);
+
+val parse_comment = Scan.this_string "<!--" --
+ Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
+ 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.not_eof)) --|
+ 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 @) >> List.concat) >> 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.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
+ parse_elem;
+
+fun tree_of_string s =
+ let
+ val seq = LazySeq.of_list (Symbol.explode s)
+ val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
+ val (x, toks) = scanner seq
+ in
+ if LazySeq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/xmlconv.ML Wed Feb 15 23:57:06 2006 +0100
@@ -0,0 +1,300 @@
+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
+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 (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
+ | xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
+ | xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
+ | xml_of_mixfix (Infix i) = wrap "infix" xml_of_int i
+ | xml_of_mixfix (Infixl i) = wrap "infixl" xml_of_int i
+ | xml_of_mixfix (Infixr i) = wrap "infixr" xml_of_int i
+ | 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
+ | "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml)
+ | "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)
+ | "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
+ | "infix" => unwrap Infix int_of_xml
+ | "infixl" => unwrap Infixl int_of_xml
+ | "infixr" => unwrap Infixr int_of_xml
+ | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
+ | _ => parse_err "mixfix"
+ ) e
+
+
+fun write_to_file output fname x = File.write (Path.unpack fname) (XML.string_of_tree (output x))
+
+fun read_from_file input fname =
+ let
+ val _ = writeln "read_from_file enter"
+ val s = File.read (Path.unpack fname)
+ val _ = writeln "done: read file"
+ val tree = timeit (fn () => XML.tree_of_string s)
+ val _ = writeln "done: tree"
+ val x = timeit (fn () => input tree)
+ val _ = writeln "done: input"
+ in
+ x
+ end
+
+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
+