variable counter is now also cached
authorobua
Thu Feb 16 04:17:19 2006 +0100 (2006-02-16)
changeset 19067c0321d7d6b3d
parent 19066 df24f2564aaa
child 19068 04b302f2902d
variable counter is now also cached
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 03:23:57 2006 +0100
     1.2 +++ b/src/HOL/Import/importrecorder.ML	Thu Feb 16 04:17:19 2006 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4  			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
     1.5  			| Hol_type_mapping of string * string * string
     1.6  			| Indexed_theorem of int * term
     1.7 +	                | Protect_varname of string * 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 @@ -35,6 +36,7 @@
    1.12      val add_typedef :  string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
    1.13      val add_hol_type_mapping : string -> string -> string -> unit
    1.14      val add_indexed_theorem : int -> thm -> unit
    1.15 +    val protect_varname : string -> 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 @@ -60,6 +62,7 @@
    1.20  		    | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
    1.21  		    | Hol_type_mapping of string * string * string
    1.22  		    | Indexed_theorem of int * term
    1.23 +	            | Protect_varname of string * string
    1.24  
    1.25  datatype history_entry = StartReplay of string*string  
    1.26  		       | StopReplay of string*string
    1.27 @@ -104,6 +107,7 @@
    1.28        | delta (Typedef args) = wrap "typedef" typedef args
    1.29        | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
    1.30        | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
    1.31 +      | delta (Protect_varname args) = wrap "protect_varname" entry 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 @@ -141,6 +145,7 @@
    1.36        | delta "typedef" = unwrap Typedef typedef
    1.37        | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
    1.38        | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
    1.39 +      | delta "protect_varname" = unwrap Protect_varname entry
    1.40        | delta _ = raise ParseException "delta"
    1.41  
    1.42      val delta = fn e => delta (name_of_wrap e) e
    1.43 @@ -172,6 +177,7 @@
    1.44  fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
    1.45  fun add_specification names th = add_delta (Specification (names, prop_of th)) 
    1.46  fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
    1.47 +fun protect_varname s t = add_delta (Protect_varname (s,t))
    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 03:23:57 2006 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 04:17:19 2006 +0100
     2.3 @@ -112,7 +112,8 @@
     2.4      val new_axiom : string -> term -> theory -> theory * thm
     2.5  
     2.6      val prin : term -> unit 
     2.7 -    val protect_factname : string -> string
     2.8 +    val protect_factname : string -> string 
     2.9 +    val replay_protect_varname : string -> string -> unit
    2.10  end
    2.11  
    2.12  structure ProofKernel :> ProofKernel =
    2.13 @@ -480,11 +481,26 @@
    2.14        let
    2.15  	  val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
    2.16  	  val t = "u_"^(IntInf.toString (!invented_isavar))
    2.17 +	  val _ = ImportRecorder.protect_varname s t
    2.18            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    2.19        in
    2.20  	  t
    2.21        end
    2.22  
    2.23 +exception REPLAY_PROTECT_VARNAME of string*string*string
    2.24 +
    2.25 +fun replay_protect_varname s t = 
    2.26 +	case Symtab.lookup (!protected_varnames) s of
    2.27 +	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
    2.28 +	| NONE => 	
    2.29 +          let
    2.30 +	      val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
    2.31 +	      val t = "u_"^(IntInf.toString (!invented_isavar))
    2.32 +              val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    2.33 +          in
    2.34 +	      ()
    2.35 +          end	       	
    2.36 +	 
    2.37  fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
    2.38  
    2.39  fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
     3.1 --- a/src/HOL/Import/replay.ML	Thu Feb 16 03:23:57 2006 +0100
     3.2 +++ b/src/HOL/Import/replay.ML	Thu Feb 16 04:17:19 2006 +0100
     3.3 @@ -361,6 +361,8 @@
     3.4  	    add_hol4_type_mapping thyname tycname true fulltyname thy
     3.5  	  | delta (Indexed_theorem (i, th)) thy = 
     3.6  	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
     3.7 +          | delta (Protect_varname (s,t)) thy =
     3.8 +	    (P.replay_protect_varname s t; thy)
     3.9      in
    3.10  	rps
    3.11      end