# HG changeset patch # User skalberg # Date 1082238815 -7200 # Node ID 1be590fd242247bb7b1ffa64692619f512f98050 # Parent 8876ad83b1fbc103de35c69f8075ae36c7175ba9 Minor cleanup of headers and some speedup of the HOL4 import. diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/GenHOL4Base.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory GenHOL4Base = HOL4Compat + HOL4Syntax:; import_segment "hol4"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/GenHOL4Prob.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/GenHOL4Prob.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory GenHOL4Prob = GenHOL4Real: import_segment "hol4"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory GenHOL4Real = GenHOL4Base: import_segment "hol4"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/GenHOL4Vec.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/GenHOL4Vec.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory GenHOL4Vec = GenHOL4Base: import_segment "hol4"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/GenHOL4Word32.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/GenHOL4Word32.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory GenHOL4Word32 = GenHOL4Base:; import_segment "hol4"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/Generate-HOL/ROOT.ML --- a/src/HOL/Import/Generate-HOL/ROOT.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/ROOT.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; use_thy "GenHOL4Prob"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/README --- a/src/HOL/Import/HOL/README Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL/README Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,20 @@ +(* Title: HOL/Import/HOL/README + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + All the files in this directory (except this README, HOL4.thy, and ROOT.ML) are automatically generated. Edit the files in -../Generate-HOL, if something needs to be changed. +../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in +~~/src/HOL, if something needs to be changed. + +To build the logic in this directory, simply do a "isatool make +HOL-Import-HOL" in ~~/src/HOL. + +Note that the quick_and_dirty flag is on as default for this +directory, which means that the original HOL4 proofs are not consulted +at all. If a real replay of the HOL4 proofs is desired, get and +unpack the HOL4 proof objects to somewhere on your harddisk, and set +the variable PROOF_DIRS to the directory where the directory "hol4" +is. Now edit the ROOT.ML file to unset the quick_and_dirty flag and +do "isatool make HOL-Import-HOL" in ~~/src/HOL. diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/ROOT.ML --- a/src/HOL/Import/HOL/ROOT.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL/ROOT.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/HOL/ROOT.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; setmp quick_and_dirty true use_thy "HOL4Prob"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL/real.imp Sat Apr 17 23:53:35 2004 +0200 @@ -77,13 +77,13 @@ "REAL_SUB_RZERO" > "Ring_and_Field.diff_0_right" "REAL_SUB_RNEG" > "Ring_and_Field.diff_minus_eq_add" "REAL_SUB_REFL" > "Ring_and_Field.diff_self" - "REAL_SUB_RDISTRIB" > "Ring_and_Field.left_diff_distrib" + "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6" "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" "REAL_SUB_LZERO" > "Ring_and_Field.diff_0" "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff" "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff" - "REAL_SUB_LDISTRIB" > "Ring_and_Field.right_diff_distrib" + "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7" "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" "REAL_SUB_ADD2" > "Ring_and_Field.add_minus_self_left" "REAL_SUB_ADD" > "Ring_and_Field.minus_add_self" @@ -91,7 +91,7 @@ "REAL_SUB_0" > "Ring_and_Field.eq_iff_diff_eq_0" "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff" "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique" - "REAL_RDISTRIB" > "Ring_and_Field.ring_distrib_2" + "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" "REAL_POW_POW" > "Power.power_mult" "REAL_POW_MONO_LT" > "Power.power_strict_increasing" "REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2" @@ -129,7 +129,7 @@ "REAL_NEG_ADD" > "Ring_and_Field.minus_add_distrib" "REAL_NEG_0" > "Ring_and_Field.minus_zero" "REAL_NEGNEG" > "Ring_and_Field.minus_minus" - "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2" + "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right" "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right" "REAL_MUL_RINV" > "Ring_and_Field.right_inverse" @@ -243,7 +243,7 @@ "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD" "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" "REAL_LE" > "RealDef.real_of_nat_le_iff" - "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1" + "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" "REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive" "REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero" "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL" @@ -257,8 +257,8 @@ "REAL_INJ" > "RealDef.real_of_nat_inject" "REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves" "REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ" - "REAL_EQ_SUB_RADD" > "Ring_and_Field.compare_rls_10" - "REAL_EQ_SUB_LADD" > "Ring_and_Field.compare_rls_11" + "REAL_EQ_SUB_RADD" > "Ring_and_Field.ring_eq_simps_15" + "REAL_EQ_SUB_LADD" > "Ring_and_Field.ring_eq_simps_16" "REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma" "REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right" "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ" @@ -283,17 +283,17 @@ "REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ" "REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST" "REAL_ARCH" > "RComplete.reals_Archimedean3" - "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2" + "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2" "REAL_ADD_SUB" > "Ring_and_Field.add_minus_self_right" "REAL_ADD_RINV" > "Ring_and_Field.right_minus" "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" "REAL_ADD_RID" > "Ring_and_Field.add_0_right" - "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_distrib_2" + "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0" - "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_distrib_1" + "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2" "REAL_ADD" > "RealDef.real_of_nat_add" diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL/realax.imp Sat Apr 17 23:53:35 2004 +0200 @@ -91,7 +91,7 @@ "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" "TREAL_10" > "HOL4Real.realax.TREAL_10" "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" - "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2" + "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1" "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" @@ -100,9 +100,9 @@ "REAL_LT_REFL" > "HOL.order_less_irrefl" "REAL_LT_MUL" > "Ring_and_Field.mult_pos" "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono" - "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1" + "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" - "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2" + "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0" "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL4Compat.thy --- a/src/HOL/Import/HOL4Compat.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL4Compat.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/HOL4Compat.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory HOL4Compat = HOL4Setup + Divides + Primes + Real: lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))" diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL4Setup.thy --- a/src/HOL/Import/HOL4Setup.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL4Setup.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/HOL4Setup.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory HOL4Setup = MakeEqual files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"): diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL4Syntax.thy --- a/src/HOL/Import/HOL4Syntax.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL4Syntax.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/HOL4Syntax.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory HOL4Syntax = HOL4Setup files "import_syntax.ML": diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/MakeEqual.thy --- a/src/HOL/Import/MakeEqual.thy Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/MakeEqual.thy Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/MakeEqual.thy + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + theory MakeEqual = Main files "shuffler.ML": diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/ROOT.ML --- a/src/HOL/Import/ROOT.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/ROOT.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,2 +1,7 @@ +(* Title: HOL/Import/ROOT.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + use_thy "HOL4Compat"; use_thy "HOL4Syntax"; diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/hol4rews.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/hol4rews.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord); type holthm = (term * term) list * thm @@ -24,7 +29,7 @@ structure ImportSegmentArgs: THEORY_DATA_ARGS = struct -val name = "HOL4/import" +val name = "HOL4/import_segment" type T = string val empty = "" val copy = I diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/import_package.ML --- a/src/HOL/Import/import_package.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/import_package.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/import_package.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + signature IMPORT_PACKAGE = sig val import_meth: Args.src -> Proof.context -> Proof.method @@ -5,6 +10,20 @@ val debug : bool ref end +structure ImportDataArgs: THEORY_DATA_ARGS = +struct +val name = "HOL4/import_data" +type T = ProofKernel.thm option array option +val empty = None +val copy = I +val prep_ext = I +fun merge _ = None +fun print sg import_segment = + Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented")) +end + +structure ImportData = TheoryDataFun(ImportDataArgs) + structure ImportPackage :> IMPORT_PACKAGE = struct @@ -24,7 +43,9 @@ val sg = sign_of_thm th val prem = hd (prems_of th) val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem))) - val int_thms = fst (Replay.setup_int_thms thyname thy) + val int_thms = case ImportData.get thy of + None => fst (Replay.setup_int_thms thyname thy) + | Some a => a val proof = snd (ProofKernel.import_proof thyname thmname thy) thy val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) val thm = snd (ProofKernel.to_isa_thm hol4thm) @@ -57,5 +78,5 @@ Method.SIMPLE_METHOD (import_tac arg thy) end) -val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem")] +val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init] end diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/import_syntax.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/import_syntax.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + signature HOL4_IMPORT_SYNTAX = sig type token = OuterSyntax.token @@ -150,14 +155,26 @@ apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list))) end +fun create_int_thms thyname thy = + case ImportData.get thy of + None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy + | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?" + +fun clear_int_thms thy = + case ImportData.get thy of + None => error "Import data already cleared - forgotten a setup_theory?" + | Some _ => ImportData.put None thy + val setup_theory = P.name >> (fn thyname => fn thy => - case HOL4DefThy.get thy of - NoImport => thy |> import_thy thyname - | Generating _ => error "Currently generating a theory!" - | Replaying _ => thy |> clear_import_thy |> import_thy thyname) + (case HOL4DefThy.get thy of + NoImport => thy + | Generating _ => error "Currently generating a theory!" + | Replaying _ => thy |> clear_import_thy) + |> import_thy thyname + |> create_int_thms thyname) fun end_setup toks = Scan.succeed @@ -168,6 +185,7 @@ in thy |> set_segment thyname segname |> clear_import_thy + |> clear_int_thms |> Theory.parent_path end) toks diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/proof_kernel.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + signature ProofKernel = sig type hol_type @@ -47,7 +52,7 @@ exception PK of string * string - val get_proof_dir: string -> theory -> string + val get_proof_dir: string -> theory -> string option val debug : bool ref val disk_info_of : proof -> (string * string) option val set_disk_info_of : proof -> string -> string -> unit @@ -165,16 +170,10 @@ (* Compatibility. *) -fun quote s = "\"" ^ s ^ "\"" - -fun alphanum str = case String.explode str of - first::rest => Char.isAlpha first andalso forall (fn c => Char.isAlphaNum c orelse c = #"_") rest - | _ => error "ProofKernel.alphanum: Empty constname??" - -fun mk_syn c = if alphanum c then NoSyn else Syntax.literal c +fun mk_syn c = if Symbol.is_identifier c then NoSyn else Syntax.literal c val keywords = ["open"] -fun quotename c = if alphanum c andalso not (c mem keywords) then c else quote c +fun quotename c = if Symbol.is_identifier c andalso not (c mem keywords) then c else quote c fun smart_string_of_cterm ct = let @@ -321,6 +320,7 @@ || scan_string "quot;" #"\"" || scan_string "gt;" #">" || scan_string "lt;" #"<" + || scan_string "apos;" #"'" in fun scan_nonquote toks = case LazySeq.getItem toks of @@ -566,29 +566,29 @@ case get_segment2 thyname thy of Some seg => seg | None => get_import_segment thy - val defpath = [(getenv "ISABELLE_HOME_USER") ^ "/proofs"] - val path = - case getenv "PROOF_DIRS" of - "" => defpath - | path => (space_explode ":" path) @ defpath - fun find [] = error ("Unable to find import segment " ^ import_segment) - | find (p::ps) = (let - val dir = p ^ "/" ^ import_segment - in - if OS.FileSys.isDir dir - then dir - else find ps - end) handle OS.SysErr _ => find ps + val defpath = [OS.Path.joinDirFile {dir=getenv "ISABELLE_HOME_USER",file="proofs"}] + val path = space_explode ":" (getenv "PROOF_DIRS") @ defpath + fun find [] = None + | find (p::ps) = + (let + val dir = OS.Path.joinDirFile {dir = p,file=import_segment} + in + if OS.FileSys.isDir dir + then Some dir + else find ps + end) handle OS.SysErr _ => find ps in - find path ^ "/" ^ thyname + apsome (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) end fun proof_file_name thyname thmname thy = let - val path = get_proof_dir thyname thy + val path = case get_proof_dir thyname thy of + Some p => p + | None => error "Cannot find proof files" val _ = OS.FileSys.mkDir path handle OS.SysErr _ => () in - String.concat[path,"/",thmname,".prf"] + OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}} end fun xml_to_proof thyname types terms prf thy = diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/replay.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/replay.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + structure Replay = struct @@ -268,7 +273,11 @@ fun setup_int_thms thyname thy = let - val is = TextIO.openIn(P.get_proof_dir thyname thy ^"/facts.lst") + val fname = + case P.get_proof_dir thyname thy of + Some p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}} + | None => error "Cannot find proof files" + val is = TextIO.openIn fname val (num_int_thms,facts) = let fun get_facts facts = diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/shuffler.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,7 +1,6 @@ -(* Title: Provers/shuffler.ML +(* Title: HOL/Import/shuffler.ML ID: $Id$ Author: Sebastian Skalberg, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) Package for proving two terms equal by normalizing (hence the "shuffler" name). Uses the simplifier for the normalization. diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Tools/specification_package.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,7 +1,6 @@ (* Title: HOL/Tools/specification_package.ML ID: $Id$ Author: Sebastian Skalberg, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) Package for defining constants by specification. *)