equal
deleted
inserted
replaced
237 exception PCompute of string |
237 exception PCompute of string |
238 |
238 |
239 datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list |
239 datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list |
240 datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list |
240 datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list |
241 |
241 |
242 datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref |
242 datatype pcomputer = |
|
243 PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref * |
|
244 pattern list Unsynchronized.ref |
243 |
245 |
244 (*fun collect_consts (Var x) = [] |
246 (*fun collect_consts (Var x) = [] |
245 | collect_consts (Bound _) = [] |
247 | collect_consts (Bound _) = [] |
246 | collect_consts (a $ b) = (collect_consts a)@(collect_consts b) |
248 | collect_consts (a $ b) = (collect_consts a)@(collect_consts b) |
247 | collect_consts (Abs (_, _, body)) = collect_consts body |
249 | collect_consts (Abs (_, _, body)) = collect_consts body |
322 fun conv_subst thy (subst : Type.tyenv) = |
324 fun conv_subst thy (subst : Type.tyenv) = |
323 map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst) |
325 map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst) |
324 |
326 |
325 fun add_monos thy monocs pats ths = |
327 fun add_monos thy monocs pats ths = |
326 let |
328 let |
327 val changed = ref false |
329 val changed = Unsynchronized.ref false |
328 fun add monocs (th as (MonoThm _)) = ([], th) |
330 fun add monocs (th as (MonoThm _)) = ([], th) |
329 | add monocs (PolyThm (th, instances, instanceths)) = |
331 | add monocs (PolyThm (th, instances, instanceths)) = |
330 let |
332 let |
331 val (newsubsts, instances) = Linker.add_instances thy instances monocs |
333 val (newsubsts, instances) = Linker.add_instances thy instances monocs |
332 val _ = if not (null newsubsts) then changed := true else () |
334 val _ = if not (null newsubsts) then changed := true else () |
384 |
386 |
385 structure CThmtab = Table(type key = cthm val ord = cthm_ord) |
387 structure CThmtab = Table(type key = cthm val ord = cthm_ord) |
386 |
388 |
387 fun remove_duplicates ths = |
389 fun remove_duplicates ths = |
388 let |
390 let |
389 val counter = ref 0 |
391 val counter = Unsynchronized.ref 0 |
390 val tab = ref (CThmtab.empty : unit CThmtab.table) |
392 val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table) |
391 val thstab = ref (Inttab.empty : thm Inttab.table) |
393 val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table) |
392 fun update th = |
394 fun update th = |
393 let |
395 let |
394 val key = thm2cthm th |
396 val key = thm2cthm th |
395 in |
397 in |
396 case CThmtab.lookup (!tab) key of |
398 case CThmtab.lookup (!tab) key of |
413 ths (cs, []) |
415 ths (cs, []) |
414 val pats = map create_pattern pats |
416 val pats = map create_pattern pats |
415 val (_, (pats, ths)) = add_monos thy monocs pats ths |
417 val (_, (pats, ths)) = add_monos thy monocs pats ths |
416 val computer = create_computer machine thy pats ths |
418 val computer = create_computer machine thy pats ths |
417 in |
419 in |
418 PComputer (Theory.check_thy thy, computer, ref ths, ref pats) |
420 PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) |
419 end |
421 end |
420 |
422 |
421 fun make machine thy ths cs = make_with_cache machine thy [] ths cs |
423 fun make machine thy ths cs = make_with_cache machine thy [] ths cs |
422 |
424 |
423 fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = |
425 fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = |