src/HOL/Import/replay.ML
changeset 19064 bf19cc5a7899
parent 17959 8db36a108213
child 19067 c0321d7d6b3d
     1.1 --- a/src/HOL/Import/replay.ML	Wed Feb 15 21:35:13 2006 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Feb 15 23:57:06 2006 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  structure P = ProofKernel
     1.5  
     1.6  open ProofKernel
     1.7 +open ImportRecorder
     1.8  
     1.9  exception REPLAY of string * string
    1.10  fun ERR f mesg = REPLAY (f,mesg)
    1.11 @@ -16,6 +17,7 @@
    1.12  
    1.13  fun replay_proof int_thms thyname thmname prf thy =
    1.14      let
    1.15 +	val _ = ImportRecorder.start_replay_proof thyname thmname 
    1.16  	fun rp (PRefl tm) thy = P.REFL tm thy
    1.17  	  | rp (PInstT(p,lambda)) thy =
    1.18  	    let
    1.19 @@ -270,8 +272,13 @@
    1.20  		  | _ => rp pc thy
    1.21  	    end
    1.22      in
    1.23 -	rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
    1.24 -    end
    1.25 +	let
    1.26 +	    val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
    1.27 +	    val _ = ImportRecorder.stop_replay_proof thyname thmname
    1.28 +	in
    1.29 +	    x
    1.30 +	end
    1.31 +    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
    1.32  
    1.33  fun setup_int_thms thyname thy =
    1.34      let
    1.35 @@ -312,9 +319,77 @@
    1.36  	replay_fact (thmname,thy)
    1.37      end
    1.38  
    1.39 +fun replay_chached_thm int_thms thyname thmname =
    1.40 +    let
    1.41 +	fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
    1.42 +	fun err msg = raise ERR "replay_cached_thm" msg
    1.43 +	val _ = writeln ("Replaying (from cache) "^thmname^" ...")
    1.44 +	fun rps [] thy = thy
    1.45 +	  | rps (t::ts) thy = rps ts (rp t thy)
    1.46 +	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
    1.47 +	  | rp (DeltaEntry ds) thy = fold delta ds thy
    1.48 +(*    datatype deltastate = Consts of (string * typ * mixfix) list
    1.49 +			| Specification of (string * string * bool) list * term
    1.50 +			| Hol_mapping of string * string * string
    1.51 +			| Hol_pending of string * string * term
    1.52 +			| Hol_const_mapping of string * string * string
    1.53 +			| Hol_move of string * string
    1.54 +			| Defs of string * term
    1.55 +			| Hol_theorem of string * string * term
    1.56 +			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
    1.57 +			| Hol_type_mapping of string * string * string
    1.58 +			| Indexed_theorem of int * term
    1.59 +*)
    1.60 +	and delta (Specification (names, th)) thy = 
    1.61 +	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
    1.62 +	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
    1.63 +	    add_hol4_mapping thyname thmname isaname thy
    1.64 +	  | delta (Hol_pending (thyname, thmname, th)) thy = 
    1.65 +	    add_hol4_pending thyname thmname ([], th_of thy th) thy
    1.66 +	  | delta (Consts cs) thy = Theory.add_consts_i cs thy
    1.67 +	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
    1.68 +	    add_hol4_const_mapping thyname constname true fullcname thy
    1.69 +	  | delta (Hol_move (fullname, moved_thmname)) thy = 
    1.70 +	    add_hol4_move fullname moved_thmname thy
    1.71 +	  | delta (Defs (thmname, eq)) thy =
    1.72 +	    snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
    1.73 +	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.74 +	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.75 +	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
    1.76 +	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
    1.77 +	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.78 +	    add_hol4_type_mapping thyname tycname true fulltyname thy
    1.79 +	  | delta (Indexed_theorem (i, th)) thy = 
    1.80 +	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
    1.81 +    in
    1.82 +	rps
    1.83 +    end
    1.84 +
    1.85  fun import_thms thyname int_thms thmnames thy =
    1.86      let
    1.87 -	fun replay_fact (thy,thmname) =
    1.88 +	fun zip names [] = ([], names)
    1.89 +	  | zip [] _ = ([], [])
    1.90 +	  | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
    1.91 +	    if thyname = thyname' andalso thmname = thmname' then
    1.92 +		(if aborted then ([], thmname::names) else 
    1.93 +		 let
    1.94 +		     val _ = writeln ("theorem is in-sync: "^thmname)
    1.95 +		     val (cached,normal) = zip names ys
    1.96 +		 in
    1.97 +		     (entry::cached, normal)
    1.98 +		 end)
    1.99 +	    else
   1.100 +		raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
   1.101 +	  | zip (thmname::_) (DeltaEntry _ :: _) = 
   1.102 + 	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   1.103 +	fun zip' xs (History ys) = 
   1.104 +	    let
   1.105 +		val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   1.106 +		val _ = writeln ("length of history: "^(string_of_int (length ys)))
   1.107 +	    in
   1.108 +		zip xs ys
   1.109 +	    end
   1.110 +	fun replay_fact thmname thy = 
   1.111  	    let
   1.112  		val prf = mk_proof PDisk	
   1.113  		val _ = set_disk_info_of prf thyname thmname
   1.114 @@ -323,7 +398,10 @@
   1.115  	    in
   1.116  		p
   1.117  	    end
   1.118 -	val res_thy = Library.foldl replay_fact (thy,thmnames)
   1.119 +	fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   1.120 +	val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   1.121 +	val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   1.122 +	val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   1.123      in
   1.124  	res_thy
   1.125      end