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