# HG changeset patch # User obua # Date 1140044226 -3600 # Node ID bf19cc5a789991ff599ac8ba82f586bb2ce21f4e # Parent 049c010c8fb7cfd87d28fdccb0cdfafa5e119f56 fixed bugs, added caching diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- 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 \ nat \ nat" "-" > "op -" :: "nat \ nat \ 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" diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/HOL4Compat.thy --- 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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/HOL4Setup.thy --- 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 *} diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/HOLLightCompat.thy --- 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 \ 'c) \ ('b \ 'c) \ (('a + 'b) \ 'c)" +primrec + "sumlift f g (Inl a) = f a" + "sumlift f g (Inr b) = g b" + +lemma sum_Recursion: "\ f. (\ a. f (Inl a) = Inl' a) \ (\ b. f (Inr b) = Inr' b)" + apply (rule exI[where x="sumlift Inl' Inr'"]) + apply auto + done end diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/ImportRecorder.thy --- /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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/import_syntax.ML --- 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), diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/importrecorder.ML --- /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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/lazy_scan.ML --- 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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/lazy_seq.ML --- 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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/proof_kernel.ML --- 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 = diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/replay.ML --- 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 diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/xml.ML --- /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 = "\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 "\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 "") (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.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.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 ")) + (Scan.this_string (""))) >> + (fn ((s, atts), ts) => Elem (s, atts, ts))) xs; + +val parse_document = + Scan.option (Scan.this_string "") + (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; diff -r 049c010c8fb7 -r bf19cc5a7899 src/HOL/Import/xmlconv.ML --- /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 +