--- a/src/HOL/Import/proof_kernel.ML Fri Sep 23 00:11:10 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 23 00:52:13 2005 +0200
@@ -448,9 +448,11 @@
fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
+fun handle_error f d = transform_error f () handle ERROR_MESSAGE _ => d
+
val check_name_thy = theory "Main"
-fun valid_boundvarname s = (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true) handle _ => false
-fun valid_varname s = (read_cterm check_name_thy (s, TypeInfer.logicT); true) handle _ => false
+fun valid_boundvarname s = handle_error (fn () => (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true)) false
+fun valid_varname s = handle_error (fn () => (read_cterm check_name_thy (s, TypeInfer.logicT); true)) false
fun protect_varname s =
if innocent_varname s andalso valid_varname s then s else
@@ -1007,6 +1009,7 @@
fun mk_GEN v th sg =
let
+ val _ = writeln "enter mk_GEN"
val c = HOLogic.dest_Trueprop (concl_of th)
val cv = cterm_of sg v
val lc = Term.lambda v c
@@ -1024,6 +1027,7 @@
| _ => raise ERR "mk_GEN" "Unknown conclusion"
val th4 = Thm.rename_boundvars cold cnew th3
val res = implies_intr_hyps th4
+ val _ = writeln "exit mk_GEN"
in
res
end
@@ -1194,6 +1198,7 @@
case get_hol4_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
+ val _ = writeln "isabelle_thm: SOME SOME"
val _ = message ("Looking for " ^ thmname)
val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
handle ERROR_MESSAGE _ =>
@@ -1212,13 +1217,14 @@
| SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
| NONE =>
let
+ val _ = writeln "isabelle_thm: None"
val _ = (message "Looking for conclusion:";
if_debug prin isaconc)
val cs = non_trivial_term_consts isaconc
val _ = (message "Looking for consts:";
message (commas cs))
val pot_thms = Shuffler.find_potential thy isaconc
- val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
+ val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
in
case Shuffler.set_prop thy isaconc pot_thms of
SOME (isaname,th) =>
@@ -1236,6 +1242,7 @@
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
let
+ val _ = writeln "enter get_isabelle_thm_and_warn"
val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
fun warn () =
let
@@ -1254,13 +1261,13 @@
end
in
case b of
- NONE => (warn () handle _ => (); (a,b))
- | _ => (a, b)
+ NONE => (warn () handle _ => (); writeln "exit get_isabelle_thm_and_warn"; (a,b))
+ | _ => (writeln "exit get_isabelle_thm_and_warn"; (a, b))
end
fun get_thm thyname thmname thy =
case get_hol4_thm thyname thmname thy of
- SOME hth => (thy,SOME hth)
+ SOME hth => (writeln "got hol4 thm"; (thy,SOME hth))
| NONE => ((case import_proof_concl thyname thmname thy of
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
| NONE => (message "No conclusion"; (thy,NONE)))
@@ -1640,7 +1647,7 @@
fun GEN v hth thy =
let
- val _ = message "GEN:"
+ val _ = writeln "GEN:"
val _ = if_debug prin v
val _ = if_debug pth hth
val (info,th) = disamb_thm hth
@@ -1648,6 +1655,7 @@
val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy))
val _ = message "RESULT:"
val _ = if_debug pth res
+ val _ = writeln "exit GEN"
in
(thy,res)
end
@@ -2074,9 +2082,16 @@
add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
end
+(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
+fun choose_upon_replay_history thy s dth =
+ case Symtab.lookup (!type_intro_replay_history) s of
+ NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
+ | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
+*)
+
fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
case HOL4DefThy.get thy of
- Replaying _ => (thy, HOLThm([], thm (thmname^"_@intern")) handle _ => hth)
+ Replaying _ => (thy, handle_error (fn () => HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern")))) hth)
| _ =>
let
val _ = message "TYPE_INTRO:"
@@ -2142,8 +2157,10 @@
val isa_abs_name_def = isa_abs_name^"_symdest"
val thy = add_dump_constdefs thy (SOME isa_rep_name_def) rep_name isa_rep_name rep_ty
val thy = add_dump_constdefs thy (SOME isa_abs_name_def) abs_name isa_abs_name abs_ty
- val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [OF "^(quotename ("type_definition_" ^ tycname)) ^
- " ,\n simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
+ val str_aty = string_of_ctyp (ctyp_of thy aty)
+ val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [where a=\"a :: "^str_aty^"\" and r=r" ^
+ " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^
+ " ,\n simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
val _ = message "RESULT:"
val _ = if_debug pth hth'
in
--- a/src/HOL/Import/replay.ML Fri Sep 23 00:11:10 2005 +0200
+++ b/src/HOL/Import/replay.ML Fri Sep 23 00:52:13 2005 +0200
@@ -77,9 +77,13 @@
end
| rp (PGen(prf,v)) thy =
let
+ val _ = writeln "enter rp PGen"
val (thy',th) = rp' prf thy
+ val _ = writeln "replayed inner proof"
+ val p = P.GEN v th thy'
+ val _ = writeln "exit rp PGen"
in
- P.GEN v th thy'
+ p
end
| rp (PGenAbs(prf,opt,vl)) thy =
let
@@ -225,7 +229,7 @@
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
| NONE =>
(case P.get_thm thyname' thmname thy of
- (thy',SOME res) => (thy',res)
+ (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
| (thy',NONE) =>
if thyname' = thyname
then
@@ -300,11 +304,15 @@
let
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("Replaying " ^ thmname)
+ val _ = writeln ("import_single_thm: Replaying " ^ thmname)
val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
in
- fst (replay_proof int_thms thyname thmname prf thy)
+ p
end
in
replay_fact (thmname,thy)
@@ -314,11 +322,15 @@
let
fun replay_fact (thy,thmname) =
let
- val _ = writeln ("Replaying " ^ thmname)
- val prf = mk_proof PDisk
- val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("import_thms: Replaying " ^ thmname)
+ val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
in
- fst (replay_proof int_thms thyname thmname prf thy)
+ p
end
val res_thy = Library.foldl replay_fact (thy,thmnames)
in
@@ -330,11 +342,15 @@
val int_thms = fst (setup_int_thms thyname thy)
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("Replaying " ^ thmname)
- val prf = mk_proof PDisk
- val _ = set_disk_info_of prf thyname thmname
- in
- fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("import_thm: Replaying " ^ thmname)
+ val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
+ in
+ p
end
in
replay_fact (thmname,thy)