# HG changeset patch
# User steckerm
# Date 1402495330 -7200
# Node ID 159c18bbc879e74df7c529564693b944b7f74224
# Parent  6cd8566e938e3f124b3057658ba76f666fffdf7e
tuned whitespaces

diff -r 6cd8566e938e -r 159c18bbc879 src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML
--- 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;