--- a/src/HOL/ATP.thy Mon Jun 16 19:39:41 2014 +0200
+++ b/src/HOL/ATP.thy Mon Jun 16 19:40:04 2014 +0200
@@ -129,12 +129,21 @@
unfolding fFalse_def fTrue_def fequal_def by auto
+subsection {* Waldmeister helpers *}
+
+(* Has all needed simplification lemmas for logic.
+ "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
+lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
+ eq_ac disj_comms disj_assoc conj_comms conj_assoc
+
+
subsection {* Setup *}
ML_file "Tools/ATP/atp_problem_generate.ML"
ML_file "Tools/ATP/atp_proof_reconstruct.ML"
ML_file "Tools/ATP/atp_systems.ML"
+ML_file "Tools/ATP/atp_waldmeister.ML"
-setup ATP_Systems.setup
+hide_fact (open) waldmeister_fol
end
--- a/src/HOL/Sledgehammer.thy Mon Jun 16 19:39:41 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:04 2014 +0200
@@ -14,11 +14,6 @@
lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_nn) (rule arg_cong)
-(* Has all needed simplification lemmas for logic.
- "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
-lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
- eq_ac disj_comms disj_assoc conj_comms conj_assoc
-
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
@@ -32,13 +27,10 @@
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
ML_file "Tools/Sledgehammer/sledgehammer.ML"
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
-hide_fact (open) waldmeister_fol
-
end
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:39:41 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:40:04 2014 +0200
@@ -58,7 +58,6 @@
val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
val effective_term_order : Proof.context -> string -> term_order
- val setup : theory -> theory
end;
structure ATP_Systems : ATP_SYSTEMS =
@@ -799,6 +798,6 @@
remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
remote_spass_pirate, remote_waldmeister]
-val setup = fold add_atp atps
+val _ = Theory.setup (fold add_atp atps)
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Mon Jun 16 19:40:04 2014 +0200
@@ -0,0 +1,294 @@
+(* Title: HOL/Tools/ATP/atp_waldmeister.ML
+ Author: Albert Steckermeier, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+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
+
+ 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
+end;
+
+structure ATP_Waldmeister : ATP_WALDMEISTER =
+struct
+
+open ATP_Problem
+open ATP_Problem_Generate
+open ATP_Proof
+open ATP_Proof_Reconstruct
+
+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
+
+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"
+
+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.
+*)
+
+fun trm_to_atp'' (Const (x, _)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x), []), args)]
+ | trm_to_atp'' (Free (x, _)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), [])::args
+ | trm_to_atp'' (Var ((x, _), _)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), [])::args
+ | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args)
+ | 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])
+ | 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
+
+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 prepare_conjecture conj_term =
+ let
+ 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 => []
+ , trm_to_atp consequence)
+ end
+
+(* Translation from ATP terms to Isabelle terms. *)
+
+fun construct_term (ATerm ((name, _), _)) =
+ let
+ val prefix = String.sub (name, 0)
+ in
+ if prefix = const_prefix then
+ Const (String.extract (name, 1, NONE), Type ("", []))
+ else if prefix = free_prefix then
+ Free (String.extract (name, 1, NONE), TFree ("", []))
+ else if Char.isUpper prefix then
+ Var ((name, 0), TVar (("", 0), []))
+ else
+ raise Failure
+ end
+ | construct_term _ = raise Failure
+
+fun atp_to_trm' (ATerm (descr, args)) =
+ (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])) =
+ 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
+
+fun mk_formula prefix_name name atype aterm =
+ 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 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, [])
+ 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
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 16 19:39:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 16 19:40:04 2014 +0200
@@ -226,8 +226,7 @@
val reserved = reserved_isar_keyword_table ()
val css = clasimpset_rule_table_of ctxt
val all_facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
- concl_t
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t
val _ = () |> not blocking ? kill_provers
val _ =
(case find_first (not o is_prover_supported ctxt) provers of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML Mon Jun 16 19:39:41 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,294 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML
- Author: Albert Steckermeier, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-General-purpose functions used by the Sledgehammer modules.
-*)
-
-signature SLEDGEHAMMER_PROVER_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
-
- 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
-end;
-
-structure Sledgehammer_Prover_Waldmeister : SLEDGEHAMMER_PROVER_WALDMEISTER =
-struct
-
-open ATP_Problem
-open ATP_Problem_Generate
-open ATP_Proof
-open ATP_Proof_Reconstruct
-
-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
-
-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"
-
-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.
-*)
-
-fun trm_to_atp'' (Const (x, _)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x), []), args)]
- | trm_to_atp'' (Free (x, _)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), [])::args
- | trm_to_atp'' (Var ((x, _), _)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), [])::args
- | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args)
- | 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])
- | 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
-
-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 prepare_conjecture conj_term =
- let
- 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 => []
- , trm_to_atp consequence)
- end
-
-(* Translation from ATP terms to Isabelle terms. *)
-
-fun construct_term (ATerm ((name, _), _)) =
- let
- val prefix = String.sub (name, 0)
- in
- if prefix = const_prefix then
- Const (String.extract (name, 1, NONE), Type ("", []))
- else if prefix = free_prefix then
- Free (String.extract (name, 1, NONE), TFree ("", []))
- else if Char.isUpper prefix then
- Var ((name, 0), TVar (("", 0), []))
- else
- raise Failure
- end
- | construct_term _ = raise Failure
-
-fun atp_to_trm' (ATerm (descr, args)) =
- (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])) =
- 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
-
-fun mk_formula prefix_name name atype aterm =
- 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 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, [])
- 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
-
-end;