src/HOL/Tools/ATP/atp_waldmeister.ML

 General-purpose functions used by the Sledgehammer modules.
 *)
 
 signature ATP_WALDMEISTER =
 sig
-  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
-  type atp_connective = ATP_Problem.atp_connective
-  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
-  type atp_format = ATP_Problem.atp_format
-  type atp_formula_role = ATP_Problem.atp_formula_role
   type 'a atp_problem = 'a ATP_Problem.atp_problem
-  type ('a, 'b) atp_step = ('a,'b) ATP_Proof.atp_step
+  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
+  type 'a atp_proof = 'a ATP_Proof.atp_proof
+  type stature = ATP_Problem_Generate.stature
 
-  val const_prefix : char
-  val var_prefix : char
-  val free_prefix : char
-  val thm_prefix : string
-  val hypothesis_prefix : string
-  val thms_header : string
-  val conjecture_condition_name : string
-  val hypothesis_header : string
-  val waldmeister_output_file_path : string
-
-  val waldmeister_simp_header : string
-  val waldmeister_simp_thms : thm list
-
-  val thm_to_atps : bool -> thm -> (string * string, 'a) atp_term list
-  val trm_to_atp : term -> (string * string, 'a) atp_term
-  val atp_to_trm : (string, 'a) atp_term -> term
-  val trm_to_atp_to_trm : term -> term
-  val create_tptp_input : thm list -> term ->
-    (string * ((string * string ATP_Problem.atp_problem_line list) list
-      * (string Symtab.table * string Symtab.table) option)) option
-  val run_waldmeister :
-    string * (string ATP_Proof.atp_problem * (string Symtab.table * string Symtab.table) option)
-    -> string ATP_Proof.atp_proof
-  val atp_proof_step_to_term :
-    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step
-    -> (term,string) atp_step
-  val fix_waldmeister_proof :
-    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list ->
-    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list
+  val generate_waldmeister_problem: Proof.context -> term list -> term ->
+    ((string * stature) * term) list ->
+    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
+  val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof ->
+    (term, string) atp_step list
 end;
 
 structure ATP_Waldmeister : ATP_WALDMEISTER =
 struct
 
+open ATP_Util
 open ATP_Problem
 open ATP_Problem_Generate
 open ATP_Proof
 open ATP_Proof_Reconstruct
 

 type 'a atp_problem = 'a ATP_Problem.atp_problem
 
 val const_prefix = #"c"
 val var_prefix = #"V"
 val free_prefix = #"f"
-val thm_prefix = "fact"
-val hypothesis_prefix = "hypothesis"
-val thms_header = "facts"
 val conjecture_condition_name = "condition"
-val hypothesis_header = "hypothesis"
-val broken_waldmeister_formula_prefix = #"1"
 
-val waldmeister_simp_header = "Waldmeister first order logic facts"
-val waldmeister_simp_thms = @{thms waldmeister_fol}
-
-val temp_files_dir = "/home/albert/waldmeister"
-val input_file_name = "input.tptp"
-val output_file_name = "output.tptp"
-val waldmeister_input_file_path = temp_files_dir ^ "/" ^ input_file_name
-val waldmeister_output_file_path = temp_files_dir ^ "/" ^ output_file_name
-val script_path = "/opt/Isabelle/src/HOL/Tools/ATP/scripts/remote_atp -s Waldmeister---710 -t 30"
+val factsN = "Relevant facts"
+val helpersN = "Helper facts"
+val conjN = "Conjecture"
 
 exception Failure
 exception FailureMessage of string
 
 (*
 Some utilitary functions for translation.
 *)
 
 fun is_eq (Const (@{const_name "HOL.eq"}, _) $ _ $ _) = true
   | is_eq _ = false
-
-fun is_eq_thm thm = thm |> Thm.prop_of |> Object_Logic.atomize_term @{theory } |> is_eq
 
 fun gen_ascii_tuple str = (str, ascii_of str)
 
 (*
 Translation from Isabelle theorms and terms to ATP terms.

   | trm_to_atp'' _ args = args
 
 fun trm_to_atp' trm = trm_to_atp'' trm [] |> hd
 
 fun eq_trm_to_atp (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =
-  ATerm (((tptp_equal, tptp_equal), []), [trm_to_atp' lhs, trm_to_atp' rhs])
+    ATerm ((("equal", "equal"), []), [trm_to_atp' lhs, trm_to_atp' rhs])
   | eq_trm_to_atp _ = raise Failure
 
 fun trm_to_atp trm =
-  if is_eq trm then
-    eq_trm_to_atp trm
-  else
-    HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
+  if is_eq trm then eq_trm_to_atp trm
+  else HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
 
-fun thm_to_atps split_conj thm =
-  let
-    val prop_term = Thm.prop_of thm |> Object_Logic.atomize_term @{theory}
-  in
-    if split_conj then
-      map trm_to_atp (prop_term |> HOLogic.dest_conj)
-    else
-      [prop_term |> trm_to_atp]
-  end
+fun thm_to_atps split_conj prop_term =
+  if split_conj then map trm_to_atp (prop_term |> HOLogic.dest_conj)
+  else [prop_term |> trm_to_atp]
 
 fun prepare_conjecture conj_term =
   let
-    fun split_conj_trm (Const (@{const_name Pure.imp}, _)$ condition $ consequence) =
+    fun split_conj_trm (Const (@{const_name Pure.imp}, _) $ condition $ consequence) =
         (SOME condition, consequence)
       | split_conj_trm conj = (NONE, conj)
     val (condition, consequence) = split_conj_trm conj_term
   in
     (case condition of SOME x => HOLogic.dest_conj x |> map trm_to_atp | NONE => []

     (case args of
       [] => construct_term (ATerm (descr, args))
      | _ => Term.list_comb (construct_term (ATerm (descr, args)), map atp_to_trm' args))
      | atp_to_trm' _ = raise Failure
 
-fun atp_to_trm  (ATerm (("equal", _), [lhs, rhs])) =
+fun atp_to_trm (ATerm (("equal", _), [lhs, rhs])) =
     Const (@{const_name HOL.eq}, Type ("", [])) $ atp_to_trm' lhs $ atp_to_trm' rhs
   | atp_to_trm (ATerm (("$true", _), _)) = Const ("HOL.True", Type ("", []))
   | atp_to_trm _ = raise Failure
 
 fun formula_to_trm (AAtom aterm) = atp_to_trm aterm
   | formula_to_trm (AConn (ANot, [aterm])) =
     Const (@{const_name HOL.Not}, @{typ "bool \<Rightarrow> bool"}) $ formula_to_trm aterm
   | formula_to_trm _ = raise Failure
 
-(* Simple testing function for translation *)
-
-fun atp_only_readable_names (ATerm ((("=", _), ty), args)) =
-    ATerm (("equal", ty), map atp_only_readable_names args)
-  | atp_only_readable_names (ATerm (((descr, _), ty), args)) =
-    ATerm ((descr, ty), map atp_only_readable_names args)
-  | atp_only_readable_names _ = raise Failure
-
-val trm_to_atp_to_trm = eq_trm_to_atp #> atp_only_readable_names #> atp_to_trm
-
-(* Abstract translation from here on. *)
-
-fun name_of_thm thm =
-  Thm.get_tags thm
-  |> List.find (fn (x, _) => x = "name")
-  |> the |> snd
+(* Abstract translation *)
 
 fun mk_formula prefix_name name atype aterm =
-  Formula ((prefix_name ^ "_" ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
+  Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
 
-fun thms_to_problem_lines [] = []
-  | thms_to_problem_lines (t::thms) =
-    (thm_to_atps false t |>
-      map (mk_formula thm_prefix (name_of_thm t) Axiom)) @ thms_to_problem_lines thms
+fun problem_lines_of_fact prefix ((s, _), t) =
+  map (mk_formula prefix s Axiom) (thm_to_atps false t)
 
 fun make_nice problem = nice_atp_problem true CNF problem
-
-fun problem_to_string [] = ""
-  | problem_to_string ((kind, lines)::problems) =
-    "% " ^ kind ^ "\n"
-    ^ String.concat (map (tptp_string_of_line CNF) lines)
-    ^ "\n"
-    ^ problem_to_string problems
 
 fun mk_conjecture aterm =
   let
     val formula = mk_anot (AAtom aterm)
   in
-    Formula (gen_ascii_tuple hypothesis_prefix, Hypothesis, formula, NONE, [])
+    Formula ((conjecture_prefix ^ "0", ""), Hypothesis, formula, NONE, [])
   end
-
-fun mk_condition_lines [] = []
-  | mk_condition_lines (term::terms) =
-    mk_formula thm_prefix conjecture_condition_name Axiom term::mk_condition_lines terms
-
-fun create_tptp_input thms conj_t =
-    let
-      val (conditions, consequence) = prepare_conjecture conj_t
-      val thms_lines = thms_to_problem_lines thms
-      val condition_lines = mk_condition_lines conditions
-      val axiom_lines = thms_lines @ condition_lines
-      val conj_line = consequence |> mk_conjecture
-      val waldmeister_simp_lines =
-        if List.exists (fn x => not (is_eq_thm x)) thms orelse not (is_eq conj_t) then
-          [(waldmeister_simp_header, thms_to_problem_lines waldmeister_simp_thms)]
-        else
-          []
-      val problem =
-        waldmeister_simp_lines @ [(thms_header, axiom_lines), (hypothesis_header, [conj_line])]
-      val (problem_nice, symtabs) = make_nice problem
-    in
-      SOME (problem_to_string problem_nice, (problem_nice, symtabs))
-    end
-
-val waldmeister_proof_delims =
-  [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
-val known_waldmeister_failures = [(OutOfResources, "Too many function symbols"),
-     (Inappropriate, "****  Unexpected end of file."),
-     (Crashed, "Unrecoverable Segmentation Fault")]
-
-fun extract_proof_part output =
-  case
-    extract_tstplike_proof_and_outcome true
-      waldmeister_proof_delims known_waldmeister_failures output of
-    (x, NONE) => x | (_, SOME y) => raise FailureMessage (string_of_atp_failure y)
-
-fun cleanup () =
-  (OS.Process.system ("rm " ^ waldmeister_input_file_path);
-   OS.Process.system ("rm " ^ waldmeister_output_file_path))
-
-fun run_script input =
-  let
-    val outputFile = TextIO.openOut waldmeister_input_file_path
-  in
-    (TextIO.output (outputFile, input);
-    TextIO.flushOut outputFile;
-    TextIO.closeOut outputFile;
-    OS.Process.system (script_path ^ " " ^ waldmeister_input_file_path ^ " > " ^
-      waldmeister_output_file_path))
-  end
-
-fun read_result () =
-  let
-    val inputFile = TextIO.openIn waldmeister_output_file_path
-    fun readAllLines is =
-      if TextIO.endOfStream is then (TextIO.closeIn is; [])
-      else (TextIO.inputLine is |> the) :: readAllLines is
-  in
-    readAllLines inputFile |> String.concat
-  end
-
-fun run_waldmeister (input, (problem, SOME (_, nice_to_nasty_table))) =
-    (cleanup ();
-     run_script input;
-     read_result ()
-     |> extract_proof_part
-     |> atp_proof_of_tstplike_proof waldmeister_newN problem
-     |> nasty_atp_proof nice_to_nasty_table)
-  | run_waldmeister _ = raise Failure
 
 fun atp_proof_step_to_term (name, role, formula, formula_name, step_names) =
   (name, role, formula_to_trm formula, formula_name, step_names)
 
-fun fix_waldmeister_proof [] = []
-  | fix_waldmeister_proof (((name, extra_names), role, formula, formula_name, step_names)::steps) =
-    if String.sub (name, 0) = broken_waldmeister_formula_prefix then
-      ((name, extra_names), role, mk_anot formula, formula_name, step_names)::fix_waldmeister_proof steps
-    else
-      ((name, extra_names), role, formula, formula_name, step_names)::fix_waldmeister_proof steps
+fun generate_waldmeister_problem ctxt hyp_ts0 concl_t0 facts0 =
+  let
+    val hyp_ts = map HOLogic.dest_Trueprop hyp_ts0
+    val concl_t = HOLogic.dest_Trueprop concl_t0
+    val facts = map (apsnd HOLogic.dest_Trueprop) facts0
+
+    val (conditions, consequence) = prepare_conjecture concl_t
+    val fact_lines = maps (problem_lines_of_fact (fact_prefix ^ "0_" (* FIXME *))) facts
+    val condition_lines =
+      map (mk_formula fact_prefix conjecture_condition_name Hypothesis) conditions
+    val axiom_lines = fact_lines @ condition_lines
+    val conj_line = mk_conjecture consequence
+
+    val helper_lines =
+      if List.exists (is_eq o snd) facts orelse not (is_eq concl_t) then
+        [(helpersN,
+          @{thms waldmeister_fol}
+          |> map (fn th => (("", (Global, General)), HOLogic.dest_Trueprop (prop_of th)))
+          |> maps (problem_lines_of_fact helper_prefix))]
+      else
+        []
+    val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])]
+
+    val (nice_problem, symtabs) = make_nice problem
+  in
+    (nice_problem, Symtab.empty, [], Symtab.empty)
+  end
+
+fun termify_line ctxt (name, role, AAtom u, rule, deps) =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val t = u
+      |> atp_to_trm
+      |> infer_formula_types ctxt
+      |> HOLogic.mk_Trueprop
+  in
+    (name, role, t, rule, deps)
+  end
+
+fun termify_waldmeister_proof ctxt pool =
+  nasty_atp_proof pool
+  #> map (termify_line ctxt)
+  #> repair_waldmeister_endgame
 
 end;