From 6f649a2b81aa7144d8efd81700e7bbe6b1395d01 Mon Sep 17 00:00:00 2001 From: Yutaka Ng <7411634+yutakang@users.noreply.github.com> Date: Sat, 5 Aug 2023 21:17:40 +0100 Subject: [PATCH] Abduction: clean-up. --- Abduction/Abduction.thy | 50 -------------------- Abduction/Abduction_Graph.ML | 2 +- Abduction/Generalise_Then_Extend.ML | 5 +- Abduction/Or_Node.ML | 5 +- Abduction/Proof_By_Abduction.ML | 71 ++++++++--------------------- Abduction/Top_Down_Util.ML | 12 +---- PSL/PGT.ML | 1 + 7 files changed, 25 insertions(+), 121 deletions(-) diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index e39dc92a..9c30fa81 100644 --- a/Abduction/Abduction.thy +++ b/Abduction/Abduction.thy @@ -9,19 +9,6 @@ theory Abduction keywords "prove" :: thy_goal_stmt begin -lemma "True" - by auto - -ML\ -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 -\ - (*** Top_Down_Util ***) ML_file \Top_Down_Util.ML\ ML_file \Generalise_By_Renaming.ML\ @@ -129,41 +116,4 @@ val _ = theorem \<^command_keyword>\prove\ "prove"; end; \ -ML\ -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 \ 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 -\ - end \ No newline at end of file diff --git a/Abduction/Abduction_Graph.ML b/Abduction/Abduction_Graph.ML index f5fce357..a0aa83e5 100644 --- a/Abduction/Abduction_Graph.ML +++ b/Abduction/Abduction_Graph.ML @@ -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; diff --git a/Abduction/Generalise_Then_Extend.ML b/Abduction/Generalise_Then_Extend.ML index d450985f..618f9ce4 100644 --- a/Abduction/Generalise_Then_Extend.ML +++ b/Abduction/Generalise_Then_Extend.ML @@ -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 @@ -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 diff --git a/Abduction/Or_Node.ML b/Abduction/Or_Node.ML index e207cbd3..6b3ac2cd 100644 --- a/Abduction/Or_Node.ML +++ b/Abduction/Or_Node.ML @@ -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, diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML index 52caeeb5..1f414591 100644 --- a/Abduction/Proof_By_Abduction.ML +++ b/Abduction/Proof_By_Abduction.ML @@ -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" @@ -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) @@ -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."; @@ -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 @@ -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; \ No newline at end of file diff --git a/Abduction/Top_Down_Util.ML b/Abduction/Top_Down_Util.ML index 808ec858..c3c2db67 100644 --- a/Abduction/Top_Down_Util.ML +++ b/Abduction/Top_Down_Util.ML @@ -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; @@ -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 @@ -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; diff --git a/PSL/PGT.ML b/PSL/PGT.ML index 09f32254..fbe8b851 100644 --- a/PSL/PGT.ML +++ b/PSL/PGT.ML @@ -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;