reorganise the directory structure a little.

Author: yutakang

Abduction/All_Top_Down_Conjecturing.ML

@@ -67,9 +67,6 @@ fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list =
 
 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;
@@ -89,9 +86,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) => 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);
+      |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion ctxt trm S4TD.has_func_with_three_occs_in_a_row)
+      |> parallel_filter     (fn (_, trm) => S4TD.run_assertion ctxt trm S4TD.fvars_in_prem_should_appear_in_concl)
+      |> parallel_filter     (fn (_, trm) => S4TD.run_assertion ctxt trm S4TD.does_not_have_trivial_equality);
     val _ = tracing "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit;
   in
     results

Abduction/SeLFiE_For_Top_Down.ML

@@ -86,7 +86,7 @@ val has_func_with_three_occs_in_a_row =
     ]
   );
 
-fun run_assertion (pst:Proof.state)  (assrt:assert) (cnjctr:term) =
+fun run_assertion' (pst:Proof.state)  (assrt:assert) (cnjctr:term) =
   let
     val outer_path_to_unode_table = Outer_Path_To_Unode.pst_n_trm_to_path_to_unode_table pst cnjctr                                               : Outer_Path_To_Unode.path_to_unode_table;
     val gen_path_table            = Gen_Path.Outer_Path_To_Unode outer_path_to_unode_table                                                        : Gen_Path.gen_path_to_unode_table;
@@ -96,4 +96,7 @@ fun run_assertion (pst:Proof.state)  (assrt:assert) (cnjctr:term) =
     eval pst outer_path_to_unode_table outer_domains empty_argument assrt = True
   end;
 
+fun run_assertion (ctxt:Proof.context) (trm:term) (assert:Eval_Syntactic_Sugar.assert) =
+    run_assertion' (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) assert trm: bool;
+
 end;