1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
structure saveThmsLib =
struct
type simpset = simpLib.simpset;
open HolKernel boolLib markerLib;
val op++ = simpLib.++;
val op-* = simpLib.-*;
val ERR = mk_HOL_ERR "saveThmsLib";
fun add_simpls tyinfo ss =
(ss ++ simpLib.tyi_to_ssdata tyinfo) handle HOL_ERR _ => ss
(* TODO: what is this? *)
fun tyinfol() = TypeBasePure.listItems (TypeBase.theTypeBase())
datatype stc_update = ADD_SSFRAG of simpLib.ssfrag | REMOVE_RWT of string
type stc_state = simpset * bool * stc_update list
(* theorems, initialised-flag, update list (most recent first) *)
val initial_simpset = simpLib.empty_ss
fun ssf1 nth = simpLib.empty_ssfrag |> simpLib.add_named_rwt nth
val state0 : stc_state = (initial_simpset, false, [])
fun apply_delta d ((sset,initp,upds):stc_state) : stc_state =
case d of
ThmSetData.ADD nth =>
(sset ++ ssf1 nth, true, [])
| ThmSetData.REMOVE s => (sset -* [s], true, [])
fun apply_stc_update (ADD_SSFRAG ssf, ss) = ss ++ ssf
| apply_stc_update (REMOVE_RWT n, ss) = ss -* [n]
(* A stateful theorems collection *)
datatype stc = STC_CON of {
name : string,
thy_ssfrag : string -> simpLib.ssfrag,
thy_simpset : string -> simpset option,
get_ss : unit -> simpset,
export_thms : string list -> unit
}
(* Create a stateful theorems collection *)
fun create_stateful_theorem_set (stc_name : string) =
let
(* val stc_name = "testStc" *)
fun init_state (st as (sset,initp,upds)) =
if initp then st
else
let fun init() =
(List.foldl apply_stc_update sset (List.rev upds)
|> rev_itlist add_simpls (tyinfol()),
true, [])
in
HOL_PROGRESS_MESG ("Initialising STC simpset: " ^ stc_name ^ " ... ", "done") init ()
end
fun opt_partition f g ls =
let
fun recurse As Bs ls =
case ls of
[] => (List.rev As, List.rev Bs)
| h::t => (case f h of
SOME a => recurse (a::As) Bs t
| NONE => (case g h of
SOME b => recurse As (b::Bs) t
| NONE => recurse As Bs t))
in
recurse [] [] ls
end
(* stale-ness is important for derived values. Derived values will get
re-calculated if their flag is true when the value is requested.
*)
val stale_flags = Sref.new ([] : bool Sref.t list)
fun notify () =
List.app (fn br => Sref.update br (K true)) (Sref.value stale_flags)
fun apply_to_global d (st as (sset,initp,upds):stc_state) : stc_state =
if not initp then
case d of
ThmSetData.ADD nth =>
let
open simpLib
val upds' =
case upds of
ADD_SSFRAG ssf :: rest =>
ADD_SSFRAG (add_named_rwt nth ssf) :: rest
| _ => ADD_SSFRAG (ssf1 nth) :: upds
in
(sset, initp, upds')
end
| ThmSetData.REMOVE s => (sset, initp, REMOVE_RWT s :: upds)
else
apply_delta d st before notify()
fun finaliser {thyname} deltas (sset,initp,upds) =
let
fun toNamedAdd (ThmSetData.ADD p) = SOME p | toNamedAdd _ = NONE
fun toRM (ThmSetData.REMOVE s) = SOME s | toRM _ = NONE
val (adds,rms) = opt_partition toNamedAdd toRM deltas
val ssfrag = simpLib.named_rewrites_with_names thyname (List.rev adds)
(* List.rev here preserves old behaviour wrt to the way theorems were
added to the global simpset; it will only make a difference when
overall rewrite system is not confluent *)
val new_upds = ADD_SSFRAG ssfrag :: map REMOVE_RWT rms
in
if initp then
(List.foldl apply_stc_update sset new_upds, true, []) before notify()
else (sset, false, List.revAppend(new_upds, upds))
end
val adresult as {DB,get_global_value,record_delta,update_global_value,...} =
ThmSetData.export_with_ancestry {
delta_ops = {
apply_delta = apply_delta,
apply_to_global = apply_to_global,
thy_finaliser = SOME finaliser,
initial_value = state0, uptodate_delta = K true
},
settype = stc_name
}
val get_deltas = #get_deltas adresult
(*
(* TODO: what is this? *)
fun update_fn tyi =
augment_stc_ss ([simpLib.tyi_to_ssdata tyi] handle HOL_ERR _ => [])
val () = TypeBase.register_update_fn (fn tyi => (update_fn tyi; tyi))
*)
fun get_ss () =
(update_global_value init_state;
#1 (get_global_value()))
fun export_thms slist =
let val ds = map ThmSetData.mk_add slist
in
List.app record_delta ds;
update_global_value (rev_itlist apply_to_global ds)
end
(* assume that there aren't any removes for things added in this theory;
it's not rational to do that; one should add it locally only, or not
add it at all
*)
fun mkfrag_from thy setdeltas =
let fun recurse ADDs [] = ADDs
| recurse ADDs (ThmSetData.ADD p :: rest) = recurse (p::ADDs) rest
| recurse ADDs (_ :: rest) = recurse ADDs rest
val ADDs = recurse [] setdeltas
(* order of addition is flipped; see above for why this is
"reasonable" *)
in
simpLib.named_rewrites_with_names thy ADDs
end
fun thy_ssfrag s = get_deltas {thyname=s} |> mkfrag_from s
fun thy_simpset s = Option.map (#1 o init_state) (DB {thyname=s})
in
STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset,
get_ss = get_ss, export_thms = export_thms }
end
fun rewrite_thms_of_simpset (ss : simpset) : thm list =
List.concat (map simpLib.frag_rewrites (simpLib.ssfrags_of ss))
(*
(* Create a stateful theorems collection *)
val STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset, get_ss = get_ss, export_thms = export_thms } =
create_stateful_theorem_set "testStc1"
Theorem th1:
T /\ (T /\ T)
Proof
fs []
QED
export_thms ["th1"]
fun rewrite_thms_of_simpset (ss : simpset) : thm list =
List.concat (map simpLib.frag_rewrites (simpLib.ssfrags_of ss))
rewrite_thms_of_simpset (get_ss ())
*)
val STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset, get_ss = get_ss, export_thms = export_thms } =
create_stateful_theorem_set "testStc1"
end
|
