add debug messages
authorobua
Fri Sep 23 00:52:13 2005 +0200 (2005-09-23)
changeset 17592ece268908438
parent 17591 33d409318266
child 17593 01870f76478c
add debug messages
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 23 00:11:10 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 23 00:52:13 2005 +0200
     1.3 @@ -448,9 +448,11 @@
     1.4  
     1.5  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
     1.6  
     1.7 +fun handle_error f d = transform_error f () handle ERROR_MESSAGE _ => d
     1.8 +
     1.9  val check_name_thy = theory "Main"
    1.10 -fun valid_boundvarname s = (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true) handle _ => false 
    1.11 -fun valid_varname s = (read_cterm check_name_thy (s, TypeInfer.logicT); true) handle _ => false 
    1.12 +fun valid_boundvarname s = handle_error (fn () => (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true)) false 
    1.13 +fun valid_varname s = handle_error (fn () => (read_cterm check_name_thy (s, TypeInfer.logicT); true)) false 
    1.14  
    1.15  fun protect_varname s =
    1.16      if innocent_varname s andalso valid_varname s then s else
    1.17 @@ -1007,6 +1009,7 @@
    1.18  
    1.19  fun mk_GEN v th sg =
    1.20      let
    1.21 +	val _ = writeln "enter mk_GEN"
    1.22  	val c = HOLogic.dest_Trueprop (concl_of th)
    1.23  	val cv = cterm_of sg v
    1.24  	val lc = Term.lambda v c
    1.25 @@ -1024,6 +1027,7 @@
    1.26  			    | _ => raise ERR "mk_GEN" "Unknown conclusion"
    1.27  	val th4 = Thm.rename_boundvars cold cnew th3
    1.28  	val res = implies_intr_hyps th4
    1.29 +	val _ = writeln "exit mk_GEN"
    1.30      in
    1.31  	res
    1.32      end
    1.33 @@ -1194,6 +1198,7 @@
    1.34  	case get_hol4_mapping thyname thmname thy of
    1.35  	    SOME (SOME thmname) =>
    1.36  	    let
    1.37 +		val _ = writeln "isabelle_thm: SOME SOME"
    1.38  		val _ = message ("Looking for " ^ thmname)
    1.39  		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
    1.40  			   handle ERROR_MESSAGE _ =>
    1.41 @@ -1212,13 +1217,14 @@
    1.42  	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
    1.43  	  | NONE =>
    1.44  	    let
    1.45 +		val _ = writeln "isabelle_thm: None"
    1.46  		val _ = (message "Looking for conclusion:";
    1.47  			 if_debug prin isaconc)
    1.48  		val cs = non_trivial_term_consts isaconc
    1.49  		val _ = (message "Looking for consts:";
    1.50  			 message (commas cs))
    1.51  		val pot_thms = Shuffler.find_potential thy isaconc
    1.52 -		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
    1.53 +		val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
    1.54  	    in
    1.55  		case Shuffler.set_prop thy isaconc pot_thms of
    1.56  		    SOME (isaname,th) =>
    1.57 @@ -1236,6 +1242,7 @@
    1.58  
    1.59  fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
    1.60    let
    1.61 +      val _ = writeln "enter get_isabelle_thm_and_warn"
    1.62      val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
    1.63      fun warn () =
    1.64          let
    1.65 @@ -1254,13 +1261,13 @@
    1.66  	end
    1.67    in
    1.68        case b of 
    1.69 -	  NONE => (warn () handle _ => (); (a,b))
    1.70 -	| _ => (a, b)
    1.71 +	  NONE => (warn () handle _ => (); writeln "exit get_isabelle_thm_and_warn"; (a,b))
    1.72 +	| _ => (writeln "exit get_isabelle_thm_and_warn"; (a, b))
    1.73    end 
    1.74  
    1.75  fun get_thm thyname thmname thy =
    1.76      case get_hol4_thm thyname thmname thy of
    1.77 -	SOME hth => (thy,SOME hth)
    1.78 +	SOME hth => (writeln "got hol4 thm"; (thy,SOME hth))
    1.79        | NONE => ((case import_proof_concl thyname thmname thy of
    1.80  		      SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
    1.81  		    | NONE => (message "No conclusion"; (thy,NONE)))
    1.82 @@ -1640,7 +1647,7 @@
    1.83  
    1.84  fun GEN v hth thy =
    1.85      let
    1.86 -	val _ = message "GEN:"
    1.87 +	val _ = writeln "GEN:"
    1.88  	val _ = if_debug prin v
    1.89  	val _ = if_debug pth hth
    1.90  	val (info,th) = disamb_thm hth
    1.91 @@ -1648,6 +1655,7 @@
    1.92  	val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy))
    1.93  	val _ = message "RESULT:"
    1.94  	val _ = if_debug pth res
    1.95 +	val _ = writeln "exit GEN"
    1.96      in
    1.97  	(thy,res)
    1.98      end
    1.99 @@ -2074,9 +2082,16 @@
   1.100  	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy    
   1.101      end
   1.102  
   1.103 +(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
   1.104 +fun choose_upon_replay_history thy s dth = 
   1.105 +    case Symtab.lookup (!type_intro_replay_history) s of
   1.106 +	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
   1.107 +      | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
   1.108 +*)
   1.109 +
   1.110  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
   1.111      case HOL4DefThy.get thy of
   1.112 -	Replaying _ => (thy, HOLThm([], thm (thmname^"_@intern")) handle _ => hth)
   1.113 +	Replaying _ => (thy, handle_error (fn () => HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern")))) hth)
   1.114        | _ => 
   1.115  	let
   1.116              val _ = message "TYPE_INTRO:"
   1.117 @@ -2142,8 +2157,10 @@
   1.118  	    val isa_abs_name_def = isa_abs_name^"_symdest"
   1.119  	    val thy = add_dump_constdefs thy (SOME isa_rep_name_def) rep_name isa_rep_name rep_ty
   1.120  	    val thy = add_dump_constdefs thy (SOME isa_abs_name_def) abs_name isa_abs_name abs_ty
   1.121 -	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [OF "^(quotename ("type_definition_" ^ tycname)) ^ 
   1.122 -				" ,\n   simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
   1.123 +	    val str_aty = string_of_ctyp (ctyp_of thy aty)
   1.124 +	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [where a=\"a :: "^str_aty^"\" and r=r" ^
   1.125 +	                    " ,\n    OF "^(quotename ("type_definition_" ^ tycname)) ^ 
   1.126 +            		    " ,\n    simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
   1.127  	    val _ = message "RESULT:"
   1.128  	    val _ = if_debug pth hth'
   1.129  	in
     2.1 --- a/src/HOL/Import/replay.ML	Fri Sep 23 00:11:10 2005 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 23 00:52:13 2005 +0200
     2.3 @@ -77,9 +77,13 @@
     2.4  	    end
     2.5  	  | rp (PGen(prf,v)) thy =
     2.6  	    let
     2.7 +		val _ = writeln "enter rp PGen"
     2.8  		val (thy',th) = rp' prf thy
     2.9 +		val _ = writeln "replayed inner proof"
    2.10 +		val p = P.GEN v th thy'
    2.11 +		val _ = writeln "exit rp PGen"
    2.12  	    in
    2.13 -		P.GEN v th thy'
    2.14 +		p
    2.15  	    end
    2.16  	  | rp (PGenAbs(prf,opt,vl)) thy =
    2.17  	    let
    2.18 @@ -225,7 +229,7 @@
    2.19  				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
    2.20  				     | NONE => 
    2.21  				       (case P.get_thm thyname' thmname thy of
    2.22 -					    (thy',SOME res) => (thy',res)
    2.23 +					    (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
    2.24  					  | (thy',NONE) => 
    2.25  					    if thyname' = thyname
    2.26  					    then
    2.27 @@ -300,11 +304,15 @@
    2.28      let
    2.29  	fun replay_fact (thmname,thy) =
    2.30  	    let
    2.31 -		val _ = writeln ("Replaying " ^ thmname)
    2.32 +		val _ = writeln ("import_single_thm: Replaying " ^ thmname)
    2.33  		val prf = mk_proof PDisk
    2.34 +		val _ = writeln ("Made proof.")
    2.35  		val _ = set_disk_info_of prf thyname thmname
    2.36 +		val _ = writeln ("set disk info")	    
    2.37 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.38 +		val _ = writeln ("exit replay_fact")
    2.39  	    in
    2.40 -		fst (replay_proof int_thms thyname thmname prf thy)
    2.41 +		p
    2.42  	    end
    2.43      in
    2.44  	replay_fact (thmname,thy)
    2.45 @@ -314,11 +322,15 @@
    2.46      let
    2.47  	fun replay_fact (thy,thmname) =
    2.48  	    let
    2.49 -		val _ = writeln ("Replaying " ^ thmname)
    2.50 -		val prf = mk_proof PDisk
    2.51 -		val _ = set_disk_info_of prf thyname thmname
    2.52 +		val _ = writeln ("import_thms: Replaying " ^ thmname)
    2.53 +		val prf = mk_proof PDisk	
    2.54 +		val _ = writeln ("Made proof.")
    2.55 +		val _ = set_disk_info_of prf thyname thmname	
    2.56 +		val _ = writeln ("set disk info")	    
    2.57 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.58 +		val _ = writeln ("exit replay_fact")
    2.59  	    in
    2.60 -		fst (replay_proof int_thms thyname thmname prf thy)
    2.61 +		p
    2.62  	    end
    2.63  	val res_thy = Library.foldl replay_fact (thy,thmnames)
    2.64      in
    2.65 @@ -330,11 +342,15 @@
    2.66  	val int_thms = fst (setup_int_thms thyname thy)
    2.67  	fun replay_fact (thmname,thy) =
    2.68  	    let
    2.69 -		val _ = writeln ("Replaying " ^ thmname)
    2.70 -		val prf = mk_proof PDisk
    2.71 -		val _ = set_disk_info_of prf thyname thmname
    2.72 -	    in
    2.73 -		fst (replay_proof int_thms thyname thmname prf thy)
    2.74 +		val _ = writeln ("import_thm: Replaying " ^ thmname)
    2.75 +		val prf = mk_proof PDisk	
    2.76 +		val _ = writeln ("Made proof.")
    2.77 +		val _ = set_disk_info_of prf thyname thmname 
    2.78 +		val _ = writeln ("set disk info")	    
    2.79 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.80 +		val _ = writeln ("exit replay_fact")	    
    2.81 +	    in 
    2.82 +		p
    2.83  	    end
    2.84      in
    2.85  	replay_fact (thmname,thy)