Abduction: fix the previous commit.

data61 · Aug 9, 2023 · b274380 · b274380
1 parent 7d6e3bf
commit b274380
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 26 deletions.
diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy
@@ -11,14 +11,7 @@ begin
 
 (*** Top_Down_Util ***)
 ML_file \<open>Top_Down_Util.ML\<close>
-ML_file \<open>Generalise_By_Renaming.ML\<close>
-ML_file \<open>Term_Table_for_Abduction.ML\<close>
-ML_file \<open>Generalise_Then_Extend.ML\<close>
-ML_file \<open>Abstract_Same_Term.ML\<close>
-ML_file \<open>Remove_Function.ML\<close>
-ML_file \<open>Remove_Outermost_Assumption.ML\<close>
-ML_file \<open>Replace_Imp_With_Eq.ML\<close>
-ML_file \<open>SeLFiE_For_Top_Down.ML\<close>
+
 ML_file \<open>And_Node.ML\<close>
 ML_file \<open>Or_Node.ML\<close>
 ML_file \<open>Or2And_Edge.ML\<close>
@@ -27,6 +20,15 @@ ML_file \<open>Update_Abduction_Node.ML\<close>
 ML_file \<open>Abduction_Graph.ML\<close>
 ML_file \<open>Update_Abduction_Graph.ML\<close>
 ML_file \<open>Shared_State.ML\<close>
+
+ML_file \<open>Generalise_By_Renaming.ML\<close>
+ML_file \<open>Term_Table_for_Abduction.ML\<close>
+ML_file \<open>Generalise_Then_Extend.ML\<close>
+ML_file \<open>Abstract_Same_Term.ML\<close>
+ML_file \<open>Remove_Function.ML\<close>
+ML_file \<open>Remove_Outermost_Assumption.ML\<close>
+ML_file \<open>Replace_Imp_With_Eq.ML\<close>
+ML_file \<open>SeLFiE_For_Top_Down.ML\<close>
 ML_file \<open>All_Top_Down_Conjecturing.ML\<close>
 ML_file \<open>Seed_Of_Or2And_Edge.ML\<close>
 ML_file \<open>Proof_By_Abduction.ML\<close>

diff --git a/Abduction/Shared_State.ML b/Abduction/Shared_State.ML
@@ -17,9 +17,12 @@ type synched_term2string_table;
 val mk_term2string_table   : unit -> synched_term2string_table;
 val get_lemma_name         : synched_term2string_table -> Proof.context -> term  -> string;
 val get_orkey_name         : synched_term2string_table -> Proof.context -> Abduction_Graph.key -> string;
-
+(*
+type synched_string2term_table;
+val mk_string2term_table: unit -> synched_string2term_table;
+val is_completely_proved: synched_string2term_table -> string -> term;
+*)
 type synched_abduction_graph = abduction_graph Synchronized.var;
-
 val mk_synched_abduction_graph                    : Proof.context -> term -> synched_abduction_graph;
 val update_is_branch                              : Abduction_Graph.key -> synched_abduction_graph -> unit;
 val add_andnodes                                  : terms -> synched_abduction_graph -> Abduction_Graph.keys;
@@ -82,7 +85,6 @@ fun is_refuted (synched_table:synched_term2bool_table) (pst:Proof.state) (cnjctr
     result
   end;
 
-
 fun any_of_these_is_refuted (synched_table:synched_term2bool_table) (pst:Proof.state) (terms:terms) =
     exists (is_refuted synched_table pst) terms;
 
@@ -96,20 +98,33 @@ fun mk_term2string_table _ = Synchronized.var "term2string_table" Term_Table.emp
 local
 
 val lookup           = Utils.the' "lookup for term2string_table failed." oo Term_Table.lookup;
-fun insert (cnjctr:term, lemma_name:string) (old_table:term2string_table) =
-  if   defined old_table cnjctr
-  then old_table
-  else Term_Table.insert (op =) (cnjctr, lemma_name) old_table;
+fun insert_string (cnjctr:term, lemma_name:string) (old_table:term2string_table) =
+  case try (Term_Table.insert (op =) (cnjctr, lemma_name)) old_table
+  of NONE           => old_table
+   | SOME new_table => new_table;
 
 in
 
 fun get_lemma_name (synched_table:synched_term2string_table) (ctxt:Proof.context) (term:term) =
   let
     val standardized_term  = Top_Down_Util.standardize_vnames term                           : term;
+    val old_table          = Synchronized.value synched_table                                : term2string_table;
+    val already_checked    = defined old_table standardized_term                             : bool;
     fun mk_new_name_pair _ = (standardized_term, Top_Down_Util.mk_new_lemma_name ctxt false) : (term * string);
-    val _                  = Synchronized.change synched_table (insert (mk_new_name_pair ())): unit;
-    val new_table          = Synchronized.value synched_table                                : term2string_table;
-    val result             = lookup new_table standardized_term                              : string;
+
+    val _                 =
+      if   already_checked then ()
+      else
+        let
+          (* It is okay to spend some time to run quick-check before calling Synchronized.change:
+           * Even if other threads find a counter-example for the same conjecture,
+           * the result should be the same. *)
+          val pair = mk_new_name_pair standardized_term
+        in
+          Synchronized.change synched_table (insert_string pair): unit
+        end;
+    val new_table          = Synchronized.value synched_table  : term2string_table;
+    val result             = lookup new_table standardized_term: string;
   in
     result
   end;

diff --git a/Abduction/Top_Down_Util.ML b/Abduction/Top_Down_Util.ML
@@ -401,11 +401,3 @@ fun mk_pst_to_prove_from_term (pst:Proof.state) (term:term): Proof.state =
     in
       Proof.theorem NONE (K I) [[(prop, [])]] (Proof.context_of pst): Proof.state
     end;
-
-(*** signature TOP_DOWN_CONJECTURING ***)
-signature TOP_DOWN_CONJECTURING =
-sig
-
-val top_down_conjectures: Shared_State.synched_term2string_table -> Proof.state -> term -> (string * term) list;
-
-end;