src/HOL/Import/replay.ML
author obua
Fri Sep 23 00:52:13 2005 +0200 (2005-09-23)
changeset 17592 ece268908438
parent 17440 df77edc4f5d0
child 17594 98be710dabc4
permissions -rw-r--r--
add debug messages
skalberg@14620
     1
(*  Title:      HOL/Import/replay.ML
skalberg@14620
     2
    ID:         $Id$
skalberg@14620
     3
    Author:     Sebastian Skalberg (TU Muenchen)
skalberg@14620
     4
*)
skalberg@14620
     5
skalberg@14516
     6
structure Replay =
skalberg@14516
     7
struct
skalberg@14516
     8
skalberg@14516
     9
structure P = ProofKernel
skalberg@14516
    10
skalberg@14516
    11
open ProofKernel
skalberg@14516
    12
skalberg@14516
    13
exception REPLAY of string * string
skalberg@14516
    14
fun ERR f mesg = REPLAY (f,mesg)
skalberg@14516
    15
fun NY f = raise ERR f "NOT YET!"
skalberg@14516
    16
skalberg@14516
    17
fun replay_proof int_thms thyname thmname prf thy =
skalberg@14516
    18
    let
skalberg@14516
    19
	fun rp (PRefl tm) thy = P.REFL tm thy
skalberg@14516
    20
	  | rp (PInstT(p,lambda)) thy =
skalberg@14516
    21
	    let
