File ‹auto2.ML›
signature SCORES =
sig
val item_score: raw_item -> int
val items_score: raw_item list -> int
val get_score: raw_update -> int
end;
structure Scores : SCORES =
struct
fun item_score ritem =
case ritem of
Handler _ => 0
| Fact (ty_str, tname, _) =>
if ty_str = TY_VAR then 10
else Integer.sum (map size_of_term tname)
fun items_score raw_items = Util.max int_ord (map item_score raw_items)
fun get_score raw_updt =
case raw_updt of
AddItems {raw_items, sc, ...} =>
(case sc of NONE => items_score raw_items | SOME n => n)
| AddBoxes {init_assum, sc, ...} =>
(case sc of NONE => 20 + 5 * size_of_term init_assum
| SOME n => n)
| ResolveBox _ => ~1
| ShadowItem _ => ~1
end
val print_trace =
Attrib.setup_config_bool @{binding "print_trace"} (K false)
val print_intended =
Attrib.setup_config_bool @{binding "print_intended"} (K false)
val print_term =
Attrib.setup_config_bool @{binding "print_term"} (K false)
val print_shadow =
Attrib.setup_config_bool @{binding "print_shadow"} (K false)
val print_score =
Attrib.setup_config_bool @{binding "print_score"} (K false)
val max_steps =
Attrib.setup_config_int @{binding "max_steps"} (K 2000)
signature PROOFSTATUS =
sig
val check_hyps: box_id -> thm -> status -> unit
val scoring: proofstep -> int -> box_item list -> status ->
(box_item -> raw_update list) -> update list
val process_shadow: update -> status -> status
val process_resolve: update -> status -> status
val apply_update_instant: update -> status -> status
val process_fact_all: box_id -> int -> box_item list -> status -> status
val process_add_items: update -> status -> status
val process_add_boxes: update -> status -> status
val apply_update: update -> status -> status
val init_status: Proof.context -> term -> status
val solve_root: int * status -> int * status
end;
functor ProofStatus(
structure Auto2Data: AUTO2_DATA;
structure BoxItem: BOXITEM;
structure ItemIO: ITEM_IO;
structure Normalizer: NORMALIZER;
structure Logic_ProofSteps: LOGIC_PROOFSTEPS;
structure Property: PROPERTY;
structure PropertyData: PROPERTY_DATA;
structure ProofStepData: PROOFSTEP_DATA;
structure RewriteTable: REWRITE_TABLE;
structure Status: STATUS;
structure UtilBase: UTIL_BASE;
structure UtilLogic: UTIL_LOGIC;
structure Update: UPDATE;
structure WellformData: WELLFORM_DATA;
): PROOFSTATUS =
struct
fun check_hyps id th (st as {ctxt, ...}) =
let
val hyps = Thm.hyps_of th
val inits = Status.get_init_assums st id
val handlers =
(Status.get_handlers st)
|> filter (fn (id', _) => BoxID.is_eq_ancestor ctxt id' id)
|> map (fn (_, (_, t, _)) => t)
val extra = subtract (op aconv) (inits @ handlers) hyps
in
if null extra then ()
else let
val _ = trace_tlist ctxt "extra:" extra
in
raise Fail "illegal hyp"
end
end
fun scoring {name, ...} sc items (st as {ctxt, ...}) func =
let
val merged_id = BoxItem.merged_id ctxt items
in
if BoxID.is_box_resolved ctxt merged_id orelse
exists (Status.query_shadowed st merged_id) items then []
else
let
val scs = map #sc items
val max_sc = fold (curry Int.max) scs sc
val raw_updts = (func (List.last items))
|> map Update.replace_id_of_update
fun process_raw_updt raw_updt =
let
val id = Update.target_of_update raw_updt
in
if BoxID.is_box_resolved ctxt id then []
else if exists (Status.query_shadowed st id) items then []
else
[{sc = Scores.get_score raw_updt + max_sc, prfstep_name = name,
source = items, raw_updt = raw_updt}]
end
in
maps process_raw_updt raw_updts
end
end
fun process_shadow (updt as {raw_updt, ...}) (st as {ctxt, ...}) =
case raw_updt of
ShadowItem {id = shadow_id, item as {ty_str, ...}} =>
let
val _ = if not (Config.get ctxt print_trace) orelse
not (Config.get ctxt print_shadow) then ()
else if ty_str = TY_TERM andalso
not (Config.get ctxt print_term) then ()
else tracing ("Shadowing " ^
ItemIO.string_of_item ctxt item ^
" at box " ^ BoxID.string_of_box_id shadow_id ^
" (" ^ Update.source_info updt ^ ")")
in
st |> Status.add_shadowed (shadow_id, item)
end
| _ => raise Fail "process_shadow: wrong type of update"
fun process_resolve (updt as {sc, raw_updt, ...}) (st as {ctxt, ...}) =
case raw_updt of
ResolveBox {id, th} =>
let
val _ = if Config.get ctxt print_trace then
tracing ("Finished box " ^ BoxID.string_of_box_id id ^
" (" ^ Update.source_info updt ^ ")")
else ()
fun update_one i st =
let
val cur_parent = BoxID.get_parent_at_i ctxt id i
val res_th = Status.get_on_resolve st id i th
val _ = check_hyps cur_parent res_th st
val res_obj_th = apply_to_thm (UtilLogic.to_obj_conv ctxt) res_th
val updt = {sc = sc, prfstep_name = "$RESOLVE", source = [],
raw_updt = Logic_ProofSteps.logic_thm_update
ctxt (cur_parent, res_obj_th)}
in
st |> apply_update_instant updt
end
in
if BoxID.is_box_resolved ctxt id then st
else if id = [BoxID.home_id] then
st |> Status.set_resolve_th (Status.get_on_resolve st id 0 th)
|> Status.add_resolved id
else
st |> fold update_one (0 upto (length id) - 1)
|> Status.add_resolved id
end
| _ => raise Fail "process_resolve: wrong type of update"
and apply_update_instant (updt as {raw_updt, ...}) (st as {ctxt, ...}) =
let
val id = Update.target_of_update raw_updt
val _ = assert (not (BoxID.has_incr_id id))
in
if BoxID.is_box_resolved ctxt id then st else
case raw_updt of
ResolveBox _ => process_resolve updt st
| ShadowItem _ => process_shadow updt st
| _ => Status.add_to_queue updt st
end
fun process_step_single sc items prfstep (st as {ctxt, ...}) =
let
val {args, func, ...} = prfstep
val arg = the_single (filter_out ItemIO.is_side_match args)
val items' = filter (ItemIO.pre_match_arg ctxt arg) items
val f = case func of
OneStep f => f
| TwoStep _ =>
raise Fail "process_step_single: wrong type of func."
fun process_one_item item st =
let
val updts = scoring prfstep sc [item] st (f ctxt)
in
st |> fold apply_update_instant updts
end
in
st |> fold process_one_item items'
end
fun process_step_pair sc items items' prfstep (st as {ctxt, ...}) =
let
val {args, func, ...} = prfstep
val (arg1, arg2) = the_pair (filter_out ItemIO.is_side_match args)
val f = case func of
TwoStep f => f
| _ => raise Fail "process_step_pair: wrong type of func."
fun filter_pairs (left, right) =
if length left < length right then
let
val left' = filter (ItemIO.pre_match_arg ctxt arg1) left
in
if null left' then ([], [])
else (left', filter (ItemIO.pre_match_arg ctxt arg2) right)
end
else
let
val right' = filter (ItemIO.pre_match_arg ctxt arg2) right
in
if null right' then ([], [])
else (filter (ItemIO.pre_match_arg ctxt arg1) left, right')
end
fun process_pairs (left, right) st =
let
val (left', right') = filter_pairs (left, right)
fun process_pair left_item func right_item st =
if BoxItem.eq_item (left_item, right_item) then st else
let
val updts =
scoring prfstep sc [left_item, right_item] st func
in
st |> fold apply_update_instant updts
end
fun loop_right left_item st =
let
val func = f ctxt left_item
in
st |> fold (process_pair left_item func) right'
end
in
st |> fold loop_right left'
end
in
st |> process_pairs (items, items')
|> process_pairs (subtract BoxItem.eq_item items items', items)
end
fun process_prfstep sc items items' prfstep (st as {ctxt, ...}) =
let
val {args, ...} = prfstep
val items = filter_out (
fn item => BoxID.is_box_resolved ctxt (#id item) orelse
Status.query_removed st item) items
in
if null items then st
else if length (filter_out ItemIO.is_side_match args) = 1 then
st |> process_step_single sc items prfstep
else
st |> process_step_pair sc items items' prfstep
end
fun get_rewr_terms ctxt item =
let
val {ty_str, tname, ...} = item
val ts = map Thm.term_of tname
val rewr_terms = ItemIO.rewr_terms_of_item ctxt (ty_str, ts)
val terms = rewr_terms |> maps UtilLogic.get_all_subterms
|> distinct (op aconv)
|> filter_out Util.has_vars
val headt = if ty_str = TY_PROP then
if UtilLogic.is_neg (the_single ts) then
[UtilLogic.dest_not (the_single ts)]
else ts
else []
in
headt @ terms
end
fun get_rewr_terms2 ctxt item =
let
val {ty_str, tname, ...} = item
val ts = map Thm.term_of tname
val rewr_terms = ItemIO.rewr_terms_of_item ctxt (ty_str, ts)
in
rewr_terms |> maps UtilLogic.get_all_subterms_skip_if
|> distinct (op aconv)
|> filter_out Util.has_vars
|> filter_out (fn t => fastype_of t = UtilBase.boolT)
end
fun process_add_terms id sc items (st as {ctxt, ...}) =
let
val term_infos = items |> maps (get_rewr_terms ctxt)
|> distinct (op aconv)
|> map (pair id o Thm.cterm_of ctxt)
val old_items =
(Status.get_items st)
|> filter_out (fn {id, ...} => BoxID.is_box_resolved ctxt id)
|> subtract BoxItem.eq_item items
val ctxt' = ctxt |> Auto2Data.add_terms old_items term_infos
fun exists_item t =
Status.find_ritem_exact st id (Fact (TY_TERM, [t], UtilBase.true_th))
val terms2 = items |> maps (get_rewr_terms2 ctxt)
|> distinct (op aconv)
|> filter_out exists_item
|> filter_out (fn t => fastype_of t = UtilBase.boolT)
val updt =
{sc = sc, prfstep_name = "$TERM", source = [],
raw_updt = AddItems {id = id, sc = NONE,
raw_items = map BoxItem.term_to_fact terms2}}
in
st |> (if length terms2 > 0 then Status.add_to_queue updt else I)
|> Status.map_context (K ctxt')
end
fun process_fact_all id sc items (st as {ctxt, ...}) =
if null items then st else
let
val thy = Proof_Context.theory_of ctxt
val items' =
(Status.get_items st)
|> filter_out (fn {id, ...} => BoxID.is_box_resolved ctxt id)
val old_items = subtract BoxItem.eq_item items items'
val ctxt' = Auto2Data.get_incr_type old_items items ctxt
val ts =
(maps Auto2Data.relevant_terms_single items @
maps (Property.strip_property_field thy o dest_arg o UtilLogic.prop_of' o snd)
(PropertyData.get_new_property ctxt') @
map fst (WellformData.get_new_wellform_data ctxt'))
|> distinct (op aconv)
|> RewriteTable.get_reachable_terms true ctxt
val init_items = filter_out (BoxItem.match_ty_str TY_PROPERTY) items
fun incr_filt {id = id', tname, ...} =
exists (Util.has_subterm ts) (map Thm.term_of tname) andalso
BoxID.is_box_unresolved ctxt (BoxID.merge_boxes ctxt (id, id'))
val incr_items =
if null ts then []
else old_items |> filter incr_filt
|> cons BoxItem.null_item
val thy = Proof_Context.theory_of ctxt
val prfsteps = ProofStepData.get_prfsteps thy
val all_items = init_items @ incr_items
in
st |> Status.map_context (K ctxt')
|> fold (process_prfstep sc all_items items') prfsteps
|> Status.map_context Auto2Data.get_single_type
|> Status.clear_incr
end
fun process_add_items (updt as {sc, prfstep_name, raw_updt, ...})
(st as {ctxt, ...}) =
case raw_updt of
AddItems {id, raw_items = ritems, ...} =>
let
val (ctxt', subst) = BoxItem.obtain_variant_frees (ctxt, ritems)
val ritems' =
ritems |> map (BoxItem.instantiate subst)
|> (if prfstep_name = "$RESOLVE" orelse
prfstep_name = "$INIT_BOX" then
maps (Normalizer.normalize_keep ctxt')
else
maps (Normalizer.normalize ctxt'))
|> distinct BoxItem.eq_ritem
val (dup_ritems, new_ritems) =
if sc = 0 then ([], ritems')
else filter_split (Status.find_ritem_exact st id) ritems'
val _ = if null dup_ritems orelse
not (Config.get ctxt print_trace) orelse
not (Config.get ctxt print_intended) then () else
if prfstep_name = "$TERM" andalso
not (Config.get ctxt print_term) then ()
else tracing ("Intend to add " ^
Update.update_info ctxt' id dup_ritems ^
" (" ^ Update.source_info updt ^ ")")
val (handlers, ritems') =
filter_split BoxItem.is_handler_raw new_ritems
val uid_incr = length ritems'
val uid_next = Status.get_num_items st
val uid_string = if uid_incr = 1 then string_of_int uid_next
else string_of_int uid_next ^ "-" ^
string_of_int (uid_next + uid_incr - 1)
val sc_string = if Config.get ctxt print_score then
(string_of_int sc) ^ ", "
else ""
val _ = if null new_ritems orelse
not (Config.get ctxt print_trace) then () else
if prfstep_name = "$TERM" andalso
not (Config.get ctxt print_term) then ()
else tracing ("Add " ^ Update.update_info ctxt' id ritems' ^
" (" ^ uid_string ^ ", " ^ sc_string ^
Update.source_info updt ^ ")")
val items =
map (fn i => BoxItem.mk_box_item
ctxt' (uid_next + i, id, sc, nth ritems' i))
(0 upto (length ritems' - 1))
val handlers_info = map (pair id o BoxItem.dest_handler_raw) handlers
in
st |> Status.map_context (K ctxt')
|> fold Status.add_handler handlers_info
|> process_add_terms id sc items
|> fold Status.add_item (map BoxItem.item_with_incr items)
|> process_fact_all id sc (map BoxItem.item_with_incr items)
end
| _ => raise Fail "process_add_items: wrong type of update"
fun process_add_boxes (updt as {sc, raw_updt, ...}) (st as {ctxt, ...}) =
case raw_updt of
AddBoxes {id, init_assum, ...} =>
let
val ritem = init_assum |> Thm.cterm_of ctxt
|> Thm.assume |> Update.thm_to_ritem
val _ = assert (fastype_of init_assum = propT)
"process_add_boxes: assumption is not of type prop."
val neg_form_opt = if id = [] then NONE else
init_assum |> UtilLogic.dest_Trueprop |> UtilLogic.get_neg
|> Status.find_fact st id
val prev_prim_box = Status.find_prim_box st id init_assum
in
if is_some prev_prim_box then st
else if is_some neg_form_opt then
let
val th = the neg_form_opt
val updt = {sc = sc, prfstep_name = "$RESOLVE", source = [],
raw_updt = Logic_ProofSteps.logic_thm_update
ctxt (id, th)}
in
st |> apply_update_instant updt
end
else let
val _ = if Config.get ctxt print_trace then
tracing ("Add box under " ^ BoxID.string_of_box_id id ^ " (" ^
Update.source_info updt ^ ")")
else ()
val (prim_id, st') = st |> Status.map_context (K ctxt)
|> Status.add_prim_box id init_assum
val new_id = [prim_id]
val _ = if Config.get ctxt print_trace then
tracing (BoxID.string_of_box_id new_id ^ ": " ^
Syntax.string_of_term ctxt init_assum)
else ()
val ritems' =
case ritem of
Handler _ => [ritem]
| Fact (ty_str, _, th) =>
if ty_str = TY_PROP andalso UtilLogic.is_neg (UtilLogic.prop_of' th) then
map Update.thm_to_ritem (
Logic_ProofSteps.split_not_imp_th th)
else [ritem]
val item_updt = {
sc = sc, prfstep_name = "$INIT_BOX", source = [],
raw_updt = AddItems {id = new_id, sc = NONE, raw_items = ritems'}}
in
st' |> process_add_items item_updt
end
end
| _ => raise Fail "process_add_boxes: wrong type of update"
fun apply_update (updt as {raw_updt, ...}) (st as {ctxt, ...}) =
let
val id = Update.target_of_update raw_updt
val _ = assert (not (BoxID.has_incr_id id))
in
if BoxID.is_box_resolved ctxt id then st else
case raw_updt of
AddItems _ => process_add_items updt st
| AddBoxes _ => process_add_boxes updt st
| ResolveBox _ => process_resolve updt st
| ShadowItem _ => process_shadow updt st
end
fun init_status ctxt subgoal =
let
val raw_updt = AddBoxes {id = [], sc = NONE, init_assum = UtilLogic.get_neg' subgoal}
val updt = {sc = 0, prfstep_name = "$INIT", source = [],
raw_updt = raw_updt}
in
ctxt |> Status.empty_status
|> Status.add_item BoxItem.null_item
|> apply_update updt
end
fun solve_root (steps, (st as {queue, ctxt, ...})) =
if BoxID.is_box_resolved ctxt [BoxID.home_id] then
(steps, st)
else if steps = 0 then
error "Maximum number of steps reached"
else let
val updt = Updates_Heap.min queue
handle List.Empty => error "No more moves"
val st' = st |> Status.delmin_from_queue |> apply_update updt
in
solve_root (steps - 1, st')
end
end
signature AUTO2 =
sig
val auto2_tac: Proof.context -> tactic
end
functor Auto2(
structure ProofStatus: PROOFSTATUS;
structure Status: STATUS;
structure UtilLogic: UTIL_LOGIC;
): AUTO2 =
struct
fun auto2_tac ctxt state =
let
val subgoals = state |> Thm.cprop_of |> Drule.strip_imp_prems
val steps = Config.get ctxt max_steps
in
if null subgoals then Seq.empty else
let
val c_subgoal = hd subgoals
val subgoal = Thm.term_of c_subgoal
val _ = tracing (
"Subgoal 1 of " ^ (string_of_int (length subgoals)) ^ ":\n" ^
(Syntax.string_of_term ctxt subgoal) ^ "\n")
val subgoal_norm = Conv.every_conv [
Util.normalize_meta_horn ctxt,
UtilLogic.to_obj_conv ctxt] c_subgoal
val st = ProofStatus.init_status ctxt (Util.rhs_of subgoal_norm)
val (steps', st') =
Util.timer ("Total time: ",
fn _ => ProofStatus.solve_root (steps, st))
val _ = writeln ("Finished in " ^
(string_of_int (steps - steps')) ^ " steps.")
val th = st' |> Status.get_resolve_th
|> Thm.equal_elim (meta_sym subgoal_norm)
in
Seq.single (Thm.implies_elim state th)
end
end
end