src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41091 0afdf5cde874
parent 41088 54eb8e7c7f9b
child 41134 de9e0adc21da
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 08 22:17:53 2010 +0100
@@ -15,10 +15,10 @@
   val conjecture_prefix : string
   val translate_atp_fact :
     Proof.context -> (string * 'a) * thm
-    -> term * ((string * 'a) * translated_formula) option
+    -> translated_formula option * ((string * 'a) * thm)
   val prepare_atp_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> (term * ((string * 'a) * translated_formula) option) list
+    -> (translated_formula option * ((string * 'a) * thm)) list
     -> string problem * string Symtab.table * int * (string * 'a) list vector
 end;
 
@@ -194,10 +194,10 @@
      ctypes_sorts = ctypes_sorts}
   end
 
-fun make_fact ctxt presimp ((name, loc), th) =
+fun make_fact ctxt presimp ((name, _), th) =
   case make_formula ctxt presimp name Axiom (prop_of th) of
     {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
-  | formula => SOME ((name, loc), formula)
+  | formula => SOME formula
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
     map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -244,16 +244,20 @@
      |> maps (fn (ss, ths) =>
                  if exists is_needed ss then map baptize ths else [])) @
     (if is_FO then [] else map baptize mandatory_helpers)
-    |> map_filter (Option.map snd o make_fact ctxt false)
+    |> map_filter (make_fact ctxt false)
   end
 
-fun translate_atp_fact ctxt (ax as (_, th)) =
-  (prop_of th, make_fact ctxt true ax)
+fun translate_atp_fact ctxt = `(make_fact ctxt true)
 
-fun translate_formulas ctxt full_types hyp_ts concl_t facts =
+fun translate_formulas ctxt full_types hyp_ts concl_t rich_facts =
   let
     val thy = ProofContext.theory_of ctxt
-    val (fact_ts, translated_facts) = ListPair.unzip facts
+    val fact_ts = map (prop_of o snd o snd) rich_facts
+    val (facts, fact_names) =
+      rich_facts
+      |> map_filter (fn (NONE, _) => NONE
+                      | (SOME fact, (name, _)) => SOME (fact, name))
+      |> ListPair.unzip
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
@@ -264,7 +268,6 @@
     val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
     (* TFrees in the conjecture; TVars in the facts *)
     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
-    val (fact_names, facts) = ListPair.unzip (map_filter I translated_facts)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'