src/HOL/Import/replay.ML
author skalberg
Fri Mar 04 15:07:34 2005 +0100 (2005-03-04)
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 17322 781abf7011e6
permissions -rw-r--r--
Removed practically all references to Library.foldr.
     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")
    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 (thy',th) = rp' prf thy
    81 	    in
    82 		P.GEN v th thy'
    83 	    end
    84 	  | rp (PGenAbs(prf,opt,vl)) thy =
    85 	    let
    86 		val (thy',th) = rp' prf thy
    87 	    in
    88 		P.GEN_ABS opt vl th thy'
    89 	    end
    90 	  | rp (PImpAS(prf1,prf2)) thy =
    91 	    let
    92 		val (thy1,th1) = rp' prf1 thy
    93 		val (thy2,th2) = rp' prf2 thy1
    94 	    in
    95 		P.IMP_ANTISYM th1 th2 thy2
    96 	    end
    97 	  | rp (PSym prf) thy =
    98 	    let
    99 		val (thy1,th) = rp' prf thy
   100 	    in
   101 		P.SYM th thy1
   102 	    end
   103 	  | rp (PTrans(prf1,prf2)) thy =
   104 	    let
   105 		val (thy1,th1) = rp' prf1 thy
   106 		val (thy2,th2) = rp' prf2 thy1
   107 	    in
   108 		P.TRANS th1 th2 thy2
   109 	    end
   110 	  | rp (PComb(prf1,prf2)) thy =
   111 	    let
   112 		val (thy1,th1) = rp' prf1 thy
   113 		val (thy2,th2) = rp' prf2 thy1
   114 	    in
   115 		P.COMB th1 th2 thy2
   116 	    end
   117 	  | rp (PEqMp(prf1,prf2)) thy =
   118 	    let
   119 		val (thy1,th1) = rp' prf1 thy
   120 		val (thy2,th2) = rp' prf2 thy1
   121 	    in
   122 		P.EQ_MP th1 th2 thy2
   123 	    end
   124 	  | rp (PEqImp prf) thy =
   125 	    let
   126 		val (thy',th) = rp' prf thy
   127 	    in
   128 		P.EQ_IMP_RULE th thy'
   129 	    end
   130 	  | rp (PExists(prf,ex,wit)) thy =
   131 	    let
   132 		val (thy',th) = rp' prf thy
   133 	    in
   134 		P.EXISTS ex wit th thy'
   135 	    end
   136 	  | rp (PChoose(v,prf1,prf2)) thy =
   137 	    let
   138 		val (thy1,th1) = rp' prf1 thy
   139 		val (thy2,th2) = rp' prf2 thy1
   140 	    in
   141 		P.CHOOSE v th1 th2 thy2
   142 	    end
   143 	  | rp (PConj(prf1,prf2)) thy =
   144 	    let
   145 		val (thy1,th1) = rp' prf1 thy
   146 		val (thy2,th2) = rp' prf2 thy1
   147 	    in
   148 		P.CONJ th1 th2 thy2
   149 	    end
   150 	  | rp (PConjunct1 prf) thy =
   151 	    let
   152 		val (thy',th) = rp' prf thy
   153 	    in
   154 		P.CONJUNCT1 th thy'
   155 	    end
   156 	  | rp (PConjunct2 prf) thy =
   157 	    let
   158 		val (thy',th) = rp' prf thy
   159 	    in
   160 		P.CONJUNCT2 th thy'
   161 	    end
   162 	  | rp (PDisj1(prf,tm)) thy =
   163 	    let
   164 		val (thy',th) = rp' prf thy
   165 	    in
   166 		P.DISJ1 th tm thy'
   167 	    end
   168 	  | rp (PDisj2(prf,tm)) thy =
   169 	    let
   170 		val (thy',th) = rp' prf thy
   171 	    in
   172 		P.DISJ2 tm th thy'
   173 	    end
   174 	  | rp (PDisjCases(prf,prf1,prf2)) thy =
   175 	    let
   176 		val (thy',th)  = rp' prf  thy
   177 		val (thy1,th1) = rp' prf1 thy'
   178 		val (thy2,th2) = rp' prf2 thy1
   179 	    in
   180 		P.DISJ_CASES th th1 th2 thy2
   181 	    end
   182 	  | rp (PNotI prf) thy =
   183 	    let
   184 		val (thy',th) = rp' prf thy
   185 	    in
   186 		P.NOT_INTRO th thy'
   187 	    end
   188 	  | rp (PNotE prf) thy =
   189 	    let
   190 		val (thy',th) = rp' prf thy
   191 	    in
   192 		P.NOT_ELIM th thy'
   193 	    end
   194 	  | rp (PContr(prf,tm)) thy =
   195 	    let
   196 		val (thy',th) = rp' prf thy
   197 	    in
   198 		P.CCONTR tm th thy'
   199 	    end
   200 	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   201 	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   202 	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   203 	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   204 	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   205 	and rp' p thy =
   206 	    let
   207 		val pc = content_of p
   208 	    in
   209 		case pc of
   210 		    PDisk => (case disk_info_of p of
   211 				  SOME(thyname',thmname) =>
   212 				  (case Int.fromString thmname of
   213 				       SOME i =>
   214 				       if thyname' = thyname
   215 				       then
   216 					   (case Array.sub(int_thms,i-1) of
   217 						NONE =>
   218 						let
   219 						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   220 						    val _ = Array.update(int_thms,i-1,SOME th)
   221 						in
   222 						    (thy',th)
   223 						end
   224 					      | SOME th => (thy,th))
   225 				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   226 				     | NONE => 
   227 				       (case P.get_thm thyname' thmname thy of
   228 					    (thy',SOME res) => (thy',res)
   229 					  | (thy',NONE) => 
   230 					    if thyname' = thyname
   231 					    then
   232 						let
   233 						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   234 						    val (f_opt,prf) = import_proof thyname' thmname thy'
   235 						    val prf = prf thy'
   236 						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   237 						in
   238 						    case content_of prf of
   239 							PTmSpec _ => (thy',th)
   240 						      | PTyDef  _ => (thy',th)
   241 						      | PTyIntro _ => (thy',th)
   242 						      | _ => P.store_thm thyname' thmname th thy'
   243 						end
   244 					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   245 				| NONE => raise ERR "rp'.PDisk" "Not enough information")
   246 		  | PAxm(name,c) =>
   247 		    (case P.get_axiom thyname name thy of
   248 			    (thy',SOME res) => (thy',res)
   249 			  | (thy',NONE) => P.new_axiom name c thy')
   250 		  | PTmSpec(seg,names,prf') =>
   251 		    let
   252 			val (thy',th) = rp' prf' thy
   253 		    in
   254 			P.new_specification seg thmname names th thy'
   255 		    end
   256 		  | PTyDef(seg,name,prf') =>
   257 		    let
   258 			val (thy',th) = rp' prf' thy
   259 		    in
   260 			P.new_type_definition seg thmname name th thy'
   261 		    end
   262 		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   263 		    let
   264 			val (thy',th) = rp' prf' thy
   265 		    in
   266 			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   267 		    end
   268 		  | _ => rp pc thy
   269 	    end
   270     in
   271 	rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
   272     end
   273 
   274 fun setup_int_thms thyname thy =
   275     let
   276 	val fname =
   277 	    case P.get_proof_dir thyname thy of
   278 		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   279 	      | NONE => error "Cannot find proof files"
   280 	val is = TextIO.openIn fname
   281 	val (num_int_thms,facts) =
   282 	    let
   283 		fun get_facts facts =
   284 		    case TextIO.inputLine is of
   285 			"" => (case facts of
   286 				   i::facts => (valOf (Int.fromString i),rev facts)
   287 				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   288 		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   289 	    in
   290 		get_facts []
   291 	    end
   292 	val _ = TextIO.closeIn is
   293 	val int_thms = Array.array(num_int_thms,NONE:thm option)
   294     in
   295 	(int_thms,facts)
   296     end
   297 
   298 fun import_single_thm thyname int_thms thmname thy =
   299     let
   300 	fun replay_fact (thmname,thy) =
   301 	    let
   302 		val _ = writeln ("Replaying " ^ thmname)
   303 		val prf = mk_proof PDisk
   304 		val _ = set_disk_info_of prf thyname thmname
   305 	    in
   306 		fst (replay_proof int_thms thyname thmname prf thy)
   307 	    end
   308     in
   309 	replay_fact (thmname,thy)
   310     end
   311 
   312 fun import_thms thyname int_thms thmnames thy =
   313     let
   314 	fun replay_fact (thy,thmname) =
   315 	    let
   316 		val _ = writeln ("Replaying " ^ thmname)
   317 		val prf = mk_proof PDisk
   318 		val _ = set_disk_info_of prf thyname thmname
   319 	    in
   320 		fst (replay_proof int_thms thyname thmname prf thy)
   321 	    end
   322 	val res_thy = Library.foldl replay_fact (thy,thmnames)
   323     in
   324 	res_thy
   325     end
   326 
   327 fun import_thm thyname thmname thy =
   328     let
   329 	val int_thms = fst (setup_int_thms thyname thy)
   330 	fun replay_fact (thmname,thy) =
   331 	    let
   332 		val _ = writeln ("Replaying " ^ thmname)
   333 		val prf = mk_proof PDisk
   334 		val _ = set_disk_info_of prf thyname thmname
   335 	    in
   336 		fst (replay_proof int_thms thyname thmname prf thy)
   337 	    end
   338     in
   339 	replay_fact (thmname,thy)
   340     end
   341 
   342 end