Skip to content

Commit

Permalink
Abduction: clean-up.
Browse files Browse the repository at this point in the history
  • Loading branch information
@yutakang
yutakang committed Aug 5, 2023
1 parent 1c051f9 commit 6f649a2
Show file tree
Hide file tree
Showing 7 changed files with 25 additions and 121 deletions.
50 changes: 0 additions & 50 deletions Abduction/Abduction.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,19 +9,6 @@ theory Abduction
keywords "prove" :: thy_goal_stmt
begin

lemma "True"
by auto

ML\<open>
Specification.theorem_cmd false "lemma" NONE (K I): Attrib.binding ->
(xstring * Position.T) list ->
Element.context list ->
Element.statement ->
bool -> local_theory -> Proof.state;
type sdf = Element.statement
\<close>

(*** Top_Down_Util ***)
ML_file \<open>Top_Down_Util.ML\<close>
ML_file \<open>Generalise_By_Renaming.ML\<close>
Expand Down Expand Up @@ -129,41 +116,4 @@ val _ = theorem \<^command_keyword>\<open>prove\<close> "prove";
end;
\<close>

ML\<open>
HOLogic.mk_conj;
Logic.mk_conjunction;
Logic.strip_imp_prems;
strip_imp_prems;
Synchronized.guarded_access;
Par_List.map;
fun prems (term:term) = Logic.strip_imp_prems;
TBC_Utils.term_has_counterexample_in_pst;
val asdf = Token.unparse;
val asdf2 = Token.explode;
val asdf3 = String.isPrefix "asd" "asdf";
fun get_topdown_lemma_names_from_sledgehammer_output (pst:Proof.state) (sh_output:string) =
let
val thy = Proof.theory_of pst : theory;
val keywords = Thy_Header.get_keywords thy : Keyword.keywords;
val tokens = Token.explode keywords Position.none sh_output;
val strings = map Token.unparse tokens: strings;
val filtered = filter (String.isPrefix "top_down_lemma_") strings: strings;
in
filtered
end;
val _ = Proof.local_skip_proof: bool -> Proof.state -> Proof.state;
val _ = Proof.assume;
val _ = (Method.sorry_text true);
val pro = @{prop "x (qrevflat var_0 nil2) nil2 = revflat var_0 \<Longrightarrow> x (qrevflat var_0 (x (rev var_1) nil2)) nil2 = x (revflat var_0) (rev var_1) "}
fun foo pst = Proof.theorem NONE (K I) [[(pro, [])]] (Proof.context_of pst) |> Proof.local_skip_proof true
\<close>

end
2 changes: 1 addition & 1 deletion Abduction/Abduction_Graph.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ val goal_as_string : Proof.state -> key -> string;
(* query on abduction_graph *)
val final_goal_proved_completely : abduction_graph -> bool;

val mk_pst_to_prove_from_orkey : Proof.state -> key -> Proof.state;(*TODO: Is it necessary to expose this function?*)
val mk_pst_to_prove_from_orkey : Proof.state -> key -> Proof.state;
val prove_orkey_completely : key -> abduction_graph -> Proof.state -> (Proof.state * strings) option;

val print_lemma_and_proof_of_key : Proof.state -> abduction_graph -> key -> string;
Expand Down
5 changes: 1 addition & 4 deletions Abduction/Generalise_Then_Extend.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,10 +89,10 @@ fun top_down_conjectures (pst:Proof.state) (orig_trm:term) =
val consts = get_consts_for_conjecturing ctxt orig_trm : terms;
val equality_pairs = get_both_sides_of_eqs_in_term orig_trm : (term * term) list;
val cleaned_pairs = map (apply2 (mk_unbound_bound_vars_free_vars ctxt)) equality_pairs: (term * term) list;
(*TODO: move this filter to mk_extended_rhses*)
fun is_nullary_const (Const (_, typ)) = Isabelle_Utils.count_numb_of_args_of_fun_typ typ = 0
| is_nullary_const _ = false
val nullalry_consts = filter is_nullary_const consts
fun add_candidate_args (lhs, rhs) = (lhs, distinct (op =) (rhs :: nullalry_consts @ standardized_fvars_in_gen) |> distinct (op =)) : term * term list;

