224 |
224 |
225 fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); |
225 fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); |
226 |
226 |
227 val delete = delete_tagged_list o joinrules; |
227 val delete = delete_tagged_list o joinrules; |
228 |
228 |
|
229 (*Warn if the rule is already present ELSEWHERE in the claset. The addition |
|
230 is still allowed.*) |
|
231 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = |
|
232 if gen_mem eq_thm (th, safeIs) then |
|
233 warning ("rule already in claset as Safe Intr\n" ^ string_of_thm th) |
|
234 else if gen_mem eq_thm (th, safeEs) then |
|
235 warning ("rule already in claset as Safe Elim\n" ^ string_of_thm th) |
|
236 else if gen_mem eq_thm (th, hazIs) then |
|
237 warning ("rule already in claset as unsafe Intr\n" ^ string_of_thm th) |
|
238 else if gen_mem eq_thm (th, hazEs) then |
|
239 warning ("rule already in claset as unsafe Elim\n" ^ string_of_thm th) |
|
240 else (); |
|
241 |
229 (*** Safe rules ***) |
242 (*** Safe rules ***) |
230 |
243 |
231 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
244 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
232 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
245 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
233 addSIs ths = |
246 th) = |
|
247 if gen_mem eq_thm (th, safeIs) then |
|
248 (warning ("ignoring duplicate Safe Intr\n" ^ string_of_thm th); |
|
249 cs) |
|
250 else |
234 let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
251 let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
235 partition (fn rl => nprems_of rl=0) ths |
252 partition (fn rl => nprems_of rl=0) [th] |
236 val nI = length safeIs + length ths |
253 val nI = length safeIs + 1 |
237 and nE = length safeEs |
254 and nE = length safeEs |
238 in CS{safeIs = ths@safeIs, |
255 in warn_dup th cs; |
|
256 CS{safeIs = th::safeIs, |
239 safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
257 safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
240 safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
258 safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
241 safeEs = safeEs, |
259 safeEs = safeEs, |
242 hazIs = hazIs, |
260 hazIs = hazIs, |
243 hazEs = hazEs, |
261 hazEs = hazEs, |
244 wrapper = wrapper, |
262 wrapper = wrapper, |
245 haz_netpair = haz_netpair, |
263 haz_netpair = haz_netpair, |
246 dup_netpair = dup_netpair} |
264 dup_netpair = dup_netpair} |
247 end; |
265 end; |
248 |
266 |
249 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
267 fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
250 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
268 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
251 addSEs ths = |
269 th) = |
|
270 if gen_mem eq_thm (th, safeEs) then |
|
271 (warning ("ignoring duplicate Safe Elim\n" ^ string_of_thm th); |
|
272 cs) |
|
273 else |
252 let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
274 let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
253 partition (fn rl => nprems_of rl=1) ths |
275 partition (fn rl => nprems_of rl=1) [th] |
254 val nI = length safeIs |
276 val nI = length safeIs |
255 and nE = length safeEs + length ths |
277 and nE = length safeEs + 1 |
256 in |
278 in warn_dup th cs; |
257 CS{safeEs = ths@safeEs, |
279 CS{safeEs = th::safeEs, |
258 safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
280 safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
259 safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
281 safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
260 safeIs = safeIs, |
282 safeIs = safeIs, |
261 hazIs = hazIs, |
283 hazIs = hazIs, |
262 hazEs = hazEs, |
284 hazEs = hazEs, |
263 wrapper = wrapper, |
285 wrapper = wrapper, |
264 haz_netpair = haz_netpair, |
286 haz_netpair = haz_netpair, |
265 dup_netpair = dup_netpair} |
287 dup_netpair = dup_netpair} |
266 end; |
288 end; |
267 |
289 |
|
290 fun rev_foldl f (e, l) = foldl f (e, rev l); |
|
291 |
|
292 val op addSIs = rev_foldl addSI; |
|
293 val op addSEs = rev_foldl addSE; |
|
294 |
268 fun cs addSDs ths = cs addSEs (map make_elim ths); |
295 fun cs addSDs ths = cs addSEs (map make_elim ths); |
269 |
296 |
270 |
297 |
271 (*** Hazardous (unsafe) rules ***) |
298 (*** Hazardous (unsafe) rules ***) |
272 |
299 |
273 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
300 fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
274 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
301 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
275 addIs ths = |
302 th)= |
276 let val nI = length hazIs + length ths |
303 if gen_mem eq_thm (th, hazIs) then |
|
304 (warning ("ignoring duplicate unsafe Intr\n" ^ string_of_thm th); |
|
305 cs) |
|
306 else |
|
307 let val nI = length hazIs + 1 |
277 and nE = length hazEs |
308 and nE = length hazEs |
278 in |
309 in warn_dup th cs; |
279 CS{hazIs = ths@hazIs, |
310 CS{hazIs = th::hazIs, |
280 haz_netpair = insert (nI,nE) (ths, []) haz_netpair, |
311 haz_netpair = insert (nI,nE) ([th], []) haz_netpair, |
281 dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair, |
312 dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, |
282 safeIs = safeIs, |
313 safeIs = safeIs, |
283 safeEs = safeEs, |
314 safeEs = safeEs, |
284 hazEs = hazEs, |
315 hazEs = hazEs, |
285 wrapper = wrapper, |
316 wrapper = wrapper, |
286 safe0_netpair = safe0_netpair, |
317 safe0_netpair = safe0_netpair, |
287 safep_netpair = safep_netpair} |
318 safep_netpair = safep_netpair} |
288 end; |
319 end; |
289 |
320 |
290 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
321 fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
291 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
322 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
292 addEs ths = |
323 th) = |
|
324 if gen_mem eq_thm (th, hazEs) then |
|
325 (warning ("ignoring duplicate unsafe Elim\n" ^ string_of_thm th); |
|
326 cs) |
|
327 else |
293 let val nI = length hazIs |
328 let val nI = length hazIs |
294 and nE = length hazEs + length ths |
329 and nE = length hazEs + 1 |
295 in |
330 in warn_dup th cs; |
296 CS{hazEs = ths@hazEs, |
331 CS{hazEs = th::hazEs, |
297 haz_netpair = insert (nI,nE) ([], ths) haz_netpair, |
332 haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, |
298 dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair, |
333 dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, |
299 safeIs = safeIs, |
334 safeIs = safeIs, |
300 safeEs = safeEs, |
335 safeEs = safeEs, |
301 hazIs = hazIs, |
336 hazIs = hazIs, |
302 wrapper = wrapper, |
337 wrapper = wrapper, |
303 safe0_netpair = safe0_netpair, |
338 safe0_netpair = safe0_netpair, |
304 safep_netpair = safep_netpair} |
339 safep_netpair = safep_netpair} |
305 end; |
340 end; |
306 |
341 |
|
342 val op addIs = rev_foldl addI; |
|
343 val op addEs = rev_foldl addE; |
|
344 |
307 fun cs addDs ths = cs addEs (map make_elim ths); |
345 fun cs addDs ths = cs addEs (map make_elim ths); |
308 |
346 |
309 |
347 |
310 (*** Deletion of rules |
348 (*** Deletion of rules |
311 Working out what to delete, requires repeating much of the code used |
349 Working out what to delete, requires repeating much of the code used |
312 to insert. |
350 to insert. |
313 Separate functions delSIs, etc., are not exported; instead delrules |
351 Separate functions delSI, etc., are not exported; instead delrules |
314 searches in all the lists and chooses the relevant delXX function. |
352 searches in all the lists and chooses the relevant delXX function. |
315 ***) |
353 ***) |
316 |
354 |
317 fun delSIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
355 fun delSI (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
318 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
356 safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
319 th) = |
357 th) = |
320 let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] |
358 let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] |
321 in CS{safeIs = gen_rem eq_thm (safeIs,th), |
359 in CS{safeIs = gen_rem eq_thm (safeIs,th), |
322 safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
360 safe0_netpair = delete (safe0_rls, []) safe0_netpair, |