# HG changeset patch
# User blanchet
# Date 1342593843 -7200
# Node ID e7f01b7e244e5ab2b0c008dad7771caf3e84cde4
# Parent  e0cf12269e60d0bd0403c98a3b514d0888d869ce
gracefully handle the case of empty theories when going up the accessibility chain

diff -r e0cf12269e60 -r e7f01b7e244e src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -20,7 +20,7 @@
 
 ML {*
 val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat};
+val thy = @{theory List};
 val params = Sledgehammer_Isar.default_params @{context} []
 *}
 
diff -r e0cf12269e60 -r e7f01b7e244e src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -43,7 +43,7 @@
         val _ = File.append path (query ^ update)
       in [name] end
     val thy_ths = old_facts |> thms_by_thy
-    val parents = parent_thms thy_ths thy
+    val parents = parent_facts thy_ths thy
   in fold do_fact new_facts parents; () end
 
 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
diff -r e0cf12269e60 -r e7f01b7e244e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -10,6 +10,8 @@
   type status = ATP_Problem_Generate.status
   type stature = ATP_Problem_Generate.stature
 
+  type fact = ((unit -> string) * stature) * thm
+
   type fact_override =
     {add : (Facts.ref * Attrib.src list) list,
      del : (Facts.ref * Attrib.src list) list,
@@ -27,13 +29,12 @@
     -> (((unit -> string) * 'a) * thm) list
   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
   val all_facts :
-    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
-    -> thm list -> status Termtab.table
-    -> (((unit -> string) * stature) * thm) list
-  val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
+    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
+    -> status Termtab.table -> fact list
+  val all_facts_of : theory -> fact list
   val nearly_all_facts :
     Proof.context -> bool -> fact_override -> thm list -> term list -> term
-    -> (((unit -> string) * stature) * thm) list
+    -> fact list
 end;
 
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -43,6 +44,8 @@
 open Metis_Tactic
 open Sledgehammer_Util
 
+type fact = ((unit -> string) * stature) * thm
+
 type fact_override =
   {add : (Facts.ref * Attrib.src list) list,
    del : (Facts.ref * Attrib.src list) list,
diff -r e0cf12269e60 -r e7f01b7e244e src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -8,6 +8,7 @@
 signature SLEDGEHAMMER_FILTER_ITER =
 sig
   type stature = ATP_Problem_Generate.stature
+  type fact = Sledgehammer_Fact.fact
   type params = Sledgehammer_Provers.params
   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
 
@@ -19,14 +20,14 @@
     -> string list
   val iterative_relevant_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
-    -> term list -> term -> (((unit -> string) * stature) * thm) list
-    -> (((unit -> string) * stature) * thm) list
+    -> term list -> term -> fact list -> fact list
 end;
 
 structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
 struct
 
 open ATP_Problem_Generate
+open Sledgehammer_Fact
 open Sledgehammer_Provers
 
 val trace =
@@ -333,12 +334,9 @@
         val res = rel_weight / (rel_weight + irrel_weight)
       in if Real.isFinite res then res else 0.0 end
 
-type annotated_thm =
-  (((unit -> string) * stature) * thm) * (string * ptype) list
-
 fun take_most_relevant ctxt max_facts remaining_max
         ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
-        (candidates : (annotated_thm * real) list) =
+        (candidates : ((fact * (string * ptype) list) * real) list) =
   let
     val max_imperfect =
       Real.ceil (Math.pow (max_imperfect,
diff -r e0cf12269e60 -r e7f01b7e244e src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -8,25 +8,23 @@
 sig
   type status = ATP_Problem_Generate.status
   type stature = ATP_Problem_Generate.stature
+  type fact = Sledgehammer_Fact.fact
+  type fact_override = Sledgehammer_Fact.fact_override
   type params = Sledgehammer_Provers.params
-  type fact_override = Sledgehammer_Fact.fact_override
   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
   type prover_result = Sledgehammer_Provers.prover_result
 
   val fact_name_of : string -> string
-  val all_non_tautological_facts_of :
-    theory -> (((unit -> string) * stature) * thm) list
+  val all_non_tautological_facts_of : theory -> fact list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val thms_by_thy : ('a * thm) list -> (string * thm list) list
   val has_thy : theory -> thm -> bool
-  val parent_thms : (string * thm list) list -> theory -> string list
+  val parent_facts : (string * thm list) list -> theory -> string list
   val features_of : theory -> status * thm -> string list
   val isabelle_dependencies_of : string list -> thm -> string list
   val goal_of_thm : theory -> thm -> thm
-  val run_prover :
-    Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm
-    -> prover_result
+  val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
   val generate_accessibility : theory -> bool -> string -> unit
   val generate_features : theory -> bool -> string -> unit
   val generate_isa_dependencies : theory -> bool -> string -> unit
@@ -42,8 +40,7 @@
 
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
-    -> term -> (((unit -> string) * stature) * thm) list
-    -> (((unit -> string) * stature) * thm) list
+    -> term -> fact list -> fact list
 end;
 
 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
@@ -205,11 +202,15 @@
 
 fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
 
-fun parent_thms thy_ths thy =
-  Theory.parents_of thy
-  |> map Context.theory_name
-  |> map_filter (AList.lookup (op =) thy_ths)
-  |> map List.last
+fun add_last_thms thy_ths thy =
+  case AList.lookup (op =) thy_ths (Context.theory_name thy) of
+    SOME (ths as _ :: _) => insert Thm.eq_thm (List.last ths)
+  | _ => add_parent_thms thy_ths thy
+and add_parent_thms thy_ths thy =
+  fold (add_last_thms thy_ths) (Theory.parents_of thy)
+
+fun parent_facts thy_ths thy =
+  add_parent_thms thy_ths thy []
   |> map (fact_name_of o Thm.get_name_hint)
 
 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
@@ -276,7 +277,7 @@
     fun do_thy ths =
       let
         val thy = theory_of_thm (hd ths)
-        val parents = parent_thms thy_ths thy
+        val parents = parent_facts thy_ths thy
         val ths = ths |> map (fact_name_of o Thm.get_name_hint)
       in fold do_thm ths parents; () end
   in List.app (do_thy o snd) thy_ths end