moved code around
authorblanchet
Mon Jun 16 19:40:04 2014 +0200 (2014-06-16)
changeset 57262b2c629647a14
parent 57261 49c1db0313e6
child 57263 2b6a96cc64c9
moved code around
src/HOL/ATP.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_waldmeister.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML
     1.1 --- a/src/HOL/ATP.thy	Mon Jun 16 19:39:41 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Jun 16 19:40:04 2014 +0200
     1.3 @@ -129,12 +129,21 @@
     1.4  unfolding fFalse_def fTrue_def fequal_def by auto
     1.5  
     1.6  
     1.7 +subsection {* Waldmeister helpers *}
     1.8 +
     1.9 +(* Has all needed simplification lemmas for logic.
    1.10 +   "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
    1.11 +lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
    1.12 +  eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.13 +
    1.14 +
    1.15  subsection {* Setup *}
    1.16  
    1.17  ML_file "Tools/ATP/atp_problem_generate.ML"
    1.18  ML_file "Tools/ATP/atp_proof_reconstruct.ML"
    1.19  ML_file "Tools/ATP/atp_systems.ML"
    1.20 +ML_file "Tools/ATP/atp_waldmeister.ML"
    1.21  
    1.22 -setup ATP_Systems.setup
    1.23 +hide_fact (open) waldmeister_fol
    1.24  
    1.25  end
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Jun 16 19:39:41 2014 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Mon Jun 16 19:40:04 2014 +0200
     2.3 @@ -14,11 +14,6 @@
     2.4  lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
     2.5  by (erule contrapos_nn) (rule arg_cong)
     2.6  
     2.7 -(* Has all needed simplification lemmas for logic.
     2.8 -   "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
     2.9 -lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
    2.10 -  eq_ac disj_comms disj_assoc conj_comms conj_assoc
    2.11 -
    2.12  ML_file "Tools/Sledgehammer/async_manager.ML"
    2.13  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
    2.14  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
    2.15 @@ -32,13 +27,10 @@
    2.16  ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
    2.17  ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
    2.18  ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
    2.19 -ML_file "Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML"
    2.20  ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
    2.21  ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
    2.22  ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
    2.23  ML_file "Tools/Sledgehammer/sledgehammer.ML"
    2.24  ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
    2.25  
    2.26 -hide_fact (open) waldmeister_fol
    2.27 -
    2.28  end
     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:39:41 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:40:04 2014 +0200
     3.3 @@ -58,7 +58,6 @@
     3.4    val is_atp_installed : theory -> string -> bool
     3.5    val refresh_systems_on_tptp : unit -> unit
     3.6    val effective_term_order : Proof.context -> string -> term_order
     3.7 -  val setup : theory -> theory
     3.8  end;
     3.9  
    3.10  structure ATP_Systems : ATP_SYSTEMS =
    3.11 @@ -799,6 +798,6 @@
    3.12     remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
    3.13     remote_spass_pirate, remote_waldmeister]
    3.14  
    3.15 -val setup = fold add_atp atps
    3.16 +val _ = Theory.setup (fold add_atp atps)
    3.17  
    3.18  end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Mon Jun 16 19:40:04 2014 +0200
     4.3 @@ -0,0 +1,294 @@
     4.4 +(*  Title:      HOL/Tools/ATP/atp_waldmeister.ML
     4.5 +    Author:     Albert Steckermeier, TU Muenchen
     4.6 +    Author:     Jasmin Blanchette, TU Muenchen
     4.7 +
     4.8 +General-purpose functions used by the Sledgehammer modules.
     4.9 +*)
    4.10 +
    4.11 +signature ATP_WALDMEISTER =
    4.12 +sig
    4.13 +  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
    4.14 +  type atp_connective = ATP_Problem.atp_connective
    4.15 +  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
    4.16 +  type atp_format = ATP_Problem.atp_format
    4.17 +  type atp_formula_role = ATP_Problem.atp_formula_role
    4.18 +  type 'a atp_problem = 'a ATP_Problem.atp_problem
    4.19 +  type ('a, 'b) atp_step = ('a,'b) ATP_Proof.atp_step
    4.20 +
    4.21 +  val const_prefix : char
    4.22 +  val var_prefix : char
    4.23 +  val free_prefix : char
    4.24 +  val thm_prefix : string
    4.25 +  val hypothesis_prefix : string
    4.26 +  val thms_header : string
    4.27 +  val conjecture_condition_name : string
    4.28 +  val hypothesis_header : string
    4.29 +  val waldmeister_output_file_path : string
    4.30 +
    4.31 +  val waldmeister_simp_header : string
    4.32 +  val waldmeister_simp_thms : thm list
    4.33 +
    4.34 +  val thm_to_atps : bool -> thm -> (string * string, 'a) atp_term list
    4.35 +  val trm_to_atp : term -> (string * string, 'a) atp_term
    4.36 +  val atp_to_trm : (string, 'a) atp_term -> term
    4.37 +  val trm_to_atp_to_trm : term -> term
    4.38 +  val create_tptp_input : thm list -> term ->
    4.39 +    (string * ((string * string ATP_Problem.atp_problem_line list) list
    4.40 +      * (string Symtab.table * string Symtab.table) option)) option
    4.41 +  val run_waldmeister :
    4.42 +    string * (string ATP_Proof.atp_problem * (string Symtab.table * string Symtab.table) option)
    4.43 +    -> string ATP_Proof.atp_proof
    4.44 +  val atp_proof_step_to_term :
    4.45 +    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step
    4.46 +    -> (term,string) atp_step
    4.47 +  val fix_waldmeister_proof :
    4.48 +    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list ->
    4.49 +    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list
    4.50 +end;
    4.51 +
    4.52 +structure ATP_Waldmeister : ATP_WALDMEISTER =
    4.53 +struct
    4.54 +
    4.55 +open ATP_Problem
    4.56 +open ATP_Problem_Generate
    4.57 +open ATP_Proof
    4.58 +open ATP_Proof_Reconstruct
    4.59 +
    4.60 +type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
    4.61 +type atp_connective = ATP_Problem.atp_connective
    4.62 +type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
    4.63 +type atp_format = ATP_Problem.atp_format
    4.64 +type atp_formula_role = ATP_Problem.atp_formula_role
    4.65 +type 'a atp_problem = 'a ATP_Problem.atp_problem
    4.66 +
    4.67 +val const_prefix = #"c"
    4.68 +val var_prefix = #"V"
    4.69 +val free_prefix = #"f"
    4.70 +val thm_prefix = "fact"
    4.71 +val hypothesis_prefix = "hypothesis"
    4.72 +val thms_header = "facts"
    4.73 +val conjecture_condition_name = "condition"
    4.74 +val hypothesis_header = "hypothesis"
    4.75 +val broken_waldmeister_formula_prefix = #"1"
    4.76 +
    4.77 +val waldmeister_simp_header = "Waldmeister first order logic facts"
    4.78 +val waldmeister_simp_thms = @{thms waldmeister_fol}
    4.79 +
    4.80 +val temp_files_dir = "/home/albert/waldmeister"
    4.81 +val input_file_name = "input.tptp"
    4.82 +val output_file_name = "output.tptp"
    4.83 +val waldmeister_input_file_path = temp_files_dir ^ "/" ^ input_file_name
    4.84 +val waldmeister_output_file_path = temp_files_dir ^ "/" ^ output_file_name
    4.85 +val script_path = "/opt/Isabelle/src/HOL/Tools/ATP/scripts/remote_atp -s Waldmeister---710 -t 30"
    4.86 +
    4.87 +exception Failure
    4.88 +exception FailureMessage of string
    4.89 +
    4.90 +(*
    4.91 +Some utilitary functions for translation.
    4.92 +*)
    4.93 +
    4.94 +fun is_eq (Const (@{const_name "HOL.eq"}, _) $ _ $ _) = true
    4.95 +  | is_eq _ = false
    4.96 +
    4.97 +fun is_eq_thm thm = thm |> Thm.prop_of |> Object_Logic.atomize_term @{theory } |> is_eq
    4.98 +
    4.99 +fun gen_ascii_tuple str = (str, ascii_of str)
   4.100 +
   4.101 +(*
   4.102 +Translation from Isabelle theorms and terms to ATP terms.
   4.103 +*)
   4.104 +
   4.105 +fun trm_to_atp'' (Const (x, _)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x), []), args)]
   4.106 +  | trm_to_atp'' (Free (x, _)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), [])::args
   4.107 +  | trm_to_atp'' (Var ((x, _), _)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), [])::args
   4.108 +  | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args)
   4.109 +  | trm_to_atp'' _ args = args
   4.110 +
   4.111 +fun trm_to_atp' trm = trm_to_atp'' trm [] |> hd
   4.112 +
   4.113 +fun eq_trm_to_atp (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =
   4.114 +  ATerm (((tptp_equal, tptp_equal), []), [trm_to_atp' lhs, trm_to_atp' rhs])
   4.115 +  | eq_trm_to_atp _ = raise Failure
   4.116 +
   4.117 +fun trm_to_atp trm =
   4.118 +  if is_eq trm then
   4.119 +    eq_trm_to_atp trm
   4.120 +  else
   4.121 +    HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
   4.122 +
   4.123 +fun thm_to_atps split_conj thm =
   4.124 +  let
   4.125 +    val prop_term = Thm.prop_of thm |> Object_Logic.atomize_term @{theory}
   4.126 +  in
   4.127 +    if split_conj then
   4.128 +      map trm_to_atp (prop_term |> HOLogic.dest_conj)
   4.129 +    else
   4.130 +      [prop_term |> trm_to_atp]
   4.131 +  end
   4.132 +
   4.133 +fun prepare_conjecture conj_term =
   4.134 +  let
   4.135 +    fun split_conj_trm (Const (@{const_name Pure.imp}, _)$ condition $ consequence) =
   4.136 +        (SOME condition, consequence)
   4.137 +      | split_conj_trm conj = (NONE, conj)
   4.138 +    val (condition, consequence) = split_conj_trm conj_term
   4.139 +  in
   4.140 +    (case condition of SOME x => HOLogic.dest_conj x |> map trm_to_atp | NONE => []
   4.141 +    , trm_to_atp consequence)
   4.142 +  end
   4.143 +
   4.144 +(* Translation from ATP terms to Isabelle terms. *)
   4.145 +
   4.146 +fun construct_term (ATerm ((name, _), _)) =
   4.147 +  let
   4.148 +    val prefix = String.sub (name, 0)
   4.149 +  in
   4.150 +    if prefix = const_prefix then
   4.151 +      Const (String.extract (name, 1, NONE), Type ("", []))
   4.152 +    else if prefix = free_prefix then
   4.153 +      Free (String.extract (name, 1, NONE), TFree ("", []))
   4.154 +    else if Char.isUpper prefix then
   4.155 +      Var ((name, 0), TVar (("", 0), []))
   4.156 +    else
   4.157 +      raise Failure
   4.158 +  end
   4.159 +  | construct_term _ = raise Failure
   4.160 +
   4.161 +fun atp_to_trm' (ATerm (descr, args)) =
   4.162 +    (case args of
   4.163 +      [] => construct_term (ATerm (descr, args))
   4.164 +     | _ => Term.list_comb (construct_term (ATerm (descr, args)), map atp_to_trm' args))
   4.165 +     | atp_to_trm' _ = raise Failure
   4.166 +
   4.167 +fun atp_to_trm  (ATerm (("equal", _), [lhs, rhs])) =
   4.168 +    Const (@{const_name HOL.eq}, Type ("", [])) $ atp_to_trm' lhs $ atp_to_trm' rhs
   4.169 +  | atp_to_trm (ATerm (("$true", _), _)) = Const ("HOL.True", Type ("", []))
   4.170 +  | atp_to_trm _ = raise Failure
   4.171 +
   4.172 +fun formula_to_trm (AAtom aterm) = atp_to_trm aterm
   4.173 +  | formula_to_trm (AConn (ANot, [aterm])) =
   4.174 +    Const (@{const_name HOL.Not}, @{typ "bool \<Rightarrow> bool"}) $ formula_to_trm aterm
   4.175 +  | formula_to_trm _ = raise Failure
   4.176 +
   4.177 +(* Simple testing function for translation *)
   4.178 +
   4.179 +fun atp_only_readable_names (ATerm ((("=", _), ty), args)) =
   4.180 +    ATerm (("equal", ty), map atp_only_readable_names args)
   4.181 +  | atp_only_readable_names (ATerm (((descr, _), ty), args)) =
   4.182 +    ATerm ((descr, ty), map atp_only_readable_names args)
   4.183 +  | atp_only_readable_names _ = raise Failure
   4.184 +
   4.185 +val trm_to_atp_to_trm = eq_trm_to_atp #> atp_only_readable_names #> atp_to_trm
   4.186 +
   4.187 +(* Abstract translation from here on. *)
   4.188 +
   4.189 +fun name_of_thm thm =
   4.190 +  Thm.get_tags thm
   4.191 +  |> List.find (fn (x, _) => x = "name")
   4.192 +  |> the |> snd
   4.193 +
   4.194 +fun mk_formula prefix_name name atype aterm =
   4.195 +  Formula ((prefix_name ^ "_" ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
   4.196 +
   4.197 +fun thms_to_problem_lines [] = []
   4.198 +  | thms_to_problem_lines (t::thms) =
   4.199 +    (thm_to_atps false t |>
   4.200 +      map (mk_formula thm_prefix (name_of_thm t) Axiom)) @ thms_to_problem_lines thms
   4.201 +
   4.202 +fun make_nice problem = nice_atp_problem true CNF problem
   4.203 +
   4.204 +fun problem_to_string [] = ""
   4.205 +  | problem_to_string ((kind, lines)::problems) =
   4.206 +    "% " ^ kind ^ "\n"
   4.207 +    ^ String.concat (map (tptp_string_of_line CNF) lines)
   4.208 +    ^ "\n"
   4.209 +    ^ problem_to_string problems
   4.210 +
   4.211 +fun mk_conjecture aterm =
   4.212 +  let
   4.213 +    val formula = mk_anot (AAtom aterm)
   4.214 +  in
   4.215 +    Formula (gen_ascii_tuple hypothesis_prefix, Hypothesis, formula, NONE, [])
   4.216 +  end
   4.217 +
   4.218 +fun mk_condition_lines [] = []
   4.219 +  | mk_condition_lines (term::terms) =
   4.220 +    mk_formula thm_prefix conjecture_condition_name Axiom term::mk_condition_lines terms
   4.221 +
   4.222 +fun create_tptp_input thms conj_t =
   4.223 +    let
   4.224 +      val (conditions, consequence) = prepare_conjecture conj_t
   4.225 +      val thms_lines = thms_to_problem_lines thms
   4.226 +      val condition_lines = mk_condition_lines conditions
   4.227 +      val axiom_lines = thms_lines @ condition_lines
   4.228 +      val conj_line = consequence |> mk_conjecture
   4.229 +      val waldmeister_simp_lines =
   4.230 +        if List.exists (fn x => not (is_eq_thm x)) thms orelse not (is_eq conj_t) then
   4.231 +          [(waldmeister_simp_header, thms_to_problem_lines waldmeister_simp_thms)]
   4.232 +        else
   4.233 +          []
   4.234 +      val problem =
   4.235 +        waldmeister_simp_lines @ [(thms_header, axiom_lines), (hypothesis_header, [conj_line])]
   4.236 +      val (problem_nice, symtabs) = make_nice problem
   4.237 +    in
   4.238 +      SOME (problem_to_string problem_nice, (problem_nice, symtabs))
   4.239 +    end
   4.240 +
   4.241 +val waldmeister_proof_delims =
   4.242 +  [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
   4.243 +val known_waldmeister_failures = [(OutOfResources, "Too many function symbols"),
   4.244 +     (Inappropriate, "****  Unexpected end of file."),
   4.245 +     (Crashed, "Unrecoverable Segmentation Fault")]
   4.246 +
   4.247 +fun extract_proof_part output =
   4.248 +  case
   4.249 +    extract_tstplike_proof_and_outcome true
   4.250 +      waldmeister_proof_delims known_waldmeister_failures output of
   4.251 +    (x, NONE) => x | (_, SOME y) => raise FailureMessage (string_of_atp_failure y)
   4.252 +
   4.253 +fun cleanup () =
   4.254 +  (OS.Process.system ("rm " ^ waldmeister_input_file_path);
   4.255 +   OS.Process.system ("rm " ^ waldmeister_output_file_path))
   4.256 +
   4.257 +fun run_script input =
   4.258 +  let
   4.259 +    val outputFile = TextIO.openOut waldmeister_input_file_path
   4.260 +  in
   4.261 +    (TextIO.output (outputFile, input);
   4.262 +    TextIO.flushOut outputFile;
   4.263 +    TextIO.closeOut outputFile;
   4.264 +    OS.Process.system (script_path ^ " " ^ waldmeister_input_file_path ^ " > " ^
   4.265 +      waldmeister_output_file_path))
   4.266 +  end
   4.267 +
   4.268 +fun read_result () =
   4.269 +  let
   4.270 +    val inputFile = TextIO.openIn waldmeister_output_file_path
   4.271 +    fun readAllLines is =
   4.272 +      if TextIO.endOfStream is then (TextIO.closeIn is; [])
   4.273 +      else (TextIO.inputLine is |> the) :: readAllLines is
   4.274 +  in
   4.275 +    readAllLines inputFile |> String.concat
   4.276 +  end
   4.277 +
   4.278 +fun run_waldmeister (input, (problem, SOME (_, nice_to_nasty_table))) =
   4.279 +    (cleanup ();
   4.280 +     run_script input;
   4.281 +     read_result ()
   4.282 +     |> extract_proof_part
   4.283 +     |> atp_proof_of_tstplike_proof waldmeister_newN problem
   4.284 +     |> nasty_atp_proof nice_to_nasty_table)
   4.285 +  | run_waldmeister _ = raise Failure
   4.286 +
   4.287 +fun atp_proof_step_to_term (name, role, formula, formula_name, step_names) =
   4.288 +  (name, role, formula_to_trm formula, formula_name, step_names)
   4.289 +
   4.290 +fun fix_waldmeister_proof [] = []
   4.291 +  | fix_waldmeister_proof (((name, extra_names), role, formula, formula_name, step_names)::steps) =
   4.292 +    if String.sub (name, 0) = broken_waldmeister_formula_prefix then
   4.293 +      ((name, extra_names), role, mk_anot formula, formula_name, step_names)::fix_waldmeister_proof steps
   4.294 +    else
   4.295 +      ((name, extra_names), role, formula, formula_name, step_names)::fix_waldmeister_proof steps
   4.296 +
   4.297 +end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 16 19:39:41 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 16 19:40:04 2014 +0200
     5.3 @@ -226,8 +226,7 @@
     5.4          val reserved = reserved_isar_keyword_table ()
     5.5          val css = clasimpset_rule_table_of ctxt
     5.6          val all_facts =
     5.7 -          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
     5.8 -                           concl_t
     5.9 +          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t
    5.10          val _ = () |> not blocking ? kill_provers
    5.11          val _ =
    5.12            (case find_first (not o is_prover_supported ctxt) provers of
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML	Mon Jun 16 19:39:41 2014 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,294 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML
     6.5 -    Author:     Albert Steckermeier, TU Muenchen
     6.6 -    Author:     Jasmin Blanchette, TU Muenchen
     6.7 -
     6.8 -General-purpose functions used by the Sledgehammer modules.
     6.9 -*)
    6.10 -
    6.11 -signature SLEDGEHAMMER_PROVER_WALDMEISTER =
    6.12 -sig
    6.13 -  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
    6.14 -  type atp_connective = ATP_Problem.atp_connective
    6.15 -  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
    6.16 -  type atp_format = ATP_Problem.atp_format
    6.17 -  type atp_formula_role = ATP_Problem.atp_formula_role
    6.18 -  type 'a atp_problem = 'a ATP_Problem.atp_problem
    6.19 -  type ('a, 'b) atp_step = ('a,'b) ATP_Proof.atp_step
    6.20 -
    6.21 -  val const_prefix : char
    6.22 -  val var_prefix : char
    6.23 -  val free_prefix : char
    6.24 -  val thm_prefix : string
    6.25 -  val hypothesis_prefix : string
    6.26 -  val thms_header : string
    6.27 -  val conjecture_condition_name : string
    6.28 -  val hypothesis_header : string
    6.29 -  val waldmeister_output_file_path : string
    6.30 -
    6.31 -  val waldmeister_simp_header : string
    6.32 -  val waldmeister_simp_thms : thm list
    6.33 -
    6.34 -  val thm_to_atps : bool -> thm -> (string * string, 'a) atp_term list
    6.35 -  val trm_to_atp : term -> (string * string, 'a) atp_term
    6.36 -  val atp_to_trm : (string, 'a) atp_term -> term
    6.37 -  val trm_to_atp_to_trm : term -> term
    6.38 -  val create_tptp_input : thm list -> term ->
    6.39 -    (string * ((string * string ATP_Problem.atp_problem_line list) list
    6.40 -      * (string Symtab.table * string Symtab.table) option)) option
    6.41 -  val run_waldmeister :
    6.42 -    string * (string ATP_Proof.atp_problem * (string Symtab.table * string Symtab.table) option)
    6.43 -    -> string ATP_Proof.atp_proof
    6.44 -  val atp_proof_step_to_term :
    6.45 -    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step
    6.46 -    -> (term,string) atp_step
    6.47 -  val fix_waldmeister_proof :
    6.48 -    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list ->
    6.49 -    ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list
    6.50 -end;
    6.51 -
    6.52 -structure Sledgehammer_Prover_Waldmeister : SLEDGEHAMMER_PROVER_WALDMEISTER =
    6.53 -struct
    6.54 -
    6.55 -open ATP_Problem
    6.56 -open ATP_Problem_Generate
    6.57 -open ATP_Proof
    6.58 -open ATP_Proof_Reconstruct
    6.59 -
    6.60 -type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
    6.61 -type atp_connective = ATP_Problem.atp_connective
    6.62 -type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
    6.63 -type atp_format = ATP_Problem.atp_format
    6.64 -type atp_formula_role = ATP_Problem.atp_formula_role
    6.65 -type 'a atp_problem = 'a ATP_Problem.atp_problem
    6.66 -
    6.67 -val const_prefix = #"c"
    6.68 -val var_prefix = #"V"
    6.69 -val free_prefix = #"f"
    6.70 -val thm_prefix = "fact"
    6.71 -val hypothesis_prefix = "hypothesis"
    6.72 -val thms_header = "facts"
    6.73 -val conjecture_condition_name = "condition"
    6.74 -val hypothesis_header = "hypothesis"
    6.75 -val broken_waldmeister_formula_prefix = #"1"
    6.76 -
    6.77 -val waldmeister_simp_header = "Waldmeister first order logic facts"
    6.78 -val waldmeister_simp_thms = @{thms waldmeister_fol}
    6.79 -
    6.80 -val temp_files_dir = "/home/albert/waldmeister"
    6.81 -val input_file_name = "input.tptp"
    6.82 -val output_file_name = "output.tptp"
    6.83 -val waldmeister_input_file_path = temp_files_dir ^ "/" ^ input_file_name
    6.84 -val waldmeister_output_file_path = temp_files_dir ^ "/" ^ output_file_name
    6.85 -val script_path = "/opt/Isabelle/src/HOL/Tools/ATP/scripts/remote_atp -s Waldmeister---710 -t 30"
    6.86 -
    6.87 -exception Failure
    6.88 -exception FailureMessage of string
    6.89 -
    6.90 -(*
    6.91 -Some utilitary functions for translation.
    6.92 -*)
    6.93 -
    6.94 -fun is_eq (Const (@{const_name "HOL.eq"}, _) $ _ $ _) = true
    6.95 -  | is_eq _ = false
    6.96 -
    6.97 -fun is_eq_thm thm = thm |> Thm.prop_of |> Object_Logic.atomize_term @{theory } |> is_eq
    6.98 -
    6.99 -fun gen_ascii_tuple str = (str, ascii_of str)
   6.100 -
   6.101 -(*
   6.102 -Translation from Isabelle theorms and terms to ATP terms.
   6.103 -*)
   6.104 -
   6.105 -fun trm_to_atp'' (Const (x, _)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x), []), args)]
   6.106 -  | trm_to_atp'' (Free (x, _)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), [])::args
   6.107 -  | trm_to_atp'' (Var ((x, _), _)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), [])::args
   6.108 -  | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args)
   6.109 -  | trm_to_atp'' _ args = args
   6.110 -
   6.111 -fun trm_to_atp' trm = trm_to_atp'' trm [] |> hd
   6.112 -
   6.113 -fun eq_trm_to_atp (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =
   6.114 -  ATerm (((tptp_equal, tptp_equal), []), [trm_to_atp' lhs, trm_to_atp' rhs])
   6.115 -  | eq_trm_to_atp _ = raise Failure
   6.116 -
   6.117 -fun trm_to_atp trm =
   6.118 -  if is_eq trm then
   6.119 -    eq_trm_to_atp trm
   6.120 -  else
   6.121 -    HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
   6.122 -
   6.123 -fun thm_to_atps split_conj thm =
   6.124 -  let
   6.125 -    val prop_term = Thm.prop_of thm |> Object_Logic.atomize_term @{theory}
   6.126 -  in
   6.127 -    if split_conj then
   6.128 -      map trm_to_atp (prop_term |> HOLogic.dest_conj)
   6.129 -    else
   6.130 -      [prop_term |> trm_to_atp]
   6.131 -  end
   6.132 -
   6.133 -fun prepare_conjecture conj_term =
   6.134 -  let
   6.135 -    fun split_conj_trm (Const (@{const_name Pure.imp}, _)$ condition $ consequence) =
   6.136 -        (SOME condition, consequence)
   6.137 -      | split_conj_trm conj = (NONE, conj)
   6.138 -    val (condition, consequence) = split_conj_trm conj_term
   6.139 -  in
   6.140 -    (case condition of SOME x => HOLogic.dest_conj x |> map trm_to_atp | NONE => []
   6.141 -    , trm_to_atp consequence)
   6.142 -  end
   6.143 -
   6.144 -(* Translation from ATP terms to Isabelle terms. *)
   6.145 -
   6.146 -fun construct_term (ATerm ((name, _), _)) =
   6.147 -  let
   6.148 -    val prefix = String.sub (name, 0)
   6.149 -  in
   6.150 -    if prefix = const_prefix then
   6.151 -      Const (String.extract (name, 1, NONE), Type ("", []))
   6.152 -    else if prefix = free_prefix then
   6.153 -      Free (String.extract (name, 1, NONE), TFree ("", []))
   6.154 -    else if Char.isUpper prefix then
   6.155 -      Var ((name, 0), TVar (("", 0), []))
   6.156 -    else
   6.157 -      raise Failure
   6.158 -  end
   6.159 -  | construct_term _ = raise Failure
   6.160 -
   6.161 -fun atp_to_trm' (ATerm (descr, args)) =
   6.162 -    (case args of
   6.163 -      [] => construct_term (ATerm (descr, args))
   6.164 -     | _ => Term.list_comb (construct_term (ATerm (descr, args)), map atp_to_trm' args))
   6.165 -     | atp_to_trm' _ = raise Failure
   6.166 -
   6.167 -fun atp_to_trm  (ATerm (("equal", _), [lhs, rhs])) =
   6.168 -    Const (@{const_name HOL.eq}, Type ("", [])) $ atp_to_trm' lhs $ atp_to_trm' rhs
   6.169 -  | atp_to_trm (ATerm (("$true", _), _)) = Const ("HOL.True", Type ("", []))
   6.170 -  | atp_to_trm _ = raise Failure
   6.171 -
   6.172 -fun formula_to_trm (AAtom aterm) = atp_to_trm aterm
   6.173 -  | formula_to_trm (AConn (ANot, [aterm])) =
   6.174 -    Const (@{const_name HOL.Not}, @{typ "bool \<Rightarrow> bool"}) $ formula_to_trm aterm
   6.175 -  | formula_to_trm _ = raise Failure
   6.176 -
   6.177 -(* Simple testing function for translation *)
   6.178 -
   6.179 -fun atp_only_readable_names (ATerm ((("=", _), ty), args)) =
   6.180 -    ATerm (("equal", ty), map atp_only_readable_names args)
   6.181 -  | atp_only_readable_names (ATerm (((descr, _), ty), args)) =
   6.182 -    ATerm ((descr, ty), map atp_only_readable_names args)
   6.183 -  | atp_only_readable_names _ = raise Failure
   6.184 -
   6.185 -val trm_to_atp_to_trm = eq_trm_to_atp #> atp_only_readable_names #> atp_to_trm
   6.186 -
   6.187 -(* Abstract translation from here on. *)
   6.188 -
   6.189 -fun name_of_thm thm =
   6.190 -  Thm.get_tags thm
   6.191 -  |> List.find (fn (x, _) => x = "name")
   6.192 -  |> the |> snd
   6.193 -
   6.194 -fun mk_formula prefix_name name atype aterm =
   6.195 -  Formula ((prefix_name ^ "_" ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
   6.196 -
   6.197 -fun thms_to_problem_lines [] = []
   6.198 -  | thms_to_problem_lines (t::thms) =
   6.199 -    (thm_to_atps false t |>
   6.200 -      map (mk_formula thm_prefix (name_of_thm t) Axiom)) @ thms_to_problem_lines thms
   6.201 -
   6.202 -fun make_nice problem = nice_atp_problem true CNF problem
   6.203 -
   6.204 -fun problem_to_string [] = ""
   6.205 -  | problem_to_string ((kind, lines)::problems) =
   6.206 -    "% " ^ kind ^ "\n"
   6.207 -    ^ String.concat (map (tptp_string_of_line CNF) lines)
   6.208 -    ^ "\n"
   6.209 -    ^ problem_to_string problems
   6.210 -
   6.211 -fun mk_conjecture aterm =
   6.212 -  let
   6.213 -    val formula = mk_anot (AAtom aterm)
   6.214 -  in
   6.215 -    Formula (gen_ascii_tuple hypothesis_prefix, Hypothesis, formula, NONE, [])
   6.216 -  end
   6.217 -
   6.218 -fun mk_condition_lines [] = []
   6.219 -  | mk_condition_lines (term::terms) =
   6.220 -    mk_formula thm_prefix conjecture_condition_name Axiom term::mk_condition_lines terms
   6.221 -
   6.222 -fun create_tptp_input thms conj_t =
   6.223 -    let
   6.224 -      val (conditions, consequence) = prepare_conjecture conj_t
   6.225 -      val thms_lines = thms_to_problem_lines thms
   6.226 -      val condition_lines = mk_condition_lines conditions
   6.227 -      val axiom_lines = thms_lines @ condition_lines
   6.228 -      val conj_line = consequence |> mk_conjecture
   6.229 -      val waldmeister_simp_lines =
   6.230 -        if List.exists (fn x => not (is_eq_thm x)) thms orelse not (is_eq conj_t) then
   6.231 -          [(waldmeister_simp_header, thms_to_problem_lines waldmeister_simp_thms)]
   6.232 -        else
   6.233 -          []
   6.234 -      val problem =
   6.235 -        waldmeister_simp_lines @ [(thms_header, axiom_lines), (hypothesis_header, [conj_line])]
   6.236 -      val (problem_nice, symtabs) = make_nice problem
   6.237 -    in
   6.238 -      SOME (problem_to_string problem_nice, (problem_nice, symtabs))
   6.239 -    end
   6.240 -
   6.241 -val waldmeister_proof_delims =
   6.242 -  [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
   6.243 -val known_waldmeister_failures = [(OutOfResources, "Too many function symbols"),
   6.244 -     (Inappropriate, "****  Unexpected end of file."),
   6.245 -     (Crashed, "Unrecoverable Segmentation Fault")]
   6.246 -
   6.247 -fun extract_proof_part output =
   6.248 -  case
   6.249 -    extract_tstplike_proof_and_outcome true
   6.250 -      waldmeister_proof_delims known_waldmeister_failures output of
   6.251 -    (x, NONE) => x | (_, SOME y) => raise FailureMessage (string_of_atp_failure y)
   6.252 -
   6.253 -fun cleanup () =
   6.254 -  (OS.Process.system ("rm " ^ waldmeister_input_file_path);
   6.255 -   OS.Process.system ("rm " ^ waldmeister_output_file_path))
   6.256 -
   6.257 -fun run_script input =
   6.258 -  let
   6.259 -    val outputFile = TextIO.openOut waldmeister_input_file_path
   6.260 -  in
   6.261 -    (TextIO.output (outputFile, input);
   6.262 -    TextIO.flushOut outputFile;
   6.263 -    TextIO.closeOut outputFile;
   6.264 -    OS.Process.system (script_path ^ " " ^ waldmeister_input_file_path ^ " > " ^
   6.265 -      waldmeister_output_file_path))
   6.266 -  end
   6.267 -
   6.268 -fun read_result () =
   6.269 -  let
   6.270 -    val inputFile = TextIO.openIn waldmeister_output_file_path
   6.271 -    fun readAllLines is =
   6.272 -      if TextIO.endOfStream is then (TextIO.closeIn is; [])
   6.273 -      else (TextIO.inputLine is |> the) :: readAllLines is
   6.274 -  in
   6.275 -    readAllLines inputFile |> String.concat
   6.276 -  end
   6.277 -
   6.278 -fun run_waldmeister (input, (problem, SOME (_, nice_to_nasty_table))) =
   6.279 -    (cleanup ();
   6.280 -     run_script input;
   6.281 -     read_result ()
   6.282 -     |> extract_proof_part
   6.283 -     |> atp_proof_of_tstplike_proof waldmeister_newN problem
   6.284 -     |> nasty_atp_proof nice_to_nasty_table)
   6.285 -  | run_waldmeister _ = raise Failure
   6.286 -
   6.287 -fun atp_proof_step_to_term (name, role, formula, formula_name, step_names) =
   6.288 -  (name, role, formula_to_trm formula, formula_name, step_names)
   6.289 -
   6.290 -fun fix_waldmeister_proof [] = []
   6.291 -  | fix_waldmeister_proof (((name, extra_names), role, formula, formula_name, step_names)::steps) =
   6.292 -    if String.sub (name, 0) = broken_waldmeister_formula_prefix then
   6.293 -      ((name, extra_names), role, mk_anot formula, formula_name, step_names)::fix_waldmeister_proof steps
   6.294 -    else
   6.295 -      ((name, extra_names), role, formula, formula_name, step_names)::fix_waldmeister_proof steps
   6.296 -
   6.297 -end;