# HG changeset patch # User obua # Date 1127429533 -7200 # Node ID ece268908438b29288dbe0858f7299afdba0e5f8 # Parent 33d4093182666592d34895986adbb8a3bc5d3397 add debug messages diff -r 33d409318266 -r ece268908438 src/HOL/Import/proof_kernel.ML --- 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 diff -r 33d409318266 -r ece268908438 src/HOL/Import/replay.ML --- 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)