src/HOL/Import/importrecorder.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 21858 05f57309170c
child 32960 69916a850301
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
obua@19064
     1
signature IMPORT_RECORDER =
obua@19064
     2
sig
obua@19064
     3
obua@19064
     4
    datatype deltastate = Consts of (string * typ * mixfix) list
obua@19064
     5
			| Specification of (string * string * bool) list * term
obua@19064
     6
			| Hol_mapping of string * string * string
obua@19064
     7
			| Hol_pending of string * string * term
obua@19064
     8
			| Hol_const_mapping of string * string * string
obua@19064
     9
			| Hol_move of string * string
obua@19064
    10
			| Defs of string * term
obua@19064
    11
			| Hol_theorem of string * string * term
obua@19064
    12
			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
obua@19064
    13
			| Hol_type_mapping of string * string * string
obua@19064
    14
			| Indexed_theorem of int * term
obua@19067
    15
	                | Protect_varname of string * string
obua@19068
    16
			| Dump of string
obua@19064
    17
obua@19064
    18
    datatype history = History of history_entry list
obua@19064
    19
	 and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
obua@19064
    20
obua@19064
    21
    val get_history : unit -> history
obua@19064
    22
    val set_history : history -> unit
obua@19064
    23
    val clear_history : unit -> unit
obua@19064
    24
				      
obua@19064
    25
    val start_replay_proof : string -> string -> unit
obua@19064
    26
    val stop_replay_proof : string -> string -> unit
obua@19064
    27
    val abort_replay_proof : string -> string -> unit
obua@19064
    28
obua@19064
    29
    val add_consts : (string * typ * mixfix) list -> unit
obua@19064
    30
    val add_specification : (string * string * bool) list -> thm -> unit
obua@19064
    31
    val add_hol_mapping : string -> string -> string -> unit
obua@19064
    32
    val add_hol_pending : string -> string -> thm -> unit
obua@19064
    33
    val add_hol_const_mapping : string -> string -> string -> unit
obua@19064
    34
    val add_hol_move : string -> string -> unit
obua@19064
    35
    val add_defs : string -> term -> unit
obua@19064
    36
    val add_hol_theorem : string -> string -> thm -> unit
obua@19064
    37
    val add_typedef :  string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
obua@19064
    38
    val add_hol_type_mapping : string -> string -> string -> unit
obua@19064
    39
    val add_indexed_theorem : int -> thm -> unit
obua@19067
    40
    val protect_varname : string -> string -> unit
obua@19068
    41
    val add_dump : string -> unit
obua@19064
    42
obua@19064
    43
    val set_skip_import_dir : string option -> unit
obua@19064
    44
    val get_skip_import_dir : unit -> string option
obua@19064
    45
obua@19064
    46
    val set_skip_import : bool -> unit
obua@19064
    47
    val get_skip_import : unit -> bool
obua@19064
    48
obua@19064
    49
    val save_history : string -> unit
obua@19064
    50
    val load_history : string -> unit
obua@19064
    51
end
obua@19064
    52
obua@19064
    53
structure ImportRecorder :> IMPORT_RECORDER  =
obua@19064
    54
struct
obua@19064
    55
obua@19064
    56
datatype deltastate = Consts of (string * typ * mixfix) list
obua@19064
    57
		    | Specification of (string * string * bool) list * term
obua@19064
    58
		    | Hol_mapping of string * string * string
obua@19064
    59
		    | Hol_pending of string * string * term
obua@19064
    60
		    | Hol_const_mapping of string * string * string
obua@19064
    61
		    | Hol_move of string * string
obua@19064
    62
		    | Defs of string * term
obua@19064
    63
		    | Hol_theorem of string * string * term
obua@19064
    64
		    | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
obua@19064
    65
		    | Hol_type_mapping of string * string * string
obua@19064
    66
		    | Indexed_theorem of int * term
obua@19067
    67
	            | Protect_varname of string * string
obua@19068
    68
		    | Dump of string
obua@19064
    69
obua@19064
    70
