--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML Wed Jun 11 15:44:09 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML Wed Jun 11 16:02:10 2014 +0200
@@ -88,34 +88,34 @@
Some utilitary functions for translation.
*)
-fun is_eq (Const (@{const_name "HOL.eq"},_) $ _ $ _) = true
+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)
+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
+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])
+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
+ HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
fun thm_to_atps split_conj thm =
let
@@ -130,53 +130,53 @@
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
+ (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)
+ , trm_to_atp consequence)
end
(* Translation from ATP terms to Isabelle terms. *)
-fun construct_term (ATerm ((name,_),_)) =
+fun construct_term (ATerm ((name, _), _)) =
let
- val prefix = String.sub (name,0)
+ val prefix = String.sub (name, 0)
in
if prefix = const_prefix then
- Const (String.extract (name,1,NONE),Type ("",[]))
+ Const (String.extract (name, 1, NONE), Type ("", []))
else if prefix = free_prefix then
- Free (String.extract (name,1,NONE),TFree ("",[]))
+ Free (String.extract (name, 1, NONE), TFree ("", []))
else if Char.isUpper prefix then
- Var ((name,0),TVar (("",0),[]))
+ Var ((name, 0), TVar (("", 0), []))
else
raise Failure
end
| construct_term _ = raise Failure
-fun atp_to_trm' (ATerm (descr,args)) =
+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))
+ [] => 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 ("",[]))
+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 (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)
+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
@@ -185,11 +185,11 @@
fun name_of_thm thm =
Thm.get_tags thm
- |> List.find (fn (x,_) => x = "name")
+ |> 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,[])
+ Formula ((prefix_name ^ "_" ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
fun thms_to_problem_lines [] = []
| thms_to_problem_lines (t::thms) =
@@ -199,7 +199,7 @@
fun make_nice problem = nice_atp_problem true CNF problem
fun problem_to_string [] = ""
- | problem_to_string ((kind,lines)::problems) =
+ | problem_to_string ((kind, lines)::problems) =
"% " ^ kind ^ "\n"
^ String.concat (map (tptp_string_of_line CNF) lines)
^ "\n"
@@ -209,7 +209,7 @@
let
val formula = mk_anot (AAtom aterm)
in
- Formula (gen_ascii_tuple hypothesis_prefix,Hypothesis,formula, NONE,[])
+ Formula (gen_ascii_tuple hypothesis_prefix, Hypothesis, formula, NONE, [])
end
fun mk_condition_lines [] = []
@@ -218,21 +218,21 @@
fun create_tptp_input thms conj_t =
let
- val (conditions,consequence) = prepare_conjecture conj_t
+ 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)]
+ [(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
+ 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))
+ SOME (problem_to_string problem_nice, (problem_nice, symtabs))
end
val waldmeister_proof_delims =
@@ -245,7 +245,7 @@
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)
+ (x, NONE) => x | (_, SOME y) => raise FailureMessage (string_of_atp_failure y)
fun cleanup () =
(OS.Process.system ("rm " ^ waldmeister_input_file_path);
@@ -255,7 +255,7 @@
let
val outputFile = TextIO.openOut waldmeister_input_file_path
in
- (TextIO.output (outputFile,input);
+ (TextIO.output (outputFile, input);
TextIO.flushOut outputFile;
TextIO.closeOut outputFile;
OS.Process.system (script_path ^ " " ^ waldmeister_input_file_path ^ " > " ^
@@ -272,7 +272,7 @@
readAllLines inputFile |> String.concat
end
-fun run_waldmeister (input,(problem,SOME (_,nice_to_nasty_table))) =
+fun run_waldmeister (input, (problem, SOME (_, nice_to_nasty_table))) =
(cleanup ();
run_script input;
read_result ()
@@ -281,14 +281,14 @@
|> 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 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
+ | 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
+ ((name, extra_names), role, formula, formula_name, step_names)::fix_waldmeister_proof steps
end;