591 (variant (map #1 vars @ names) a, T) :: vars |
591 (variant (map #1 vars @ names) a, T) :: vars |
592 in foldl rename_aT ([],vars) end; |
592 in foldl rename_aT ([],vars) end; |
593 |
593 |
594 fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); |
594 fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); |
595 |
595 |
|
596 |
|
597 |
|
598 (*** Compression of terms and types by sharing common subtrees. Currently |
|
599 naive but could be made to run faster. Saves 50-75% on storage |
|
600 requirements. As it is slow, should be called only for axioms, stored |
|
601 theorems, etc. ***) |
|
602 |
|
603 (** Sharing of types **) |
|
604 |
|
605 (*Allow non-"fun" types??*) |
|
606 fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match |
|
607 | atomic_tag (TFree (a,_)) = a |
|
608 | atomic_tag (TVar ((a,_),_)) = a; |
|
609 |
|
610 fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T |
|
611 | type_tag T = atomic_tag T; |
|
612 |
|
613 val memo_types = ref (Symtab.null : typ list Symtab.table); |
|
614 |
|
615 fun find_type (T, []: typ list) = None |
|
616 | find_type (T, T'::Ts) = |
|
617 if T=T' then Some T' |
|
618 else find_type (T, Ts); |
|
619 |
|
620 fun compress_type T = |
|
621 let val tag = type_tag T |
|
622 val tylist = the (Symtab.lookup (!memo_types, tag)) |
|
623 handle _ => [] |
|
624 in |
|
625 case find_type (T,tylist) of |
|
626 Some T' => T' |
|
627 | None => |
|
628 let val T' = |
|
629 case T of |
|
630 Type (a,Ts) => Type (a, map compress_type Ts) |
|
631 | _ => T |
|
632 in memo_types := Symtab.update ((tag, T'::tylist), !memo_types); |
|
633 T |
|
634 end |
|
635 end |
|
636 handle Match => |
|
637 let val Type (a,Ts) = T |
|
638 in Type (a, map compress_type Ts) end; |
|
639 |
|
640 (** Sharing of atomic terms **) |
|
641 |
|
642 val memo_terms = ref (Symtab.null : term list Symtab.table); |
|
643 |
|
644 fun find_term (t, []: term list) = None |
|
645 | find_term (t, t'::ts) = |
|
646 if t=t' then Some t' |
|
647 else find_term (t, ts); |
|
648 |
|
649 fun const_tag (Const (a,_)) = a |
|
650 | const_tag (Free (a,_)) = a |
|
651 | const_tag (Var ((a,i),_)) = a |
|
652 | const_tag (t as Bound _) = ".B."; |
|
653 |
|
654 fun share_term (t $ u) = share_term t $ share_term u |
|
655 | share_term (Abs (a,T,u)) = Abs (a, T, share_term u) |
|
656 | share_term t = |
|
657 let val tag = const_tag t |
|
658 val ts = the (Symtab.lookup (!memo_terms, tag)) |
|
659 handle _ => [] |
|
660 in |
|
661 case find_term (t,ts) of |
|
662 Some t' => t' |
|
663 | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms); |
|
664 t) |
|
665 end; |
|
666 |
|
667 val compress_term = share_term o map_term_types compress_type; |
|
668 |
596 end; |
669 end; |
597 |
670 |
598 open Term; |
671 open Term; |