datatype history_entry = StartReplay of string*string  
obua@19064
    71
		       | StopReplay of string*string
obua@19064
    72
		       | AbortReplay of string*string
obua@19064
    73
		       | Delta of deltastate list
obua@19064
    74
wenzelm@32740
    75
val history = Unsynchronized.ref ([]:history_entry list)
wenzelm@32740
    76
val history_dir = Unsynchronized.ref (SOME "")
wenzelm@32740
    77
val skip_imports = Unsynchronized.ref false
obua@19064
    78
obua@19064
    79
fun set_skip_import b = skip_imports := b
obua@19064
    80
fun get_skip_import () = !skip_imports
obua@19064
    81
obua@19064
    82
fun clear_history () = history := []
obua@19064
    83
obua@19064
    84
fun add_delta d = history := (case !history of (Delta ds)::hs => (Delta (d::ds))::hs | hs => (Delta [d])::hs)
obua@19064
    85
fun add_replay r = history := (r :: (!history))
obua@19064
    86
obua@19064
    87
local 
obua@19064
    88
    open XMLConvOutput
obua@19064
    89
    val consts = list (triple string typ mixfix)
obua@19064
    90
    val specification = pair (list (triple string string bool)) term
obua@19064
    91
    val hol_mapping = triple string string string
obua@19064
    92
    val hol_pending = triple string string term
obua@19064
    93
    val hol_const_mapping = triple string string string
obua@19064
    94
    val hol_move = pair string string
obua@19064
    95
    val defs = pair string term
obua@19064
    96
    val hol_theorem = triple string string term
obua@19064
    97
    val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
obua@19064
    98
    val hol_type_mapping = triple string string string
obua@19064
    99
    val indexed_theorem = pair int term
obua@19064
   100
    val entry = pair string string
obua@19064
   101
obua@19064
   102
    fun delta (Consts args) = wrap "consts" consts args
obua@19064
   103
      | delta (Specification args) = wrap "specification" specification args
obua@19064
   104
      | delta (Hol_mapping args) = wrap "hol_mapping" hol_mapping args
obua@19064
   105
      | delta (Hol_pending args) = wrap "hol_pending" hol_pending args
obua@19064
   106
      | delta (Hol_const_mapping args) = wrap "hol_const_mapping" hol_const_mapping args
obua@19064
   107
      | delta (Hol_move args) = wrap "hol_move" hol_move args
obua@19064
   108
      | delta (Defs args) = wrap "defs" defs args
obua@19064
   109
      | delta (Hol_theorem args) = wrap "hol_theorem" hol_theorem args
obua@19064
   110
      | delta (Typedef args) = wrap "typedef" typedef args
obua@19064
   111
      | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
obua@19064
   112
      | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
obua@19067
   113
      | delta (Protect_varname args) = wrap "protect_varname" entry args
obua@19068
   114
      | delta (Dump args) = wrap "dump" string args
obua@19064
   115
obua@19064
   116
    fun history_entry (StartReplay args) = wrap "startreplay" entry args
obua@19064
   117
      | history_entry (StopReplay args) = wrap "stopreplay" entry args
obua@19064
   118
      | history_entry (AbortReplay args) = wrap "abortreplay" entry args
obua@19064
   119
      | history_entry (Delta args) = wrap "delta" (list delta) args
obua@19064
   120
in
obua@19064
   121
obua@19064
   122
val xml_of_history = list history_entry
obua@19064
   123
obua@19064
   124
end
obua@19064
   125
obua@19064
   126
local 
obua@19064
   127
    open XMLConvInput
obua@19064
   128
    val consts = list (triple string typ mixfix)
obua@19064
   129
    val specification = pair (list (triple string string bool)) term
obua@19064
   130
    val hol_mapping = triple string string string
obua@19064
   131
    val hol_pending = triple string string term
obua@19064
   132
    val hol_const_mapping = triple string string string
obua@19064
   133
    val hol_move = pair string string
obua@19064
   134
    val defs = pair string term
obua@19064
   135
    val hol_theorem = triple string string term
