sort terms when addning new nodes to graphs.

Author: yutakang

Abduction/Abduction_Graph.ML

@@ -99,14 +99,11 @@ fun node_type_compare (Or_N,     Or_N    ) = EQUAL
  |  node_type_compare (O2A_E i1, O2A_E i2) = Int.compare (i1, i2)
  |  node_type_compare (O2A_E _,  _       ) = GREATER;
 
-fun term_compare (trm1, trm2) =
-  Term_Ord.term_ord ((Top_Down_Util.standardize_vnames trm1), (Top_Down_Util.standardize_vnames trm2))
-
 (* PGraph_Key *)
 structure PGraph_Key =
     struct
       type key = (node_type * terms(*normal terms not thms*))
-      val  ord = prod_ord node_type_compare (list_ord term_compare)
+      val  ord = prod_ord node_type_compare (list_ord Top_Down_Util.term_compare)
     end:KEY
 
 (* PGraph *)
@@ -134,14 +131,23 @@ fun equal_keys key_pair = PGraph_Key.ord key_pair = EQUAL;
 type is_final_goal = bool;
 
 fun mk_ornode (is_final_goal:is_final_goal) (lemma_name:string) (goal:term) =
+let
+  val standardized_goal = Top_Down_Util.standardize_vnames goal;
+in
   (
-    (Or_N, [goal]): key,
-    Abduction_Node.mk_ornode is_final_goal lemma_name goal: abduction_node
-   );
+    (Or_N, [standardized_goal]): key,
+    Abduction_Node.mk_ornode is_final_goal lemma_name standardized_goal: abduction_node
+   )
+end;
 
 fun mk_andnode (goals:terms) =
-  ((And_N, goals): key,
-    Abduction_Node.mk_andnode goals);
+let
+  val standardized_terms = map Top_Down_Util.standardize_vnames goals;
+  val sorted_terms       = sort Term_Ord.term_ord standardized_terms;
+in
+  ((And_N, sorted_terms): key,
+    Abduction_Node.mk_andnode sorted_terms)
+end;
 
 (* key to term *)
 fun orkey_to_term (Or_N, [orleaf_term]) = orleaf_term

Abduction/All_Top_Down_Conjecturing.ML

@@ -158,6 +158,11 @@ fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list =
     result
   end;
 
+structure S4TD = SeLFiE_for_Top_Down;
+
+fun run_assertion (ctxt:Proof.context) (trm:term) (assert:Eval_Syntactic_Sugar.assert) =
+    S4TD.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) assert trm;
+
 fun top_down_conjectures (ctxt:Proof.context) trm =
   let
     val _ = tracing "[[[[[[[[[[[top_down_conjecture starts]]]]]]]]]]": unit;
@@ -177,9 +182,9 @@ fun top_down_conjectures (ctxt:Proof.context) trm =
 (*
       |> parallel_filter_out (fn (_, trm) => eq_over_same_func ctxt trm)
 *)
-      |> parallel_filter_out (fn (_, trm) => SeLFiE_for_Top_Down.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) SeLFiE_for_Top_Down.has_func_with_three_occs_in_a_row trm)
-      |> parallel_filter (fn (_, trm) => SeLFiE_for_Top_Down.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) SeLFiE_for_Top_Down.fvars_in_prem_should_appear_in_concl trm)
-      |> parallel_filter (fn (_, trm) => SeLFiE_for_Top_Down.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) SeLFiE_for_Top_Down.does_not_have_trivial_equality trm);
+      |> parallel_filter_out (fn (_, trm) => run_assertion ctxt trm S4TD.has_func_with_three_occs_in_a_row)
+      |> parallel_filter     (fn (_, trm) => run_assertion ctxt trm S4TD.fvars_in_prem_should_appear_in_concl)
+      |> parallel_filter     (fn (_, trm) => run_assertion ctxt trm S4TD.does_not_have_trivial_equality);
     val _ = tracing "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit;
   in
     results

Abduction/Proof_By_Abduction.ML

@@ -83,15 +83,15 @@ fun loop (counter: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 _ = tracing ("The number of keys worth expanding is:" ^ Int.toString (length orkeys_worth_expanding));
-        val _ = tracing "They are:"
-        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 (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 (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 (if solved then "    In loop. Solved." else "    In loop. Not solved.")
       in
         (if solved then K I else loop) (counter + 1) (new_pst, graph_w_keys_expanded)
       end

Abduction/Seed_Of_Or2And_Edge.ML

@@ -88,6 +88,13 @@ fun apply_PSL_to_get_seeds_of_or2and_edges (pst:Proof.state) =
     map mk_proof_key_value script_n_psts: seeds_of_or2and_edge
   end;
 
+(*TODO*)
+fun condition_to_filter_out_cnjctr (parent_or:term) (pst:Proof.state) (ag:abduction_graph) (cnjctr:term) = true;
+
+datatype conjecture_typ = Explicit_Conjecturing | Implicit_Conjecturing (*tactic application*);
+
+fun filtering_policy Explicit_Conjecturing = ()
+
 fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_graph) (seed:seed_of_or2and_edge) =
     let
       val final_goal      = get_final_goal_key ag |> snd |> hd: term;
@@ -120,7 +127,11 @@ fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_gra
       fun terms_have_counter_example_in_prems (pst:Proof.state) (terms:terms) =
           exists (has_counter_example_in_prems pst) terms: bool;
     in
-      trms_empty orelse too_large () orelse
+      (*TODO: for each stage we should filter out either
+              some of conjectures in a seed (Explicit Conjecturing) or
+              all conjectures in a seed (Implicit Conjecturing)*)
+      trms_empty orelse
+      too_large () orelse
       eq_to_final_goal () andalso seed_is_from_tactic seed orelse
       concl_is_eq_to_final_goal () (*andalso seed_is_from_tactic seed*) orelse
       has_func_with_three_occs_in_a_row () orelse

Abduction/Top_Down_Util.ML

@@ -34,6 +34,7 @@ val get_lemma_names_from_sh_output   : theory -> string -> strings;
 val assume_cnjctrs_in_pst            : (string * term) list -> Proof.state -> Proof.state;
 val is_thm_registered                : Proof.context -> string -> bool;
 val mk_new_lemma_name                : Proof.context -> string;
+val term_compare                     : term * term -> order;
 
 end;
 
@@ -232,4 +233,7 @@ fun mk_new_lemma_name (ctxt:Proof.context): string =
     else candidate_name
   end
 
+fun term_compare (trm1, trm2) =
+  Term_Ord.term_ord (standardize_vnames trm1, standardize_vnames trm2);
+
 end;