File ‹wfdata.ML›
signature WELLFORM_DATA =
sig
val clean_resolved: box_id -> Proof.context -> Proof.context
val clear_incr: Proof.context -> Proof.context
val initialize_wellform_data: term -> Proof.context -> Proof.context
val get_wellform_for_term:
Proof.context -> term -> (cterm * (box_id * thm) list) list
val get_wellform_infos_for_term: Proof.context -> term -> (box_id * thm) list
val convert_wellform:
Proof.context -> box_id * thm -> box_id * thm -> box_id * thm
val get_wellform: Proof.context -> box_id * cterm -> (box_id * thm) list
val get_wellform_t: Proof.context -> box_id * term -> (box_id * thm) list
val get_complete_wellform:
Proof.context -> box_id * cterm -> (box_id * thm list) list
val cterm_to_wfterm:
Proof.context -> term list -> box_id * cterm -> (box_id * wfterm) list
val term_to_wfterm:
Proof.context -> term list -> box_id * term -> (box_id * wfterm) list
val add_wellform_data_raw:
term * (box_id * thm) -> Proof.context -> Proof.context
val find_fact: Proof.context -> box_item list -> box_id * cterm -> (box_id * thm) list
val complete_wellform_data_for_terms:
box_item list -> term list -> Proof.context -> Proof.context
val complete_wellform_data: box_item list -> Proof.context -> Proof.context
val get_new_wellform_data: Proof.context -> (term * (box_id * thm)) list
val simplify_info:
Proof.context -> term list -> cterm -> (box_id * (wfterm * thm)) list
val simplify: Proof.context -> term list -> cterm list -> box_id * wfterm ->
(box_id * (wfterm * thm)) list
val get_head_equiv:
Proof.context -> term list -> box_id * cterm -> (box_id * (wfterm * thm)) list
end;
functor WellformData(
structure Basic_UtilBase : BASIC_UTIL_BASE;
structure Basic_UtilLogic : BASIC_UTIL_LOGIC;
structure ItemIO: ITEM_IO;
structure Property: PROPERTY;
structure PropertyData: PROPERTY_DATA;
structure RewriteTable: REWRITE_TABLE;
structure WfTerm: WFTERM
) : WELLFORM_DATA =
struct
structure Data = Proof_Data
(
type T = ((cterm * (box_id * thm) list) list) Termtab.table
fun init _ = Termtab.empty
)
fun clean_resolved id ctxt =
let
fun clean_wellform_1 (ctarget, infos) =
(ctarget, filter_out (BoxID.is_eq_ancestor ctxt id o fst) infos)
fun clean_wellform tb =
tb |> Termtab.map (fn _ => map clean_wellform_1)
in
ctxt |> Data.map clean_wellform
end
fun clear_incr ctxt =
let
fun clear_one (ct, infos) =
if exists (BoxID.has_incr_id o fst) infos then
(ct, infos |> map (apfst BoxID.replace_incr_id)
|> Util.max_partial (BoxID.info_eq_better ctxt))
else
(ct, infos)
in
ctxt |> Data.map (Termtab.map (fn _ => map clear_one))
end
fun initialize_wellform_data t ctxt =
let
val wellform = Data.get ctxt
val thy = Proof_Context.theory_of ctxt
val targets = map (Thm.cterm_of ctxt) (WellForm.lookup_wellform_data thy t)
in
if Termtab.defined wellform t then ctxt
else if null targets then ctxt
else ctxt |> Data.map (Termtab.update (t, map (rpair []) targets))
end
fun get_wellform_for_term ctxt t =
let
val wellform = Data.get ctxt
in
the_default [] (Termtab.lookup wellform t)
end
fun get_wellform_infos_for_term ctxt t =
maps snd (get_wellform_for_term ctxt t)
fun convert_wellform ctxt (id', eq_th) (id, th) =
let
val (lhs, rhs) = Logic.dest_equals (Thm.prop_of eq_th)
val thy = Proof_Context.theory_of ctxt
in
if lhs aconv rhs then (id, th) else
case WellForm.lookup_wellform_pattern thy (Util.lhs_of eq_th, Basic_UtilLogic.prop_of' th) of
NONE => raise Fail "convert_wellform: invalid input."
| SOME (pat, data_pat) =>
let
val cargs1 = Util.dest_cargs (Thm.lhs_of eq_th)
val cargs2 = Util.dest_cargs (Thm.rhs_of eq_th)
val eq_ths =
map (fn (ct, ct') =>
(RewriteTable.equiv_info ctxt id' (ct, ct'))
|> filter (fn (id'', _) => id'' = id')
|> map snd |> the_single)
(cargs1 ~~ cargs2)
val pat_args = Util.dest_args pat
val th' = Basic_UtilLogic.apply_to_thm' (
Util.pattern_rewr_conv data_pat (pat_args ~~ eq_ths)) th
val subst' = pat_args ~~ map Thm.term_of cargs2
val prop' = Term.subst_atomic subst' data_pat
val _ = assert (Basic_UtilLogic.prop_of' th' aconv prop')
"convert_wellform: invalid output."
in
(BoxID.merge_boxes ctxt (id, id'), th')
end
end
fun get_wellform ctxt (id, ct) =
let
val t = Thm.term_of ct
in
if RewriteTable.in_table_raw_for_id ctxt (id, t) then
(get_wellform_infos_for_term ctxt t)
|> BoxID.merge_box_with_info ctxt id
else
let
fun process_head_rep (id', eq_th) =
(get_wellform_infos_for_term ctxt (Util.rhs_of eq_th))
|> map (convert_wellform ctxt (id', meta_sym eq_th))
in
(RewriteTable.subterm_simplify_info ctxt ct)
|> maps (RewriteTable.get_head_rep_with_id_th ctxt)
|> maps process_head_rep
|> BoxID.merge_box_with_info ctxt id
|> Util.max_partial (BoxID.info_eq_better ctxt)
end
end
fun get_wellform_t ctxt (id, t) =
get_wellform ctxt (id, Thm.cterm_of ctxt t)
fun get_complete_wellform ctxt (id, ct) =
let
val thy = Proof_Context.theory_of ctxt
val t = Thm.term_of ct
val targets = WellForm.lookup_wellform_data thy t
in
case targets of
[] => [(id, [])]
| _ =>
let
val data = (get_wellform ctxt (id, ct))
|> map (fn (id', th) => (Basic_UtilLogic.prop_of' th, (id', th)))
|> AList.group (op aconv)
|> map snd
val _ = assert (length data <= length targets)
"get_complete_wellform: unexpected length data"
in
if length data < length targets then []
else data |> BoxID.get_all_merges_info ctxt
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
end
end
fun cterm_to_wfterm ctxt fheads (id, ct) =
case Thm.term_of ct of
_ $ _ =>
let
val t = Thm.term_of ct
val (cf, cargs) = Drule.strip_comb ct
in
if forall (fn fhead => not (Util.is_head fhead t)) fheads then
[(id, WfTerm ct)] else
let
val wfdata = get_complete_wellform ctxt (id, ct)
fun process_wfdata (id', ths) =
cargs |> map (pair id')
|> map (cterm_to_wfterm ctxt fheads)
|> BoxID.get_all_merges_info ctxt
|> map (fn (id'', arg') => (id'', WfComb (cf, arg', ths)))
in
(maps process_wfdata wfdata)
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
end
end
| _ => [(id, WfTerm ct)]
fun term_to_wfterm ctxt fheads (id, t) =
cterm_to_wfterm ctxt fheads (id, Thm.cterm_of ctxt t)
fun add_wellform_data_raw (t, (id, th)) ctxt =
let
val cprop = Basic_UtilLogic.cprop_of' th
val wellform_data = get_wellform_for_term ctxt t
val infos = the (AList.lookup (op aconvc) wellform_data cprop)
handle Option.Option => raise Fail "add_wellform_data_raw"
in
if exists (fn info => BoxID.info_eq_better ctxt info (id, th)) infos then ctxt
else let
val infos' = infos |> filter_out (BoxID.info_eq_better ctxt (id, th))
|> cons (id, th)
in
ctxt |> Data.map (
Termtab.map_entry t (AList.map_entry (op aconvc) cprop (K infos')))
end
end
fun find_fact ctxt items (id, ct) =
let
val t = Thm.term_of ct
fun match_item item =
(ItemIO.match_arg ctxt (PropMatch t) item (id, fo_init))
|> map (fn ((id', _), th) => (id', th))
in
if Basic_UtilBase.is_eq_term t then
map (apsnd Basic_UtilLogic.to_obj_eq)
(RewriteTable.equiv_info ctxt id (Basic_UtilBase.cdest_eq ct))
else if Property.is_property t then
PropertyData.get_property ctxt (id, ct)
else
maps match_item items
end
fun complete_wellform_data_for_terms items ts ctxt =
let
fun get_for_t t =
let
val cur_data = get_wellform_for_term ctxt t
val target_ids = RewriteTable.in_table_raw_ids ctxt t
fun is_target (id, cprop) =
let
val prop_data = the (AList.lookup (op aconvc) cur_data cprop)
in
not (exists (fn (id', _) => BoxID.is_eq_ancestor ctxt id' id)
prop_data)
end
val targets = (Util.all_pairs (target_ids, map fst cur_data))
|> filter is_target
in
targets |> maps (find_fact ctxt items)
|> map (pair t)
end
val all_data = maps get_for_t ts
in
fold add_wellform_data_raw all_data ctxt
end
fun complete_wellform_data items ctxt =
let
val wellform = Data.get ctxt
val ts = Termtab.keys wellform
in
complete_wellform_data_for_terms items ts ctxt
end
fun get_new_wellform_data ctxt =
let
val wellform = Data.get ctxt
in
wellform |> Termtab.dest
|> maps (fn (t, vals) => map (pair t) (maps snd vals))
|> filter (fn (_, (id, _)) => BoxID.has_incr_id id)
end
fun simplify_info ctxt fheads ct =
let
val infos = RewriteTable.simplify_info ctxt ct
fun process_info (id, eq_th) =
let
val rhs = Thm.rhs_of eq_th
val wfts = cterm_to_wfterm ctxt fheads (id, rhs)
in
map (fn (id', wft) => (id', (wft, eq_th))) wfts
end
in
maps process_info infos
end
fun simplify ctxt fheads cts (id, wft) =
if null cts then [(id, (wft, Thm.reflexive (WfTerm.cterm_of wft)))]
else
cts |> map (simplify_info ctxt fheads)
|> BoxID.get_all_merges_info ctxt
|> BoxID.merge_box_with_info ctxt id
|> map (fn (id', wf_eqs) =>
(id', WfTerm.rewrite_on_eqs fheads wf_eqs wft))
fun get_head_equiv ctxt fheads (id, ct) =
let
val head_equivs =
ct |> RewriteTable.get_head_equiv ctxt
|> BoxID.merge_box_with_info ctxt id
fun process_head_equiv (id', eq_th) =
let
val rhs = Thm.rhs_of eq_th
val wfts = cterm_to_wfterm ctxt fheads (id', rhs)
in
map (fn (id'', wft) => (id'', (wft, eq_th))) wfts
end
in
maps process_head_equiv head_equivs
end
end