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