fun generalise_pairs (lhs: term, rhs: term) =
let
Expand All @@ -104,11 +104,8 @@ fun top_down_conjectures (pst:Proof.state) (orig_trm:term) =
new_pairs: (term * term) list
end;
val generalised_pairs = map generalise_pairs cleaned_pairs |> flat;
fun add_candidate_args (lhs, rhs) = (lhs, distinct (op =) (rhs :: nullalry_consts @ standardized_fvars_in_gen) |> distinct (op =)) : term * term list;
val candidate_pairs = map add_candidate_args generalised_pairs : (term * term list) list;

val filtered_pairs = filter_out (is_Free o fst) candidate_pairs : (term * term list) list;

val extension_eqs = map (extension_for_one_lhs ctxt consts) filtered_pairs |> flat: terms;
val checked_eqs = check_terms ctxt extension_eqs : terms;
val results = map (pair "generalisation_then_extension") checked_eqs
Expand Down
5 changes: 3 additions & 2 deletions Abduction/Or_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,8 +64,9 @@ fun is_worth_proving (ctxt:Proof.context) (ornode:ornode) =
type is_final_goal = bool;
fun mk_ornode (ctxt:Proof.context) (is_final_goal:is_final_goal) (lemma_name:string) (goal:term) =
let
(*TODO: check if the name is already taken.*)
val name = (if is_final_goal then Top_Down_Util.mk_new_lemma_name ctxt is_final_goal else lemma_name);
val name = if is_final_goal
then Top_Down_Util.mk_new_lemma_name ctxt is_final_goal
else lemma_name;
in
{final_goal = is_final_goal,
is_branch = false,
Expand Down
71 changes: 18 additions & 53 deletions Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ type seeds_of_or2and_edge = SOOE.seeds_of_or2and_edge;

(* expand_ornode *)
fun expand_ornode (or_key as (Or_N, [lemma_term]):key) (pst:state, graph:abduction_graph): state * abduction_graph =
(*TODO: we should check if the node is still worth proving.*)
let
fun tracing' mssg = ()(*tracing mssg*);
val _ = tracing' "Start computing expand_ornode"
Expand All @@ -44,8 +43,7 @@ fun expand_ornode (or_key as (Or_N, [lemma_term]):key) (pst:state, graph:abducti
then
let
val _ = tracing' "We PROVED the or-node.";
val _= tracing' (Isabelle_Utils.trm_to_string (Proof.context_of pst) lemma_term);
val _ = tracing' "\n"
val _ = tracing' (Isabelle_Utils.trm_to_string (Proof.context_of pst) lemma_term);
val (_, proof) = the maybe_proved: (state * strings);
in
(pst, update_after_proving_ornode proof or_key (Proof.context_of pst) graph)
Expand All @@ -55,40 +53,19 @@ fun expand_ornode (or_key as (Or_N, [lemma_term]):key) (pst:state, graph:abducti
val _ = tracing' "We did NOT prove the or-node.";
(*top-down explicit conjecturing*)
val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures pst lemma_term : (string * term) list;
(*
val _ = tracing "\n\n++ explicit_conjectures ++ ";
val _ = map snd explicit_conjectures |> map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst));
*)
val filtered_explicit = filter_out (SOOE.condition_to_filter_out_cnjctr lemma_term pst graph false o snd) explicit_conjectures: (string * term) list;
(*
val _ = tracing "\n\n++ filtered_explicit ++ ";
val _ = map snd filtered_explicit |> map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst));
*)
val explicit_wo_counterexample = filter_out (Shared_State.is_refuted pst o snd) filtered_explicit : (string * term) list;
(*
val _ = tracing "\n\n++ explicit_wo_counterexample ++ ";
val _ = map snd explicit_wo_counterexample |> map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst));
*)
val seed_from_explicit = (*At the moment, we throw away the hints for top-down auxiliary lemma names, since incorporating this information requires changing the type of andnode.*)
SOOE.conjectures_to_seed_of_or2and_edge pst explicit_wo_counterexample : seed_of_or2and_edge;
val _ = tracing' "AAAAAAAAAAAAAAAAAAAAAA seed_from_explicit finished:"
val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge pst explicit_wo_counterexample : seed_of_or2and_edge;
val graph_extended_by_cnjctr = SOOE.decremental_abduction pst or_key seed_from_explicit graph : abduction_graph;
(*tactic application as conjecturing. a little expensive*)
val pst_to_prove = mk_pst_to_prove_from_orkey pst or_key : state;
val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges pst_to_prove : seeds_of_or2and_edge;
val _ = tracing' "\n AAAAAAAAAAAAAAAAAAAAAA The length of seeds_from_tactics:\n seeds are:"
(*val _ = map (Seed_Of_Or2And_Edge.print_seed_of_or2and_edge ctxt) seeds_from_tactics*)
val _ = tracing' (Int.toString (length seeds_from_tactics))
(*tactic application as conjecturing. A little expensive*)
val pst_to_prove = mk_pst_to_prove_from_orkey pst or_key : state;
val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges pst_to_prove : seeds_of_or2and_edge;
val filtered_seeds_from_tactics = SOOE.filter_out_bad_seeds_from_tactic lemma_term pst graph_extended_by_cnjctr seeds_from_tactics
|> (fn x => (tracing' (Int.toString (length x)); x))
|> filter_out (SOOE.seed_has_counterexample pst) : seeds_of_or2and_edge;
val _ = tracing' "AAAAAAAAAAAAAAAAAAAAAA The length of filtered_seeds_from_tactics:"
val _ = tracing' (Int.toString (length filtered_seeds_from_tactics))
val graph_extended_by_tactics = SOOE.seeds_to_updated_graph pst or_key filtered_seeds_from_tactics graph_extended_by_cnjctr : abduction_graph;
val _ = tracing' "AAAAAAAAAAAAAAAAAAAAAA graph_extended_by_tactics finished:"
|> filter_out (SOOE.seed_has_counterexample pst) : seeds_of_or2and_edge;
val graph_extended_by_tactics = SOOE.seeds_to_updated_graph pst or_key filtered_seeds_from_tactics graph_extended_by_cnjctr : abduction_graph;
in
(*seeds_to_updated_graph is very expensive*)
(pst, graph_extended_by_tactics(*expanded_graph*))
(pst, graph_extended_by_tactics)
end
end
| expand_ornode _ _ = error "expand_ornode failed. Not an Or_N.";
Expand All @@ -103,25 +80,16 @@ fun loop (counter:int) (max_depth:int) (pst:state, graph: abduction_graph) =
if counter < 8
then
let
val _ = tracing ("==== In loop. Counter is: " ^ Int.toString counter ^ " =====");
val ctxt = Proof.context_of pst;

val orkeys_worth_expanding = orkeys_tobe_expanded_in ctxt graph: keys;
(*
val orkeys_worth_expanding = Abduction_Tree_Proved.ornode_keys_that_need_proof ctxt max_depth graph: keys;
*)
val _ = tracing ("The number of keys worth expanding is:" ^ Int.toString (length orkeys_worth_expanding));
val _ = tracing "They are:"
val _ = map (tracing o Shared_State.get_orkey_name ctxt) orkeys_worth_expanding;
val _ = map (print_key ctxt) orkeys_worth_expanding
val (new_pst, graph_w_keys_expanded) = fold expand_ornode_if_original_goral_is_unproved orkeys_worth_expanding (pst, graph): (state * abduction_graph);

val solved = final_goal_proved_completely graph_w_keys_expanded: bool;
(*
val _ = tracing "VV before calling Abduction_Tree_Proved.graph_is_proved graph_w_keys_expanded:"
val solved = Abduction_Tree_Proved.graph_is_proved (Proof.context_of pst) graph_w_keys_expanded: bool;
*)
val _ = tracing (if solved then " In loop. Solved." else " In loop. Not solved.")
val _ = tracing ("==== In loop. Counter is: " ^ Int.toString counter ^ " =====");
val ctxt = Proof.context_of pst;
val orkeys_worth_expanding = orkeys_tobe_expanded_in ctxt graph: keys;
val _ = tracing ("The number of keys worth expanding is:" ^ Int.toString (length orkeys_worth_expanding));
val _ = tracing "They are:"
val _ = map (tracing o Shared_State.get_orkey_name ctxt) orkeys_worth_expanding;
val _ = map (print_key ctxt) orkeys_worth_expanding
val (_, graph_w_keys_expanded) = fold expand_ornode_if_original_goral_is_unproved orkeys_worth_expanding (pst, graph): (state * abduction_graph);
val solved = final_goal_proved_completely graph_w_keys_expanded: bool;
val _ = tracing (if solved then " In loop. Solved." else " In loop. Not solved.")
in
(if solved then K (K I) else loop) (counter + 1) max_depth ((*new_*)pst, graph_w_keys_expanded)
end
Expand All @@ -138,9 +106,6 @@ fun proof_by_abduction (pst:state) (term:(*normal*)term) =
val (final_pst, final_graph) = loop 0 max_depth (pst, initial_graph);
in
print_proof_of_graph final_pst final_graph
(*
Abduction_Tree_Proved.print_proof_script final_pst max_depth final_graph
*)
end;

end;
12 changes: 1 addition & 11 deletions Abduction/Top_Down_Util.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ val remove_Trueprop : term -> term;
val mk_free_variable_of_typ : typ -> int -> term;
val numb_of_distinct_fvars : term -> int;
val numb_of_distinct_bvars : term -> int;
val get_subtrms : term -> terms;
val get_both_sides_of_eqs_in_term : term -> (term * term) list;
val get_consts_for_conjecturing : Proof.context -> term -> terms;
val remove_type_consts : term -> term;
Expand Down Expand Up @@ -92,17 +91,9 @@ fun numb_of_distinct_fvars (trm:term) = numb_of_distinct_atom is_Free trm;

fun numb_of_distinct_bvars (trm:term) = numb_of_distinct_atom is_Bound trm;

(* How to get the list of subterms? *)(*TODO: code-duplication with Proof_Goal_Transformer.*)
fun get_subtrms (Const p:term) = [Const p]
| get_subtrms (Free p:term) = [Free p]
| get_subtrms (Var p:term) = [Var p]
| get_subtrms (Bound i:term) = [Bound i]
| get_subtrms (trm as Abs (_, _, sub)) = trm :: get_subtrms sub
| get_subtrms (trm as trm1 $ trm2) = trm :: get_subtrms trm1 @ get_subtrms trm2;

fun get_both_sides_of_eqs_in_term (term:term): (term * term) list =
let
val subtrms = get_subtrms term: terms;
val subtrms = Proof_Goal_Transformer.get_subtrms term: terms;
val pairs = List.mapPartial (try HOLogic.dest_eq) subtrms;
in
pairs
Expand Down Expand Up @@ -300,7 +291,6 @@ fun strip_outermost_meta_quantifiers (trm:term) =

fun mk_extended_rhses (ctxt:Proof.context) (candidate_args:terms) (candidate_func as Const _:term): terms =
let
(*TODO: if func does not take explicit functions, filter out non-nullary constants from candidate_args*)
val candidate_func_wo_type_consts = Top_Down_Util.remove_type_consts candidate_func : term;
val candidate_args_wo_type_consts = map Top_Down_Util.remove_type_consts candidate_args : terms;
val arg_numb = type_of candidate_func |> Term.binder_types |> length: int;
Expand Down
1 change: 1 addition & 0 deletions PSL/PGT.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ This file presents the functions for automatic generalization of tactics.
signature PROOF_GOAL_TRANSFORMER =
sig

val get_subtrms : term -> terms;
val generalize_str : Proof.context -> thm -> string list;
val conjecture_strs: Proof.context -> thm -> string list;

Expand Down

0 comments on commit 6f649a2

Please sign in to comment.