obua@19064
   136
    val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
obua@19064
   137
    val hol_type_mapping = triple string string string
obua@19064
   138
    val indexed_theorem = pair int term
obua@19064
   139
    val entry = pair string string
obua@19064
   140
obua@19064
   141
    fun delta "consts" = unwrap Consts consts
obua@19064
   142
      | delta "specification" = unwrap Specification specification 
obua@19064
   143
      | delta "hol_mapping" = unwrap Hol_mapping hol_mapping 
obua@19064
   144
      | delta "hol_pending" = unwrap Hol_pending hol_pending
obua@19064
   145
      | delta "hol_const_mapping" = unwrap Hol_const_mapping hol_const_mapping
obua@19064
   146
      | delta "hol_move" = unwrap Hol_move hol_move
obua@19064
   147
      | delta "defs" = unwrap Defs defs
obua@19064
   148
      | delta "hol_theorem" = unwrap Hol_theorem hol_theorem
obua@19064
   149
      | delta "typedef" = unwrap Typedef typedef
obua@19064
   150
      | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
obua@19064
   151
      | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
obua@19067
   152
      | delta "protect_varname" = unwrap Protect_varname entry
obua@19068
   153
      | delta "dump" = unwrap Dump string
obua@19064
   154
      | delta _ = raise ParseException "delta"
obua@19064
   155
obua@19064
   156
    val delta = fn e => delta (name_of_wrap e) e
obua@19064
   157
obua@19064
   158
    fun history_entry "startreplay" = unwrap StartReplay entry 
obua@19064
   159
      | history_entry "stopreplay" = unwrap StopReplay entry
obua@19064
   160
      | history_entry "abortreplay" = unwrap AbortReplay entry
obua@19064
   161
      | history_entry "delta" = unwrap Delta (list delta)
obua@19064
   162
      | history_entry _ = raise ParseException "history_entry"
obua@19064
   163
obua@19064
   164
    val history_entry = fn e => history_entry (name_of_wrap e) e
obua@19064
   165
in
obua@19064
   166
obua@19064
   167
val history_of_xml = list history_entry
obua@19064
   168
obua@19064
   169
end
obua@19064
   170
obua@19064
   171
fun start_replay_proof thyname thmname = add_replay (StartReplay (thyname, thmname))
obua@19064
   172
fun stop_replay_proof thyname thmname = add_replay (StopReplay (thyname, thmname))
obua@19064
   173
fun abort_replay_proof thyname thmname = add_replay (AbortReplay (thyname, thmname))
obua@19064
   174
fun add_hol_theorem thyname thmname thm = add_delta (Hol_theorem (thyname, thmname, prop_of thm))
obua@19064
   175
fun add_hol_mapping thyname thmname isaname = add_delta (Hol_mapping (thyname, thmname, isaname))
obua@19064
   176
fun add_consts consts = add_delta (Consts consts)
obua@19064
   177
fun add_typedef thmname_opt typ c absrep_opt th = add_delta (Typedef (thmname_opt, typ, c, absrep_opt, prop_of th))
obua@19064
   178
fun add_defs thmname eq = add_delta (Defs (thmname, eq)) 
obua@19064
   179
fun add_hol_const_mapping thyname constname fullcname = add_delta (Hol_const_mapping (thyname, constname, fullcname))
obua@19064
   180
fun add_hol_move fullname moved_thmname = add_delta (Hol_move (fullname, moved_thmname))
obua@19064
   181
fun add_hol_type_mapping thyname tycname fulltyname = add_delta (Hol_type_mapping (thyname, tycname, fulltyname))
obua@19064
   182
fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
obua@19064
   183
fun add_specification names th = add_delta (Specification (names, prop_of th)) 
obua@19064
   184
fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
obua@19067
   185
fun protect_varname s t = add_delta (Protect_varname (s,t))
obua@19068
   186
fun add_dump s = add_delta (Dump s)
obua@19064
   187
			    
obua@19064
   188
fun set_skip_import_dir dir = (history_dir := dir)
obua@19064
   189
