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