src/HOL/Import/replay.ML
author obua
Thu Feb 16 04:17:19 2006 +0100 (2006-02-16)
changeset 19067 c0321d7d6b3d
parent 19064 bf19cc5a7899
child 19068 04b302f2902d
permissions -rw-r--r--
variable counter is now also cached
     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 open ImportRecorder
    13 
    14 exception REPLAY of string * string
    15 fun ERR f mesg = REPLAY (f,mesg)
    16 fun NY f = raise ERR f "NOT YET!"
    17 
    18 fun replay_proof int_thms thyname thmname prf thy =
    19     let
    20 	val _ = ImportRecorder.start_replay_proof thyname thmname 
    21 	fun rp (PRefl tm) thy = P.REFL tm thy
    22 	  | rp (PInstT(p,lambda)) thy =
    23 	    let
    24 		val (thy',th) = rp' p thy
    25 	    in
    26 		P.INST_TYPE lambda th thy'
    27 	    end
    28 	  | rp (PSubst(prfs,ctxt,prf)) thy =
    29 	    let
    30 		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
    31 					   let
    32 					       val (thy',th) = rp' p thy
    33 					   in
    34 					       (thy',th::ths)
    35 					   end) (thy,[]) prfs
    36 		val (thy'',th) = rp' prf thy'
    37 	    in
    38 		P.SUBST ths ctxt th thy''
    39 	    end
    40 	  | rp (PAbs(prf,v)) thy =
    41 	    let
    42 		val (thy',th) = rp' prf thy
    43 	    in
    44 		P.ABS v th thy'
    45 	    end
    46 	  | rp (PDisch(prf,tm)) thy =
    47 	    let
    48 		val (thy',th) = rp' prf thy
    49 	    in
    50 		P.DISCH tm th thy'
    51 	    end
    52 	  | rp (PMp(prf1,prf2)) thy =
    53 	    let
    54 		val (thy1,th1) = rp' prf1 thy
    55 		val (thy2,th2) = rp' prf2 thy1
    56 	    in
    57 		P.MP th1 th2 thy2
    58 	    end
    59 	  | rp (PHyp tm) thy = P.ASSUME tm thy
    60 	  | rp (PDef(seg,name,rhs)) thy =
    61 	    (case P.get_def seg name rhs thy of
    62 		 (thy',SOME res) => (thy',res)
    63 	       | (thy',NONE) => 
    64 		 if seg = thyname
    65 		 then P.new_definition seg name rhs thy'
    66 		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    67 	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    68 	  | rp (PSpec(prf,tm)) thy =
    69 	    let
    70 		val (thy',th) = rp' prf thy
    71 	    in
    72 		P.SPEC tm th thy'
    73 	    end
    74 	  | rp (PInst(prf,theta)) thy =
    75 	    let
    76 		val (thy',th) = rp' prf thy
    77 	    in
    78 		P.INST theta th thy'
    79 	    end
    80 	  | rp (PGen(prf,v)) thy =
    81 	    let
    82 		val (thy',th) = rp' prf thy
    83 		val p = P.GEN v th thy'
    84 	    in
    85 		p
    86 	    end
    87 	  | rp (PGenAbs(prf,opt,vl)) thy =
    88 	    let
    89 		val (thy',th) = rp' prf thy
    90 	    in
    91 		P.GEN_ABS opt vl th thy'
    92 	    end
    93 	  | rp (PImpAS(prf1,prf2)) thy =
    94 	    let
    95 		val (thy1,th1) = rp' prf1 thy
    96 		val (thy2,th2) = rp' prf2 thy1
    97 	    in
    98 		P.IMP_ANTISYM th1 th2 thy2
    99 	    end
   100 	  | rp (PSym prf) thy =
   101 	    let
   102 		val (thy1,th) = rp' prf thy
   103 	    in
   104 		P.SYM th thy1
   105 	    end
   106 	  | rp (PTrans(prf1,prf2)) thy =
   107 	    let
   108 		val (thy1,th1) = rp' prf1 thy
   109 		val (thy2,th2) = rp' prf2 thy1
   110 	    in
   111 		P.TRANS th1 th2 thy2
   112 	    end
   113 	  | rp (PComb(prf1,prf2)) thy =
   114 	    let
   115 		val (thy1,th1) = rp' prf1 thy
   116 		val (thy2,th2) = rp' prf2 thy1
   117 	    in
   118 		P.COMB th1 th2 thy2
   119 	    end
   120 	  | rp (PEqMp(prf1,prf2)) thy =
   121 	    let
   122 		val (thy1,th1) = rp' prf1 thy
   123 		val (thy2,th2) = rp' prf2 thy1
   124 	    in
   125 		P.EQ_MP th1 th2 thy2
   126 	    end
   127 	  | rp (PEqImp prf) thy =
   128 	    let
   129 		val (thy',th) = rp' prf thy
   130 	    in
   131 		P.EQ_IMP_RULE th thy'
   132 	    end
   133 	  | rp (PExists(prf,ex,wit)) thy =
   134 	    let
   135 		val (thy',th) = rp' prf thy
   136 	    in
   137 		P.EXISTS ex wit th thy'
   138 	    end
   139 	  | rp (PChoose(v,prf1,prf2)) thy =
   140 	    let
   141 		val (thy1,th1) = rp' prf1 thy
   142 		val (thy2,th2) = rp' prf2 thy1
   143 	    in
   144 		P.CHOOSE v th1 th2 thy2
   145 	    end
   146 	  | rp (PConj(prf1,prf2)) thy =
   147 	    let
   148 		val (thy1,th1) = rp' prf1 thy
   149 		val (thy2,th2) = rp' prf2 thy1
   150 	    in
   151 		P.CONJ th1 th2 thy2
   152 	    end
   153 	  | rp (PConjunct1 prf) thy =
   154 	    let
   155 		val (thy',th) = rp' prf thy
   156 	    in
   157 		P.CONJUNCT1 th thy'
   158 	    end
   159 	  | rp (PConjunct2 prf) thy =
   160 	    let
   161 		val (thy',th) = rp' prf thy
   162 	    in
   163 		P.CONJUNCT2 th thy'
   164 	    end
   165 	  | rp (PDisj1(prf,tm)) thy =
   166 	    let
   167 		val (thy',th) = rp' prf thy
   168 	    in
   169 		P.DISJ1 th tm thy'
   170 	    end
   171 	  | rp (PDisj2(prf,tm)) thy =
   172 	    let
   173 		val (thy',th) = rp' prf thy
   174 	    in
   175 		P.DISJ2 tm th thy'
   176 	    end
   177 	  | rp (PDisjCases(prf,prf1,prf2)) thy =
   178 	    let
   179 		val (thy',th)  = rp' prf  thy
   180 		val (thy1,th1) = rp' prf1 thy'
   181 		val (thy2,th2) = rp' prf2 thy1
   182 	    in
   183 		P.DISJ_CASES th th1 th2 thy2
   184 	    end
   185 	  | rp (PNotI prf) thy =
   186 	    let
   187 		val (thy',th) = rp' prf thy
   188 	    in
   189 		P.NOT_INTRO th thy'
   190 	    end
   191 	  | rp (PNotE prf) thy =
   192 	    let
   193 		val (thy',th) = rp' prf thy
   194 	    in
   195 		P.NOT_ELIM th thy'
   196 	    end
   197 	  | rp (PContr(prf,tm)) thy =
   198 	    let
   199 		val (thy',th) = rp' prf thy
   200 	    in
   201 		P.CCONTR tm th thy'
   202 	    end
   203 	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   204 	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   205 	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   206 	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   207 	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   208 	and rp' p thy =
   209 	    let
   210 		val pc = content_of p
   211 	    in
   212 		case pc of
   213 		    PDisk => (case disk_info_of p of
   214 				  SOME(thyname',thmname) =>
   215 				  (case Int.fromString thmname of
   216 				       SOME i =>
   217 				       if thyname' = thyname
   218 				       then
   219 					   (case Array.sub(int_thms,i-1) of
   220 						NONE =>
   221 						let
   222 						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   223 						    val _ = Array.update(int_thms,i-1,SOME th)
   224 						in
   225 						    (thy',th)
   226 						end
   227 					      | SOME th => (thy,th))
   228 				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   229 				     | NONE => 
   230 				       (case P.get_thm thyname' thmname thy of
   231 					    (thy',SOME res) => (thy',res)
   232 					  | (thy',NONE) => 
   233 					    if thyname' = thyname
   234 					    then
   235 						let
   236 						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   237 						    val (f_opt,prf) = import_proof thyname' thmname thy'
   238 						    val prf = prf thy'
   239 						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   240                                                     val _ = writeln ("Successfully finished replaying "^thmname^" !")
   241 						in
   242 						    case content_of prf of
   243 							PTmSpec _ => (thy',th)
   244 						      | PTyDef  _ => (thy',th)
   245 						      | PTyIntro _ => (thy',th)
   246 						      | _ => P.store_thm thyname' thmname th thy'
   247 						end
   248 					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   249 				| NONE => raise ERR "rp'.PDisk" "Not enough information")
   250 		  | PAxm(name,c) =>
   251 		    (case P.get_axiom thyname name thy of
   252 			    (thy',SOME res) => (thy',res)
   253 			  | (thy',NONE) => P.new_axiom name c thy')
   254 		  | PTmSpec(seg,names,prf') =>
   255 		    let
   256 			val (thy',th) = rp' prf' thy
   257 		    in
   258 			P.new_specification seg thmname names th thy'
   259 		    end
   260 		  | PTyDef(seg,name,prf') =>
   261 		    let
   262 			val (thy',th) = rp' prf' thy
   263 		    in
   264 			P.new_type_definition seg thmname name th thy'
   265 		    end
   266 		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   267 		    let
   268 			val (thy',th) = rp' prf' thy
   269 		    in
   270 			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   271 		    end
   272 		  | _ => rp pc thy
   273 	    end
   274     in
   275 	let
   276 	    val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
   277 	    val _ = ImportRecorder.stop_replay_proof thyname thmname
   278 	in
   279 	    x
   280 	end
   281     end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
   282 
   283 fun setup_int_thms thyname thy =
   284     let
   285 	val fname =
   286 	    case P.get_proof_dir thyname thy of
   287 		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   288 	      | NONE => error "Cannot find proof files"
   289 	val is = TextIO.openIn fname
   290 	val (num_int_thms,facts) =
   291 	    let
   292 		fun get_facts facts =
   293 		    case TextIO.inputLine is of
   294 			"" => (case facts of
   295 				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
   296 				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   297 		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   298 	    in
   299 		get_facts []
   300 	    end
   301 	val _ = TextIO.closeIn is
   302 	val int_thms = Array.array(num_int_thms,NONE:thm option)
   303     in
   304 	(int_thms,facts)
   305     end
   306 
   307 fun import_single_thm thyname int_thms thmname thy =
   308     let
   309 	fun replay_fact (thmname,thy) =
   310 	    let
   311 		val prf = mk_proof PDisk
   312 		val _ = set_disk_info_of prf thyname thmname
   313                 val _ = writeln ("Replaying "^thmname^" ...")
   314 		val p = fst (replay_proof int_thms thyname thmname prf thy)
   315 	    in
   316 		p
   317 	    end
   318     in
   319 	replay_fact (thmname,thy)
   320     end
   321 
   322 fun replay_chached_thm int_thms thyname thmname =
   323     let
   324 	fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
   325 	fun err msg = raise ERR "replay_cached_thm" msg
   326 	val _ = writeln ("Replaying (from cache) "^thmname^" ...")
   327 	fun rps [] thy = thy
   328 	  | rps (t::ts) thy = rps ts (rp t thy)
   329 	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
   330 	  | rp (DeltaEntry ds) thy = fold delta ds thy
   331 (*    datatype deltastate = Consts of (string * typ * mixfix) list
   332 			| Specification of (string * string * bool) list * term
   333 			| Hol_mapping of string * string * string
   334 			| Hol_pending of string * string * term
   335 			| Hol_const_mapping of string * string * string
   336 			| Hol_move of string * string
   337 			| Defs of string * term
   338 			| Hol_theorem of string * string * term
   339 			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
   340 			| Hol_type_mapping of string * string * string
   341 			| Indexed_theorem of int * term
   342 *)
   343 	and delta (Specification (names, th)) thy = 
   344 	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
   345 	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
   346 	    add_hol4_mapping thyname thmname isaname thy
   347 	  | delta (Hol_pending (thyname, thmname, th)) thy = 
   348 	    add_hol4_pending thyname thmname ([], th_of thy th) thy
   349 	  | delta (Consts cs) thy = Theory.add_consts_i cs thy
   350 	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
   351 	    add_hol4_const_mapping thyname constname true fullcname thy
   352 	  | delta (Hol_move (fullname, moved_thmname)) thy = 
   353 	    add_hol4_move fullname moved_thmname thy
   354 	  | delta (Defs (thmname, eq)) thy =
   355 	    snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
   356 	  | delta (Hol_theorem (thyname, thmname, th)) thy =
   357 	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
   358 	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
   359 	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
   360 	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   361 	    add_hol4_type_mapping thyname tycname true fulltyname thy
   362 	  | delta (Indexed_theorem (i, th)) thy = 
   363 	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
   364           | delta (Protect_varname (s,t)) thy =
   365 	    (P.replay_protect_varname s t; thy)
   366     in
   367 	rps
   368     end
   369 
   370 fun import_thms thyname int_thms thmnames thy =
   371     let
   372 	fun zip names [] = ([], names)
   373 	  | zip [] _ = ([], [])
   374 	  | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
   375 	    if thyname = thyname' andalso thmname = thmname' then
   376 		(if aborted then ([], thmname::names) else 
   377 		 let
   378 		     val _ = writeln ("theorem is in-sync: "^thmname)
   379 		     val (cached,normal) = zip names ys
   380 		 in
   381 		     (entry::cached, normal)
   382 		 end)
   383 	    else
   384 		raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
   385 	  | zip (thmname::_) (DeltaEntry _ :: _) = 
   386  	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   387 	fun zip' xs (History ys) = 
   388 	    let
   389 		val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   390 		val _ = writeln ("length of history: "^(string_of_int (length ys)))
   391 	    in
   392 		zip xs ys
   393 	    end
   394 	fun replay_fact thmname thy = 
   395 	    let
   396 		val prf = mk_proof PDisk	
   397 		val _ = set_disk_info_of prf thyname thmname
   398                 val _ = writeln ("Replaying "^thmname^" ...")
   399 		val p = fst (replay_proof int_thms thyname thmname prf thy)
   400 	    in
   401 		p
   402 	    end
   403 	fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   404 	val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   405 	val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   406 	val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   407     in
   408 	res_thy
   409     end
   410 
   411 fun import_thm thyname thmname thy =
   412     let
   413 	val int_thms = fst (setup_int_thms thyname thy)
   414 	fun replay_fact (thmname,thy) =
   415 	    let
   416 		val prf = mk_proof PDisk	
   417 		val _ = set_disk_info_of prf thyname thmname 	    
   418                 val _ = writeln ("Replaying "^thmname^" ...")
   419 		val p = fst (replay_proof int_thms thyname thmname prf thy)
   420 	    in 
   421 		p
   422 	    end
   423     in
   424 	replay_fact (thmname,thy)
   425     end
   426 
   427 end