skalberg@14516
    22
		val (thy',th) = rp' p thy
skalberg@14516
    23
	    in
skalberg@14516
    24
		P.INST_TYPE lambda th thy'
skalberg@14516
    25
	    end
skalberg@14516
    26
	  | rp (PSubst(prfs,ctxt,prf)) thy =
skalberg@14516
    27
	    let
skalberg@15574
    28
		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
skalberg@14516
    29
					   let
skalberg@14516
    30
					       val (thy',th) = rp' p thy
skalberg@14516
    31
					   in
skalberg@14516
    32
					       (thy',th::ths)
skalberg@15574
    33
					   end) (thy,[]) prfs
skalberg@14516
    34
		val (thy'',th) = rp' prf thy'
skalberg@14516
    35
	    in
skalberg@14516
    36
		P.SUBST ths ctxt th thy''
skalberg@14516
    37
	    end
skalberg@14516
    38
	  | rp (PAbs(prf,v)) thy =
skalberg@14516
    39
	    let
skalberg@14516
    40
		val (thy',th) = rp' prf thy
skalberg@14516
    41
	    in
skalberg@14516
    42
		P.ABS v th thy'
skalberg@14516
    43
	    end
skalberg@14516
    44
	  | rp (PDisch(prf,tm)) thy =
skalberg@14516
    45
	    let
skalberg@14516
    46
		val (thy',th) = rp' prf thy
skalberg@14516
    47
	    in
skalberg@14516
    48
		P.DISCH tm th thy'
skalberg@14516
    49
	    end
skalberg@14516
    50
	  | rp (PMp(prf1,prf2)) thy =
skalberg@14516
    51
	    let
skalberg@14516
    52
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
    53
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
    54
	    in
skalberg@14516
    55
		P.MP th1 th2 thy2
skalberg@14516
    56
	    end
skalberg@14516
    57
	  | rp (PHyp tm) thy = P.ASSUME tm thy
skalberg@14516
    58
	  | rp (PDef(seg,name,rhs)) thy =
skalberg@14516
    59
	    (case P.get_def seg name rhs thy of
skalberg@15531
    60
		 (thy',SOME res) => (thy',res)
skalberg@15531
    61
	       | (thy',NONE) => 
skalberg@14516
    62
		 if seg = thyname
skalberg@14516
    63
		 then P.new_definition seg name rhs thy'
obua@17322
    64
		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
skalberg@14516
    65
	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
skalberg@14516
    66
	  | rp (PSpec(prf,tm)) thy =
skalberg@14516
    67
	    let
skalberg@14516
    68
		val (thy',th) = rp' prf thy
skalberg@14516
    69
	    in
skalberg@14516
    70
		P.SPEC tm th thy'
skalberg@14516
    71
	    end
skalberg@14516
    72
	  | rp (PInst(prf,theta)) thy =
skalberg@14516
    73
	    let
skalberg@14516
    74
		val (thy',th) = rp' prf thy
skalberg@14516
    75
	    in
skalberg@14516
    76
		P.INST theta th thy'
skalberg@14516
    77
	    end
skalberg@14516
    78
	  | rp (PGen(prf,v)) thy =
skalberg@14516
    79
	    let
obua@17592
    80
		val _ = writeln "enter rp PGen"
skalberg@14516
    81
		val (thy',th) = rp' prf thy
obua@17592
    82
		val _ = writeln "replayed inner proof"
obua@17592
    83
		val p = P.GEN v th thy'
obua@17592
    84
		val _ = writeln "exit rp PGen"
skalberg@14516
    85
	    in
obua@17592
    86
		p
skalberg@14516
    87
	    end
skalberg@14516
    88
	  | rp (PGenAbs(prf,opt,vl)) thy =
skalberg@14516
    89
	    let
skalberg@14516
    90
		val (thy',th) = rp' prf thy
skalberg@14516
    91
	    in
skalberg@14516
    92
		P.GEN_ABS opt vl th thy'
skalberg@14516
    93
	    end
skalberg@14516
    94
	  | rp (PImpAS(prf1,prf2)) thy =
skalberg@14516
    95
	    let
skalberg@14516
    96
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
    97
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
    98
	    in
skalberg@14516
    99
		P.IMP_ANTISYM th1 th2 thy2
skalberg@14516
   100
	    end
skalberg@14516
   101
	  | rp (PSym prf) thy =
skalberg@14516
   102
	    let
skalberg@14516
   103
		val (thy1,th) = rp' prf thy
skalberg@14516
   104
	    in
skalberg@14516
   105
		P.SYM th thy1
skalberg@14516
   106
	    end
skalberg@14516
   107
	  | rp (PTrans(prf1,prf2)) thy =
skalberg@14516
   108
	    let
skalberg@14516
   109
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   110
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   111
	    in
skalberg@14516
   112
		P.TRANS th1 th2 thy2
skalberg@14516
   113
	    end
skalberg@14516
   114
	  | rp (PComb(prf1,prf2)) thy =
skalberg@14516
   115
	    let
skalberg@14516
   116
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   117
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   118
	    in
skalberg@14516
   119
		P.COMB th1 th2 thy2
skalberg@14516
   120
	    end
skalberg@14516
   121
	  | rp (PEqMp(prf1,prf2)) thy =
skalberg@14516
   122
	    let
skalberg@14516
   123
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   124
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   125
	    in
skalberg@14516
   126
		P.EQ_MP th1 th2 thy2
skalberg@14516
   127
	    end
skalberg@14516
   128
	  | rp (PEqImp prf) thy =
skalberg@14516
   129
	    let
skalberg@14516
   130
		val (thy',th) = rp' prf thy
skalberg@14516
   131
	    in
skalberg@14516
   132
		P.EQ_IMP_RULE th thy'
skalberg@14516
   133
	    end
skalberg@14516
   134
	  | rp (PExists(prf,ex,wit)) thy =
skalberg@14516
   135
	    let
skalberg@14516
   136
		val (thy',th) = rp' prf thy
skalberg@14516
   137
	    in
skalberg@14516
   138
		P.EXISTS ex wit th thy'
skalberg@14516
   139
	    end
skalberg@14516
   140
	  | rp (PChoose(v,prf1,prf2)) thy =
skalberg@14516
   141
	    let
skalberg@14516
   142
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   143
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   144
	    in
skalberg@14516
   145
		P.CHOOSE v th1 th2 thy2
skalberg@14516
   146
	    end
skalberg@14516
   147
	  | rp (PConj(prf1,prf2)) thy =
skalberg@14516
   148
	    let
skalberg@14516
   149
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   150
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   151
	    in
skalberg@14516
   152
		P.CONJ th1 th2 thy2
skalberg@14516
   153
	    end
skalberg@14516
   154
	  | rp (PConjunct1 prf) thy =
skalberg@14516
   155
	    let
skalberg@14516
   156
		val (thy',th) = rp' prf thy
skalberg@14516
   157
	    in
skalberg@14516
   158
		P.CONJUNCT1 th thy'
skalberg@14516
   159
	    end
skalberg@14516
   160
	  | rp (PConjunct2 prf) thy =
skalberg@14516
   161
	    let
skalberg@14516
   162
		val (thy',th) = rp' prf thy
skalberg@14516
   163
	    in
skalberg@14516
   164
		P.CONJUNCT2 th thy'
skalberg@14516
   165
	    end
skalberg@14516
   166
	  | rp (PDisj1(prf,tm)) thy =
skalberg@14516
   167
	    let
skalberg@14516
   168
		val (thy',th) = rp' prf thy
skalberg@14516
   169
	    in
skalberg@14516
   170
		P.DISJ1 th tm thy'
skalberg@14516
   171
	    end
skalberg@14516
   172
	  | rp (PDisj2(prf,tm)) thy =
skalberg@14516
   173
	    let
skalberg@14516
   174
		val (thy',th) = rp' prf thy
skalberg@14516
   175
	    in
skalberg@14516
   176
		P.DISJ2 tm th thy'
skalberg@14516
   177
	    end
skalberg@14516
   178
	  | rp (PDisjCases(prf,prf1,prf2)) thy =
skalberg@14516
   179
	    let
skalberg@14516
   180
		val (thy',th)  = rp' prf  thy
skalberg@14516
   181
		val (thy1,th1) = rp' prf1 thy'
skalberg@14516
   182
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   183
	    in
skalberg@14516
   184
		P.DISJ_CASES th th1 th2 thy2
skalberg@14516
   185
	    end
skalberg@14516
   186
	  | rp (PNotI prf) thy =
skalberg@14516
   187
	    let
skalberg@14516
   188
		val (thy',th) = rp' prf thy
skalberg@14516
   189
	    in
skalberg@14516
   190
		P.NOT_INTRO th thy'
skalberg@14516
   191
	    end
skalberg@14516
   192
	  | rp (PNotE prf) thy =
skalberg@14516
   193
	    let
skalberg@14516
   194
		val (thy',th) = rp' prf thy
skalberg@14516
   195
	    in
skalberg@14516
   196
		P.NOT_ELIM th thy'
skalberg@14516
   197
	    end
skalberg@14516
   198
	  | rp (PContr(prf,tm)) thy =
skalberg@14516
   199
	    let
skalberg@14516
   200
		val (thy',th) = rp' prf thy
skalberg@14516
   201
	    in
skalberg@14516
   202
		P.CCONTR tm th thy'
skalberg@14516
   203
	    end
skalberg@14516
   204
	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
skalberg@14516
   205
	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
skalberg@14516
   206
	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
skalberg@14516
   207
	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
skalberg@14516
   208
	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
skalberg@14516
   209
	and rp' p thy =
skalberg@14516
   210
	    let
skalberg@14516
   211
		val pc = content_of p
skalberg@14516
   212
	    in
skalberg@14516
   213
		case pc of
skalberg@14516
   214
		    PDisk => (case disk_info_of p of
skalberg@15531
   215
				  SOME(thyname',thmname) =>
skalberg@14516
   216
				  (case Int.fromString thmname of
skalberg@14516
   217
				       SOME i =>
skalberg@14516
   218
				       if thyname' = thyname
skalberg@14516
   219
				       then
skalberg@14516
   220
					   (case Array.sub(int_thms,i-1) of
skalberg@15531
   221
						NONE =>
skalberg@14516
   222
						let
skalberg@14516
   223
						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
skalberg@15531
   224
						    val _ = Array.update(int_thms,i-1,SOME th)
skalberg@14516
   225
						in
skalberg@14516
   226
						    (thy',th)
skalberg@14516
   227
						end
skalberg@15531
   228
					      | SOME th => (thy,th))
skalberg@14516
   229
				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
skalberg@14516
   230
				     | NONE => 
skalberg@14516
   231
				       (case P.get_thm thyname' thmname thy of
obua@17592
   232
					    (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
skalberg@15531
   233
					  | (thy',NONE) => 
skalberg@14516
   234
					    if thyname' = thyname
skalberg@14516
   235
					    then
skalberg@14516
   236
						let
skalberg@14516
   237
						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
skalberg@14516
   238
						    val (f_opt,prf) = import_proof thyname' thmname thy'
skalberg@14516
   239
						    val prf = prf thy'
skalberg@14516
   240
						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
obua@17322
   241
                                                    val _ = writeln ("Successfully finished replaying "^thmname^" !")
skalberg@14516
   242
						in
skalberg@14516
   243
						    case content_of prf of
skalberg@14516
   244
							PTmSpec _ => (thy',th)
skalberg@14516
   245
						      | PTyDef  _ => (thy',th)
skalberg@14516
   246
						      | PTyIntro _ => (thy',th)
skalberg@14516
   247
						      | _ => P.store_thm thyname' thmname th thy'
skalberg@14516
   248
						end
skalberg@14516
   249
					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
skalberg@15531
   250
				| NONE => raise ERR "rp'.PDisk" "Not enough information")
skalberg@14516
   251
		  | PAxm(name,c) =>
skalberg@14516
   252
		    (case P.get_axiom thyname name thy of
skalberg@15531
   253
			    (thy',SOME res) => (thy',res)
skalberg@15531
   254
			  | (thy',NONE) => P.new_axiom name c thy')
skalberg@14516
   255
		  | PTmSpec(seg,names,prf') =>
skalberg@14516
   256
		    let
skalberg@14516
   257
			val (thy',th) = rp' prf' thy
skalberg@14516
   258
		    in
skalberg@14516
   259
			P.new_specification seg thmname names th thy'
skalberg@14516
   260
		    end
skalberg@14516
   261
		  | PTyDef(seg,name,prf') =>
skalberg@14516
   262
		    let
skalberg@14516
   263
			val (thy',th) = rp' prf' thy
skalberg@14516
   264
		    in
skalberg@14516
   265
			P.new_type_definition seg thmname name th thy'
skalberg@14516
   266
		    end
skalberg@14516
   267
		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
skalberg@14516
   268
		    let
skalberg@14516
   269
			val (thy',th) = rp' prf' thy
skalberg@14516
   270
		    in
skalberg@14516
   271
			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
skalberg@14516
   272
		    end
skalberg@14516
   273
		  | _ => rp pc thy
skalberg@14516
   274
	    end
skalberg@14516
   275
    in
skalberg@14516
   276
	rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
skalberg@14516
   277
    end
skalberg@14516
   278
skalberg@14516
   279
fun setup_int_thms thyname thy =
skalberg@14516
   280
    let
skalberg@14620
   281
	val fname =
skalberg@14620
   282
	    case P.get_proof_dir thyname thy of
skalberg@15531
   283
		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
skalberg@15531
   284
	      | NONE => error "Cannot find proof files"
skalberg@14620
   285
	val is = TextIO.openIn fname
skalberg@14516
   286
	val (num_int_thms,facts) =
skalberg@14516
   287
	    let
skalberg@14516
   288
		fun get_facts facts =
skalberg@14516
   289
		    case TextIO.inputLine is of
skalberg@14516
   290
			"" => (case facts of
obua@17440
   291
				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
skalberg@14516
   292
				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
skalberg@14516
   293
		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
skalberg@14516
   294
	    in
skalberg@14516
   295
		get_facts []
skalberg@14516
   296
	    end
skalberg@14516
   297
	val _ = TextIO.closeIn is
skalberg@15531
   298
	val int_thms = Array.array(num_int_thms,NONE:thm option)
skalberg@14516
   299
    in
skalberg@14516
   300
	(int_thms,facts)
skalberg@14516
   301
    end
skalberg@14516
   302
skalberg@14516
   303
fun import_single_thm thyname int_thms thmname thy =
skalberg@14516
   304
    let
skalberg@14516
   305
	fun replay_fact (thmname,thy) =
skalberg@14516
   306
	    let
obua@17592
   307
		val _ = writeln ("import_single_thm: Replaying " ^ thmname)
skalberg@14516
   308
		val prf = mk_proof PDisk
obua@17592
   309
		val _ = writeln ("Made proof.")
skalberg@14516
   310
		val _ = set_disk_info_of prf thyname thmname
obua@17592
   311
		val _ = writeln ("set disk info")	    
obua@17592
   312
		val p = fst (replay_proof int_thms thyname thmname prf thy)
obua@17592
   313
		val _ = writeln ("exit replay_fact")
skalberg@14516
   314
	    in
obua@17592
   315
		p
skalberg@14516
   316
	    end
skalberg@14516
   317
    in
skalberg@14516
   318
	replay_fact (thmname,thy)
skalberg@14516
   319
    end
skalberg@14516
   320
skalberg@14516
   321
fun import_thms thyname int_thms thmnames thy =
skalberg@14516
   322
    let
skalberg@14516
   323
	fun replay_fact (thy,thmname) =
skalberg@14516
   324
	    let
obua@17592
   325
		val _ = writeln ("import_thms: Replaying " ^ thmname)
obua@17592
   326
		val prf = mk_proof PDisk	
obua@17592
   327
		val _ = writeln ("Made proof.")
obua@17592
   328
		val _ = set_disk_info_of prf thyname thmname	
obua@17592
   329
		val _ = writeln ("set disk info")	    
obua@17592
   330
		val p = fst (replay_proof int_thms thyname thmname prf thy)
obua@17592
   331
		val _ = writeln ("exit replay_fact")
skalberg@14516
   332
	    in
obua@17592
   333
		p
skalberg@14516
   334
	    end
skalberg@15570
   335
	val res_thy = Library.foldl replay_fact (thy,thmnames)
skalberg@14516
   336
    in
skalberg@14516
   337
	res_thy
skalberg@14516
   338
    end
skalberg@14516
   339
skalberg@14516
   340
fun import_thm thyname thmname thy =
skalberg@14516
   341
    let
skalberg@14516
   342
	val int_thms = fst (setup_int_thms thyname thy)
skalberg@14516
   343
	fun replay_fact (thmname,thy) =
skalberg@14516
   344
	    let
obua@17592
   345
		val _ = writeln ("import_thm: Replaying " ^ thmname)
obua@17592
   346
		val prf = mk_proof PDisk	
obua@17592
   347
		val _ = writeln ("Made proof.")
obua@17592
   348
		val _ = set_disk_info_of prf thyname thmname 
obua@17592
   349
		val _ = writeln ("set disk info")	    
obua@17592
   350
		val p = fst (replay_proof int_thms thyname thmname prf thy)
obua@17592
   351
		val _ = writeln ("exit replay_fact")	    
obua@17592
   352
	    in 
obua@17592
   353
		p
skalberg@14516
   354
	    end
skalberg@14516
   355
    in
skalberg@14516
   356
	replay_fact (thmname,thy)
skalberg@14516
   357
    end
skalberg@14516
   358
obua@17440
   359
end