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