fun get_skip_import_dir () = !history_dir
obua@19064
   190
wenzelm@21858
   191
fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
obua@19064
   192
obua@19064
   193
fun save_history thyname = 
obua@19064
   194
    if get_skip_import () then
obua@19064
   195
	XMLConv.write_to_file xml_of_history (get_filename thyname) (!history)
obua@19064
   196
    else 
obua@19064
   197
	()
obua@19064
   198
obua@19064
   199
fun load_history thyname = 
obua@19064
   200
    if get_skip_import () then
obua@19064
   201
	let 
obua@19064
   202
	    val filename = get_filename thyname
obua@19064
   203
	    val _ = writeln "load_history / before"
obua@19064
   204
	    val _ = 
wenzelm@21858
   205
		if File.exists (Path.explode filename) then					
obua@19064
   206
		    (history := XMLConv.read_from_file history_of_xml (get_filename thyname)) 
obua@19064
   207
		else
obua@19064
   208
		    clear_history ()
obua@19064
   209
	    val _ = writeln "load_history / after"
obua@19064
   210
	in
obua@19064
   211
	    ()
obua@19064
   212
	end
obua@19064
   213
    else
obua@19064
   214
	()
obua@19064
   215
    
obua@19064
   216
 
obua@19064
   217
datatype history = History of history_entry list
obua@19064
   218
     and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
obua@19064
   219
obua@19064
   220
exception CONV 
obua@19064
   221
obua@19064
   222
fun conv_histories ((StartReplay (thyname, thmname))::rest) = 
obua@19064
   223
    let
obua@19064
   224
	val (hs, rest) = conv_histories rest
obua@19064
   225
	fun continue thyname' thmname' aborted rest = 
obua@19064
   226
	    if thyname = thyname' andalso thmname = thmname' then
obua@19064
   227
		let
obua@19064
   228
		    val (hs', rest) = conv_histories rest
obua@19064
   229
		in
obua@19064
   230
		    ((ThmEntry (thyname, thmname, aborted, History hs))::hs', rest)
obua@19064
   231
		end
obua@19064
   232
	    else
obua@19064
   233
		raise CONV 
obua@19064
   234
    in
obua@19064
   235
	case rest of 
obua@19064
   236
	    (StopReplay (thyname',thmname'))::rest =>
obua@19064
   237
	    continue thyname' thmname' false rest
obua@19064
   238
	  | (AbortReplay (thyname',thmname'))::rest =>
obua@19064
   239
	    continue thyname' thmname' true rest
obua@19064
   240
	  | [] => (hs, [])
obua@19064
   241
	  | _ => raise CONV
obua@19064
   242
    end
obua@19064
   243
  | conv_histories ((Delta ds)::rest) = (conv_histories rest) |>> (fn hs => (DeltaEntry (rev ds))::hs)  
obua@19064
   244
  | conv_histories rest = ([], rest)
obua@19064
   245
obua@19064
   246
fun conv es = 
obua@19064
   247
    let
obua@19064
   248
	val (h, rest) = conv_histories (rev es)
obua@19064
   249
    in
obua@19064
   250
	case rest of
obua@19064
   251
	    [] => h
obua@19064
   252
	  | _ => raise CONV
obua@19064
   253
    end 
obua@19064
   254
obua@19064
   255
fun get_history () = History (conv (!history))
obua@19064
   256
obua@19064
   257
fun reconv (History hs) rs = fold reconv_entry hs rs
obua@19064
   258
and reconv_entry (ThmEntry (thyname, thmname, aborted, h)) rs =
obua@19064
   259
    ((if aborted then AbortReplay else StopReplay) (thyname, thmname)) :: (reconv h ((StartReplay (thyname, thmname))::rs))
obua@19064
   260
  | reconv_entry (DeltaEntry ds) rs = (Delta (rev ds))::rs
obua@19064
   261
    
obua@19064
   262
fun set_history h = history := reconv h []
obua@19064
   263
obua@19064
   264
obua@19064
   265
end