# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID 8dc9dc241973151d78e6764889e72e15fae7c555
# Parent  faab5feffb426c9c2a3a652adc41d39ae6d64f18
make TPTP tools work on polymorphic (TFF1) problems as well

diff -r faab5feffb42 -r 8dc9dc241973 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -5,10 +5,7 @@
 header {* ATP Problem Importer *}
 
 theory ATP_Problem_Import
-imports
-  Complex_Main
-  TPTP_Interpret
-  "~~/src/HOL/Library/Refute"
+imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
 begin
 
 ML_file "sledgehammer_tactics.ML"
@@ -24,8 +21,7 @@
 ML_file "atp_problem_import.ML"
 
 (*
-ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
-          "$TPTP/Problems/PUZ/PUZ107^5.p" *}
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
 *)
 
 end
diff -r faab5feffb42 -r 8dc9dc241973 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -13,7 +13,8 @@
   val refute_tptp_file : theory -> int -> string -> unit
   val can_tac : Proof.context -> tactic -> term -> bool
   val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
-  val atp_tac : Proof.context -> int -> (string * string) list -> int -> string -> int -> tactic
+  val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
+    int -> tactic
   val smt_solver_tac : string -> Proof.context -> int -> tactic
   val freeze_problem_consts : theory -> term -> term
   val make_conj : term list * term list -> term list -> term
@@ -56,7 +57,7 @@
   in
     (map (get_prop I) conjs,
      pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
-     Proof_Context.init_global thy)
+     Named_Target.theory_init thy)
   end
 
 
@@ -181,10 +182,16 @@
       end
   end
 
-fun atp_tac ctxt completeness override_params timeout prover =
+fun atp_tac ctxt completeness override_params timeout assms prover =
   let
-    val ctxt = ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+    val thy = Proof_Context.theory_of ctxt
+    val assm_ths0 = map (Skip_Proof.make_thm thy) assms
+    val ((assm_name, _), ctxt) = ctxt
+      |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+      |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
+
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
+    val ref_of_assms = (Facts.named assm_name, [])
   in
     Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
       ([("debug", if debug then "true" else "false"),
@@ -196,16 +203,16 @@
         else
           []) @
        override_params)
-      {add = map ref_of [ext, @{thm someI}], del = [], only = true}
+      {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
   end
 
-fun sledgehammer_tac demo ctxt timeout i =
+fun sledgehammer_tac demo ctxt timeout assms i =
   let
     val frac = if demo then 16 else 12
     fun slice mult completeness prover =
       SOLVE_TIMEOUT (mult * timeout div frac)
         (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
-        (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
+        (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
   in
     slice 2 0 ATP_Proof.spassN
     ORELSE slice 2 0 ATP_Proof.vampireN
@@ -228,12 +235,12 @@
     val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
   in SMT_Solver.smt_tac ctxt [] end
 
-fun auto_etc_tac ctxt timeout i =
+fun auto_etc_tac ctxt timeout assms i =
   SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
-    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Proof.spassN))
+    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
   ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
@@ -266,23 +273,26 @@
 fun sledgehammer_tptp_file thy timeout file_name =
   let
     val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
-    val conj = make_conj assms conjs
+    val conj = make_conj ([], []) conjs
+    val assms = op @ assms
   in
-    can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
+    can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj
     |> print_szs_of_success conjs
   end
 
 fun generic_isabelle_tptp_file demo thy timeout file_name =
   let
     val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
-    val conj = make_conj assms conjs
+    val conj = make_conj ([], []) conjs
+    val full_conj = make_conj assms conjs
+    val assms = op @ assms
     val (last_hope_atp, last_hope_completeness) =
       if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
   in
-    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
+    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
+     can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
      can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
-       (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
+       (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
     |> print_szs_of_success conjs
   end
 
diff -r faab5feffb42 -r 8dc9dc241973 src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -10,9 +10,9 @@
   type fact_override = Sledgehammer_Fact.fact_override
 
   val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
-    int -> tactic
+    thm list -> int -> tactic
   val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
-    int -> tactic
+    thm list -> int -> tactic
 end;
 
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
@@ -26,7 +26,7 @@
 open Sledgehammer_MaSh
 open Sledgehammer_Commands
 
-fun run_prover override_params fact_override i n ctxt goal =
+fun run_prover override_params fact_override chained i n ctxt goal =
   let
     val thy = Proof_Context.theory_of ctxt
     val mode = Normal
@@ -39,10 +39,9 @@
     val reserved = reserved_isar_keyword_table ()
     val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts concl_t
-      |> relevant_facts ctxt params name
-             (the_default default_max_facts max_facts) fact_override hyp_ts
-             concl_t
+      nearly_all_facts ctxt ho_atp fact_override reserved css_table chained hyp_ts concl_t
+      |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
+        hyp_ts concl_t
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
@@ -54,22 +53,24 @@
     handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end
 
-fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
+fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
   let val override_params = override_params @ [("preplay_timeout", "0")] in
-    case run_prover override_params fact_override i i ctxt th of
+    (case run_prover override_params fact_override chained i i ctxt th of
       SOME facts =>
       Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
-          (maps (thms_of_name ctxt) facts) i th
-    | NONE => Seq.empty
+        (maps (thms_of_name ctxt) facts) i th
+    | NONE => Seq.empty)
   end
 
-fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
+fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
   let
     val override_params =
       override_params @
       [("preplay_timeout", "0"),
        ("minimize", "false")]
-    val xs = run_prover override_params fact_override i i ctxt th
-  in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
+    val xs = run_prover override_params fact_override chained i i ctxt th
+  in
+    if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty
+  end
 
 end;