cache improvements
authorobua
Thu Feb 16 14:59:57 2006 +0100 (2006-02-16)
changeset 1906804b302f2902d
parent 19067 c0321d7d6b3d
child 19069 a4b956f8b233
cache improvements
src/HOL/Import/importrecorder.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
     1.1 --- a/src/HOL/Import/importrecorder.ML	Thu Feb 16 04:17:19 2006 +0100
     1.2 +++ b/src/HOL/Import/importrecorder.ML	Thu Feb 16 14:59:57 2006 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4  			| Hol_type_mapping of string * string * string
     1.5  			| Indexed_theorem of int * term
     1.6  	                | Protect_varname of string * string
     1.7 +			| Dump of string
     1.8  
     1.9      datatype history = History of history_entry list
    1.10  	 and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
    1.11 @@ -37,6 +38,7 @@
    1.12      val add_hol_type_mapping : string -> string -> string -> unit
    1.13      val add_indexed_theorem : int -> thm -> unit
    1.14      val protect_varname : string -> string -> unit
    1.15 +    val add_dump : string -> unit
    1.16  
    1.17      val set_skip_import_dir : string option -> unit
    1.18      val get_skip_import_dir : unit -> string option
    1.19 @@ -63,6 +65,7 @@
    1.20  		    | Hol_type_mapping of string * string * string
    1.21  		    | Indexed_theorem of int * term
    1.22  	            | Protect_varname of string * string
    1.23 +		    | Dump of string
    1.24  
    1.25  datatype history_entry = StartReplay of string*string  
    1.26  		       | StopReplay of string*string
    1.27 @@ -108,6 +111,7 @@
    1.28        | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
    1.29        | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
    1.30        | delta (Protect_varname args) = wrap "protect_varname" entry args
    1.31 +      | delta (Dump args) = wrap "dump" string args
    1.32  
    1.33      fun history_entry (StartReplay args) = wrap "startreplay" entry args
    1.34        | history_entry (StopReplay args) = wrap "stopreplay" entry args
    1.35 @@ -146,6 +150,7 @@
    1.36        | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
    1.37        | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
    1.38        | delta "protect_varname" = unwrap Protect_varname entry
    1.39 +      | delta "dump" = unwrap Dump string
    1.40        | delta _ = raise ParseException "delta"
    1.41  
    1.42      val delta = fn e => delta (name_of_wrap e) e
    1.43 @@ -178,6 +183,7 @@
    1.44  fun add_specification names th = add_delta (Specification (names, prop_of th)) 
    1.45  fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
    1.46  fun protect_varname s t = add_delta (Protect_varname (s,t))
    1.47 +fun add_dump s = add_delta (Dump s)
    1.48  			    
    1.49  fun set_skip_import_dir dir = (history_dir := dir)
    1.50  fun get_skip_import_dir () = !history_dir
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 04:17:19 2006 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 14:59:57 2006 +0100
     2.3 @@ -114,6 +114,7 @@
     2.4      val prin : term -> unit 
     2.5      val protect_factname : string -> string 
     2.6      val replay_protect_varname : string -> string -> unit
     2.7 +    val replay_add_dump : string -> theory -> theory
     2.8  end
     2.9  
    2.10  structure ProofKernel :> ProofKernel =
    2.11 @@ -128,6 +129,9 @@
    2.12  
    2.13  fun to_hol_thm th = HOLThm ([], th)
    2.14  
    2.15 +val replay_add_dump = add_dump
    2.16 +fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
    2.17 +
    2.18  datatype proof_info
    2.19    = Info of {disk_info: (string * string) option ref}
    2.20  	    
     3.1 --- a/src/HOL/Import/replay.ML	Thu Feb 16 04:17:19 2006 +0100
     3.2 +++ b/src/HOL/Import/replay.ML	Thu Feb 16 14:59:57 2006 +0100
     3.3 @@ -328,18 +328,6 @@
     3.4  	  | rps (t::ts) thy = rps ts (rp t thy)
     3.5  	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
     3.6  	  | rp (DeltaEntry ds) thy = fold delta ds thy
     3.7 -(*    datatype deltastate = Consts of (string * typ * mixfix) list
     3.8 -			| Specification of (string * string * bool) list * term
     3.9 -			| Hol_mapping of string * string * string
    3.10 -			| Hol_pending of string * string * term
    3.11 -			| Hol_const_mapping of string * string * string
    3.12 -			| Hol_move of string * string
    3.13 -			| Defs of string * term
    3.14 -			| Hol_theorem of string * string * term
    3.15 -			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
    3.16 -			| Hol_type_mapping of string * string * string
    3.17 -			| Indexed_theorem of int * term
    3.18 -*)
    3.19  	and delta (Specification (names, th)) thy = 
    3.20  	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
    3.21  	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
    3.22 @@ -361,8 +349,8 @@
    3.23  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    3.24  	  | delta (Indexed_theorem (i, th)) thy = 
    3.25  	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
    3.26 -          | delta (Protect_varname (s,t)) thy =
    3.27 -	    (P.replay_protect_varname s t; thy)
    3.28 +          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
    3.29 +	  | delta (Dump s) thy = P.replay_add_dump s thy
    3.30      in
    3.31  	rps
    3.32      end