File ‹rewrite.ML›
val simp_ord = Term_Ord.term_ord o (apply2 Util.rhs_of)
fun eq_info ((id, th), (id', th')) =
(id = id' andalso Util.rhs_of th aconv Util.rhs_of th')
fun print_info ctxt (id, th) = "(" ^ (BoxID.string_of_box_id id) ^ ", " ^
(th |> Util.rhs_of |> Syntax.string_of_term ctxt) ^ ")"
fun print_infos ctxt lst = commas (map (print_info ctxt) lst)
fun print_info' ctxt (id, ths) =
"(" ^ (BoxID.string_of_box_id id) ^ ", " ^
(ths |> map Util.rhs_of |> Util.string_of_terms ctxt) ^ ")"
fun print_infos' ctxt lst = cat_lines (map (print_info' ctxt) lst)
type rewrite_table = {
terms: (box_id list * cterm) Termtab.table,
equiv: ((box_id * thm) list) Termtab.table,
all_equiv: ((box_id * thm) list) Termtab.table,
contain: (cterm list) Termtab.table,
simp: ((box_id * thm) list) Termtab.table,
subsimp: ((box_id * thm) list) Termtab.table,
reps: ((box_id * thm) list) Termtab.table
}
signature REWRITE_TABLE =
sig
val clean_resolved: box_id -> Proof.context -> Proof.context
val clear_incr: Proof.context -> Proof.context
val add_contain: cterm -> term -> Proof.context -> Proof.context
val immediate_contains: Proof.context -> term -> cterm list
val in_table_raw_ids: Proof.context -> term -> box_id list
val in_table_raw_for_id: Proof.context -> box_id * term -> bool
val in_table_raw: Proof.context -> term -> bool
val add_term_raw: box_id * cterm -> Proof.context -> Proof.context
val get_all_terms: Proof.context -> cterm list
val get_all_id_terms: Proof.context -> (box_id * cterm) list
val add_equiv: box_id * thm -> Proof.context -> Proof.context
val equiv_neighs: Proof.context -> term -> (box_id * thm) list
val get_all_equiv: Proof.context -> term -> (box_id * thm) list
val update_simp: box_id * thm -> Proof.context -> Proof.context
val get_rewrite_info: Proof.context -> cterm -> (box_id * thm) list
val get_rewrite: box_id -> Proof.context -> cterm -> thm
val get_subterm_rewrite_info: Proof.context -> cterm -> (box_id * thm) list
val remove_rep: box_id * thm -> Proof.context -> Proof.context
val update_subsimp: box_id * thm -> Proof.context -> Proof.context
val get_head_rep_info: Proof.context -> term -> (box_id * thm) list
val get_head_rep: box_id -> Proof.context -> term -> thm option
val get_head_rep_with_id_th:
Proof.context -> box_id * thm -> (box_id * thm) list
val get_cached_subterm_rewrite_info:
Proof.context -> term -> (box_id * thm) list
val get_cached_subterm_rewrite: box_id -> Proof.context -> cterm -> thm
val head_simplify: box_id -> Proof.context -> cterm -> thm
val simplify: box_id -> Proof.context -> cterm -> thm
val subterm_simplify: box_id -> Proof.context -> cterm -> thm
val simp_val: box_id -> Proof.context -> cterm -> cterm
val simp_val_t: box_id -> Proof.context -> term -> term
val simplify_info: Proof.context -> cterm -> (box_id * thm) list
val subterm_simplify_info: Proof.context -> cterm -> (box_id * thm) list
val is_equiv: box_id -> Proof.context -> cterm * cterm -> bool
val is_equiv_t: box_id -> Proof.context -> term * term -> bool
val get_head_equiv: Proof.context -> cterm -> (box_id * thm) list
val get_head_equiv_with_t:
Proof.context -> box_id * cterm -> term -> (box_id * thm) list
val process_update_simp: (box_id * thm) list -> Proof.context -> Proof.context
val equiv_info:
Proof.context -> box_id -> cterm * cterm -> (box_id * thm) list
val equiv_info_t:
Proof.context -> box_id -> term * term -> (box_id * thm) list
val subequiv_info:
Proof.context -> box_id -> cterm * cterm -> (box_id * thm) list
val add_rewrite_raw: box_id -> thm -> Proof.context -> Proof.context
val get_reachable_terms: bool -> Proof.context -> term list -> term list
val complete_table: Proof.context -> (box_id * thm) list * Proof.context
val add_term:
box_id * cterm -> Proof.context -> (box_id * thm) list * Proof.context
val add_term_list:
(box_id * cterm) list -> Proof.context -> (box_id * thm) list * Proof.context
val add_rewrite:
box_id * thm -> Proof.context -> (box_id * thm) list * Proof.context
val get_new_terms: Proof.context * Proof.context -> (box_id * cterm) list
end;
functor RewriteTable(UtilLogic : UTIL_LOGIC) : REWRITE_TABLE =
struct
structure Data = Proof_Data
(
type T = rewrite_table
fun init _ = {terms = Termtab.empty, equiv = Termtab.empty,
all_equiv = Termtab.empty, contain = Termtab.empty,
simp = Termtab.empty, subsimp = Termtab.empty,
reps = Termtab.empty}
)
fun clean_resolved id ctxt =
let
val {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
Data.get ctxt
fun clean tb id_fun =
tb |> Termtab.map
(fn _ => filter_out (BoxID.is_eq_ancestor ctxt id o id_fun))
fun clean_terms_1 (ids, ct) =
(filter_out (BoxID.is_eq_ancestor ctxt id) ids, ct)
fun clean_terms tb =
tb |> Termtab.map (fn _ => clean_terms_1)
in
ctxt |> Data.map (
K {terms = clean_terms terms, equiv = clean equiv fst,
all_equiv = clean all_equiv fst,
contain = contain, simp = clean simp fst, subsimp = clean subsimp fst,
reps = clean reps fst})
end
fun equiv_eq_better ctxt (id, th) (id', th') =
Util.rhs_of th aconv Util.rhs_of th' andalso BoxID.is_eq_ancestor ctxt id id'
fun simp_eq_better ctxt (id, th) (id', th') =
if BoxID.is_eq_ancestor ctxt id id' then
let val (t, t') = (Util.rhs_of th, Util.rhs_of th')
in t aconv t' orelse Term_Ord.term_ord (t, t') = LESS end
else false
fun clear_incr ctxt =
let
val {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
Data.get ctxt
fun clear_one cmp infos =
if exists (BoxID.has_incr_id o fst) infos then
infos |> map (apfst BoxID.replace_incr_id)
|> Util.max_partial cmp
else
infos
fun clear cmp tb =
tb |> Termtab.map (fn _ => clear_one cmp)
fun clear_term_one (ids, ct) =
if exists BoxID.has_incr_id ids then
(ids |> map BoxID.replace_incr_id
|> Util.max_partial (BoxID.is_eq_ancestor ctxt), ct)
else
(ids, ct)
fun clear_term tb =
tb |> Termtab.map (fn _ => clear_term_one)
in
ctxt |> Data.map (
K {terms = clear_term terms,
equiv = clear (equiv_eq_better ctxt) equiv,
all_equiv = clear (equiv_eq_better ctxt) all_equiv,
contain = contain,
simp = clear (simp_eq_better ctxt) simp,
subsimp = clear (simp_eq_better ctxt) subsimp,
reps = clear (equiv_eq_better ctxt) reps})
end
fun map_terms f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = f terms, equiv = equiv, all_equiv = all_equiv,
contain = contain, simp = simp, subsimp = subsimp, reps = reps}
fun map_equiv f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = f equiv, all_equiv = all_equiv,
contain = contain, simp = simp, subsimp = subsimp, reps = reps}
fun map_all_equiv f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = equiv, all_equiv = f all_equiv,
contain = contain, simp = simp, subsimp = subsimp, reps = reps}
fun map_contain f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = equiv, all_equiv = all_equiv,
contain = f contain, simp = simp, subsimp = subsimp, reps = reps}
fun map_simp f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = equiv, all_equiv = all_equiv,
contain = contain, simp = f simp, subsimp = subsimp, reps = reps}
fun map_subsimp f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = equiv, all_equiv = all_equiv,
contain = contain, simp = simp, subsimp = f subsimp, reps = reps}
fun map_reps f {terms, equiv, all_equiv, contain, simp, subsimp, reps} =
{terms = terms, equiv = equiv, all_equiv = all_equiv,
contain = contain, simp = simp, subsimp = subsimp, reps = f reps}
fun add_contain ct subt ctxt =
let
val {contain, ...} = Data.get ctxt
val contain_subt = the_default [] (Termtab.lookup contain subt)
in
if member (op aconvc) contain_subt ct then ctxt
else ctxt |> Data.map (map_contain (Termtab.update (subt, ct :: contain_subt)))
end
fun immediate_contains ctxt t =
let
val {contain, ...} = Data.get ctxt
in
the_default [] (Termtab.lookup contain t)
end
fun in_table_raw_ids ctxt t =
let
val {terms, ...} = Data.get ctxt
in
case Termtab.lookup terms t of
NONE => []
| SOME (ids, _) => ids
end
fun in_table_raw_for_id ctxt (id, t) =
exists (BoxID.is_eq_descendent ctxt id) (in_table_raw_ids ctxt t)
fun in_table_raw ctxt t =
length (in_table_raw_ids ctxt t) > 0
fun add_term_raw (id, ct) ctxt =
let
val t = Thm.term_of ct
val prev_ids = in_table_raw_ids ctxt t
val ids_t = (id :: prev_ids)
|> Util.max_partial (BoxID.is_eq_ancestor ctxt)
in
ctxt |> Data.map (map_terms (Termtab.update (t, (ids_t, ct))))
end
fun get_all_terms ctxt =
let
val {terms, ...} = Data.get ctxt
in
map (fn (_, (_, ct)) => ct) (Termtab.dest terms)
end
fun get_all_id_terms ctxt =
let
val {terms, ...} = Data.get ctxt
in
maps (fn (_, (ids, ct)) => map (rpair ct) ids)
(Termtab.dest terms)
end
fun has_equiv_eq_better ctxt infos info' =
exists (fn info => equiv_eq_better ctxt info info') infos
fun add_equiv_raw (cur_info as (_, th)) ctxt =
let
val {equiv, ...} = Data.get ctxt
val t = Util.lhs_of th
val equiv_t = the_default [] (Termtab.lookup equiv t)
in
if exists (fn info => equiv_eq_better ctxt info cur_info) equiv_t then ctxt
else ctxt |> Data.map (map_equiv (
Termtab.update (
t, equiv_t |> filter_out (equiv_eq_better ctxt cur_info)
|> cons cur_info)))
end
fun add_equiv (id, th) ctxt =
let
val _ = assert (not (Util.lhs_of th aconv Util.rhs_of th)) "add_equiv: t == t'"
in
ctxt |> add_equiv_raw (id, th)
|> add_equiv_raw (id, meta_sym th)
end
fun equiv_neighs ctxt t =
let
val {equiv, ...} = Data.get ctxt
in
case Termtab.lookup equiv t of
NONE => []
| SOME infos => infos
end
fun get_all_equiv ctxt t =
let
val {all_equiv, ...} = Data.get ctxt
in
the (Termtab.lookup all_equiv t)
handle Option.Option => raise Fail "all_equiv: not found"
end
fun update_simp (id, th) ctxt =
let
val {simp, ...} = Data.get ctxt
val ct = Thm.lhs_of th
val t = Thm.term_of ct
val simp_t = the_default [([], Thm.reflexive ct)] (Termtab.lookup simp t)
in
if exists (fn info => simp_eq_better ctxt info (id, th)) simp_t then ctxt
else
ctxt |> Data.map (map_simp (
Termtab.update (
t, simp_t |> filter_out (simp_eq_better ctxt (id, th))
|> cons (id, th))))
end
fun get_rewrite_info ctxt ct =
let
val {simp, ...} = Data.get ctxt
in
case Termtab.lookup simp (Thm.term_of ct) of
NONE => [([], Thm.reflexive ct)]
| SOME infos => infos
end
fun get_rewrite id ctxt ct =
case get_rewrite_info ctxt ct of
[] => Thm.reflexive ct
| ths' => ths' |> filter (BoxID.is_eq_descendent ctxt id o fst)
|> map snd
|> Util.max (rev_order o simp_ord)
fun merge_simp_infos ctxt lsts =
let
val ids = map (map fst) lsts |> BoxID.get_all_merges ctxt
fun get_for_id_lst id lst =
lst |> filter (BoxID.is_eq_descendent ctxt id o fst)
|> map snd |> Util.max (rev_order o simp_ord)
fun get_for_id id = (id, map (get_for_id_lst id) lsts)
in
map get_for_id ids
end
fun get_subterm_rewrite_info ctxt ct =
let
val (cf, subs) = Drule.strip_comb ct
in
if null subs then [([], Thm.reflexive ct)] else
(map (get_rewrite_info ctxt) subs)
|> merge_simp_infos ctxt
|> map (fn (id, equivs) => (id, Util.comb_equiv (cf, equivs)))
|> Util.max_partial (simp_eq_better ctxt)
end
fun remove_rep (id, th) ctxt =
let
val {reps, ...} = Data.get ctxt
val t = Util.lhs_of th
val reps_t = the_default [] (Termtab.lookup reps t)
val _ = assert (member eq_info reps_t (id, th)) "remove_rep: not found"
in
ctxt |> Data.map (map_reps (Termtab.map_entry t (remove eq_info (id, th))))
end
fun update_subsimp (id, th) ctxt =
let
val {subsimp, ...} = Data.get ctxt
val (t, t') = (Util.lhs_of th, Util.rhs_of th)
val subsimp_t = the_default [] (Termtab.lookup subsimp t)
in
if exists (fn info => simp_eq_better ctxt info (id, th)) subsimp_t then ctxt
else
let
val th' = meta_sym th
val (rem, keep) = filter_split (simp_eq_better ctxt (id, th)) subsimp_t
in
ctxt |> Data.map (map_subsimp (Termtab.update (t, (id, th) :: keep)))
|> Data.map (map_reps (Termtab.map_default (t', []) (cons (id, th'))))
|> fold remove_rep (map (apsnd meta_sym) rem)
end
end
fun get_head_rep_info ctxt t =
let
val {reps, ...} = Data.get ctxt
in
case Termtab.lookup reps t of
NONE => []
| SOME infos => infos
end
fun get_head_rep id ctxt t =
get_first (fn (id', t') =>
if BoxID.is_eq_ancestor ctxt id' id then SOME t' else NONE)
(get_head_rep_info ctxt t)
fun get_head_rep_with_id_th ctxt (id, th) =
get_head_rep_info ctxt (Util.rhs_of th) |> map (BoxID.merge_eq_infos ctxt (id, th))
fun get_cached_subterm_rewrite_info ctxt t =
let
val {subsimp, ...} = Data.get ctxt
in
case Termtab.lookup subsimp t of
NONE => []
| SOME infos => infos
end
fun get_cached_subterm_rewrite id ctxt ct =
case get_cached_subterm_rewrite_info ctxt (Thm.term_of ct) of
[] => Thm.reflexive ct
| ths' => ths' |> filter (BoxID.is_eq_descendent ctxt id o fst)
|> map snd
|> Util.max (rev_order o simp_ord)
fun head_simplify id ctxt ct =
case get_head_rep id ctxt (Thm.term_of ct) of
NONE => Thm.reflexive ct
| SOME th => Util.transitive_list [th, get_rewrite id ctxt (Thm.rhs_of th)]
fun simplify id ctxt ct =
if in_table_raw ctxt (Thm.term_of ct) then
get_rewrite id ctxt ct else
let
val th = subterm_simplify id ctxt ct
in
Util.transitive_list [th, head_simplify id ctxt (Thm.rhs_of th)]
end
and subterm_simplify id ctxt ct =
if in_table_raw ctxt (Thm.term_of ct) then
get_cached_subterm_rewrite id ctxt ct else
let
val (cf, subs) = Drule.strip_comb ct
val equivs = map (simplify id ctxt) subs
in
Util.comb_equiv (cf, equivs)
end
fun simp_val id ctxt ct = Thm.rhs_of (simplify id ctxt ct)
fun simp_val_t id ctxt t =
Util.rhs_of (simplify id ctxt (Thm.cterm_of ctxt t))
fun simplify_info ctxt ct =
if in_table_raw ctxt (Thm.term_of ct) then
get_rewrite_info ctxt ct else
let
val subterm_info = subterm_simplify_info ctxt ct
fun get_rewrite_with_id_th (id', th') =
(get_rewrite_info ctxt (Thm.rhs_of th'))
|> map (BoxID.merge_eq_infos ctxt (id', th'))
val head_info =
subterm_info |> maps (get_head_rep_with_id_th ctxt)
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
|> maps get_rewrite_with_id_th
in
subterm_info @ head_info |> Util.max_partial (simp_eq_better ctxt)
end
and subterm_simplify_info ctxt ct =
if in_table_raw ctxt (Thm.term_of ct) then
get_cached_subterm_rewrite_info ctxt (Thm.term_of ct) else
let
val (cf, subs) = Drule.strip_comb ct
in
if null subs then [([], Thm.reflexive ct)] else
(map (simplify_info ctxt) subs)
|> merge_simp_infos ctxt
|> map (fn (id, equivs) => (id, Util.comb_equiv (cf, equivs)))
|> Util.max_partial (simp_eq_better ctxt)
end
fun is_equiv id ctxt (ct1, ct2) =
ct1 aconvc ct2 orelse simp_val id ctxt ct1 aconvc simp_val id ctxt ct2
fun is_equiv_t id ctxt (t1, t2) =
t1 aconv t2 orelse is_equiv id ctxt (Thm.cterm_of ctxt t1, Thm.cterm_of ctxt t2)
fun get_head_equiv ctxt cu =
let
val u = Thm.term_of cu
val _ = assert (not (Term.is_open u)) "get_all_head_equivs: u is open"
fun rep_eq_better (id1, th1) (id2, th2) =
BoxID.is_eq_ancestor ctxt id1 id2 andalso
is_equiv id2 ctxt (Thm.rhs_of th1, Thm.rhs_of th2)
fun get_all_equiv_under_id (id', th') =
(get_all_equiv ctxt (Util.rhs_of th'))
|> map (BoxID.merge_eq_infos ctxt (id', th'))
in
if in_table_raw ctxt u then
get_all_equiv ctxt u
else
cu |> subterm_simplify_info ctxt
|> maps (get_head_rep_with_id_th ctxt)
|> Util.max_partial rep_eq_better
|> maps get_all_equiv_under_id
|> cons ([], Thm.reflexive cu)
|> Util.max_partial (equiv_eq_better ctxt)
end
fun get_head_equiv_with_t ctxt (id, cu) t =
let
fun is_valid (_, th) =
if Term.is_Var t then true
else if Term.is_Var (Term.head_of t) then true
else Term.aconv_untyped (Term.head_of (Util.rhs_of th), Term.head_of t)
in
(get_head_equiv ctxt cu)
|> filter is_valid
|> BoxID.merge_box_with_info ctxt id
end
fun process_update_simp inits ctxt =
let
fun eq_update ((id, th), (id', th')) =
(id = id' andalso Thm.prop_of th aconv Thm.prop_of th')
fun process_simp (id, th) (to_process, ctxt) =
if simp_ord (th, get_rewrite id ctxt (Thm.lhs_of th)) = LESS then
(insert eq_update (id, th) to_process, update_simp (id, th) ctxt)
else
(to_process, ctxt)
fun process_term ct (to_process, ctxt) =
let
val subsimps = get_subterm_rewrite_info ctxt ct
val ctxt' = fold update_subsimp subsimps ctxt
in
fold process_simp subsimps (to_process, ctxt')
end
fun update_step (to_process, ctxt) =
case to_process of
[] => ([], ctxt)
| (id, th) :: rest =>
let
val t = Util.lhs_of th
fun process_neigh (id', th') =
BoxID.merge_eq_infos ctxt (id', meta_sym th') (id, th)
val new_simp = map process_neigh (equiv_neighs ctxt t)
in
(rest, ctxt) |> fold process_simp new_simp
|> fold process_term (immediate_contains ctxt t)
|> update_step
end
in
([], ctxt) |> fold process_simp inits |> update_step |> snd
end
fun equiv_info ctxt id (ct1, ct2) =
let
val simp1 = simplify_info ctxt ct1
val simp2 = simplify_info ctxt ct2
fun compare (id1, th1) (id2, th2) =
if Util.rhs_of th1 aconv Util.rhs_of th2 then
[(BoxID.merge_boxes ctxt (id1, id2), Util.transitive_list [th1, meta_sym th2])]
else []
in
(maps (fn s1 => maps (compare s1) simp2) simp1)
|> BoxID.merge_box_with_info ctxt id
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
end
fun equiv_info_t ctxt id (t1, t2) =
equiv_info ctxt id (Thm.cterm_of ctxt t1, Thm.cterm_of ctxt t2)
fun subequiv_info ctxt id (ct1, ct2) =
if not ((Term.head_of (Thm.term_of ct1))
aconv Term.head_of (Thm.term_of ct2)) then []
else let
val simp1 = subterm_simplify_info ctxt ct1
val simp2 = subterm_simplify_info ctxt ct2
fun compare (id1, th1) (id2, th2) =
if Util.rhs_of th1 aconv Util.rhs_of th2 then
[(BoxID.merge_boxes ctxt (id1, id2),
Util.transitive_list [th1, meta_sym th2])]
else []
in
(maps (fn s1 => maps (compare s1) simp2) simp1)
|> BoxID.merge_box_with_info ctxt id
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
end
fun get_reachable_terms trav_contains ctxt ts =
let
fun helper (new, all) =
case new of
[] => ([], all)
| t :: rest =>
let
val contains =
if trav_contains then
map Thm.term_of (immediate_contains ctxt t)
else []
val neighs = (equiv_neighs ctxt t)
|> map (fn (_, th) => Util.rhs_of th)
val new' = (contains @ neighs)
|> distinct (op aconv)
|> subtract (op aconv) all
val all' = new' @ all
in
helper (rest @ new', all')
end
in
snd (helper (ts, ts))
end
fun add_all_equiv_raw (cur_info as (_, th)) ctxt =
let
val {all_equiv, ...} = Data.get ctxt
val t = Util.lhs_of th
val equiv_t = the_default [] (Termtab.lookup all_equiv t)
in
if exists (fn info => equiv_eq_better ctxt info cur_info) equiv_t then ctxt
else ctxt |> Data.map (map_all_equiv (
Termtab.update (
t, equiv_t |> filter_out (equiv_eq_better ctxt cur_info)
|> cons cur_info)))
end
fun update_all_equiv id th ctxt =
let
val (ct1, ct2) = (Thm.lhs_of th, Thm.rhs_of th)
val t1_equiv = get_all_equiv ctxt (Thm.term_of ct1)
val t2_equiv = get_all_equiv ctxt (Thm.term_of ct2)
fun process_pair ((id1, eq1), (id2, eq2)) ctxt =
let
val id' = BoxID.merge_boxes
ctxt (id, BoxID.merge_boxes ctxt (id1, id2))
val eq = Util.transitive_list [meta_sym eq1, th, eq2]
in
ctxt |> add_all_equiv_raw (id', eq)
|> add_all_equiv_raw (id', meta_sym eq)
end
in
fold process_pair (Util.all_pairs (t1_equiv, t2_equiv)) ctxt
end
fun add_rewrite_raw id th ctxt =
let
val (ct1, ct2) = (Thm.lhs_of th, Thm.rhs_of th)
val t1_rinfo = get_rewrite_info ctxt ct1
val t2_rinfo = get_rewrite_info ctxt ct2
val t1_news = t2_rinfo |> map (BoxID.merge_eq_infos ctxt (id, th))
val t2_news = t1_rinfo |> map (BoxID.merge_eq_infos ctxt (id, meta_sym th))
in
ctxt |> add_equiv (id, th)
|> process_update_simp (t1_news @ t2_news)
|> update_all_equiv id th
end
fun complete_table ctxt =
let
fun find_new_equiv ct =
let
val equivs = get_all_equiv ctxt (Thm.term_of ct)
in
(get_subterm_rewrite_info ctxt ct)
|> maps (get_head_rep_with_id_th ctxt)
|> Util.max_partial (equiv_eq_better ctxt)
|> filter_out (has_equiv_eq_better ctxt equivs)
end
val new_equivs = (maps find_new_equiv (get_all_terms ctxt))
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
in
case new_equivs of
[] => ([], ctxt)
| (id, th) :: _ =>
let
val ctxt' = ctxt |> add_rewrite_raw id th
val (edges, ctxt'') = complete_table ctxt'
in
((id, th) :: edges, ctxt'')
end
end
fun add_term' (id, ct) ctxt =
if in_table_raw_for_id ctxt (id, Thm.term_of ct) then ctxt
else let
val t = Thm.term_of ct
val imm_subterms = UtilLogic.list_subterms t
val id_subs = map (fn t => (id, Thm.cterm_of ctxt t)) imm_subterms
val ctxt' = ctxt |> fold add_term' id_subs |> add_term_raw (id, ct)
in
if in_table_raw ctxt t then ctxt'
else let
val simps = get_subterm_rewrite_info ctxt' ct
in
ctxt' |> fold (add_contain ct) imm_subterms
|> fold update_simp simps
|> fold update_subsimp simps
|> add_all_equiv_raw ([], Thm.reflexive ct)
end
end
fun add_term (id, ct) ctxt =
if in_table_raw_for_id ctxt (id, Thm.term_of ct) then ([], ctxt)
else ctxt |> add_term' (id, ct) |> complete_table
fun add_term_list term_infos ctxt =
case term_infos of
[] => ([], ctxt)
| (id, ct) :: rest =>
let
val (edges, ctxt') = add_term (id, ct) ctxt
val (edges', ctxt'') = add_term_list rest ctxt'
in
(edges @ edges', ctxt'')
end
fun add_rewrite (id, eq_th) ctxt =
let
val meta_eq = if Util.is_meta_eq (Thm.prop_of eq_th) then eq_th
else UtilLogic.to_meta_eq eq_th
val (ct1, ct2) = meta_eq |> Thm.cprop_of |> Thm.dest_equals
in
if is_equiv id ctxt (ct1, ct2) then ([], ctxt)
else
ctxt |> add_term' (id, ct1) |> add_term' (id, ct2)
|> add_rewrite_raw id meta_eq
|> complete_table
|> apfst (cons (id, meta_eq))
end
fun get_new_terms (ctxt, ctxt') =
let
fun get_for_term ct =
(in_table_raw_ids ctxt' (Thm.term_of ct))
|> filter_out (fn id => in_table_raw_for_id ctxt (id, Thm.term_of ct))
|> map (rpair ct)
in
maps get_for_term (get_all_terms ctxt')
end
end