# HG changeset patch # User blanchet # Date 1386946479 -28800 # Node ID 05c9f3d84ba35588bca846727c0d76f8bf5f1f17 # Parent b91afc3aa3e6d58e3fee6847a44b5a8c26b60edb made SML/NJ happy + whitespace tuning diff -r b91afc3aa3e6 -r 05c9f3d84ba3 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Dec 13 12:31:45 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Dec 13 22:54:39 2013 +0800 @@ -79,6 +79,7 @@ #> Atom_Graph.default_node (to, ()) #> Atom_Graph.add_edge_acyclic (from, to) fun add_infer (froms, to) = fold (add_edge to) froms + val graph = fold add_infer infers Atom_Graph.empty val reachable = Atom_Graph.all_preds graph [bot] in @@ -88,8 +89,7 @@ fun axioms_of_refute_graph refute_graph conjs = subtract atom_eq conjs (Atom_Graph.minimals refute_graph) -fun tainted_atoms_of_refute_graph refute_graph = - Atom_Graph.all_succs refute_graph +fun tainted_atoms_of_refute_graph refute_graph = Atom_Graph.all_succs refute_graph fun sequents_of_refute_graph refute_graph = Atom_Graph.keys refute_graph @@ -101,7 +101,8 @@ fun string_of_sequent (gamma, c) = string_of_context gamma ^ " \ " ^ Atom.string_of c -val string_of_refute_graph = sequents_of_refute_graph #> map string_of_sequent #> cat_lines +fun string_of_refute_graph refute_graph = + refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines fun redirect_sequent tainted bot (gamma, c) = if member atom_eq tainted c then @@ -117,7 +118,9 @@ #> Atom_Graph.default_node (to, ()) #> Atom_Graph.add_edge_acyclic (from, to) fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma - in Atom_Graph.empty |> fold add_seq seqs end + in + fold add_seq seqs Atom_Graph.empty + end fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord @@ -143,9 +146,9 @@ fun redirect_graph axioms tainted bot refute_graph = let - val seqs = - map (redirect_sequent tainted bot) (sequents_of_refute_graph refute_graph) + val seqs = map (redirect_sequent tainted bot) (sequents_of_refute_graph refute_graph) val direct_graph = direct_graph seqs + fun redirect c proved seqs = if null seqs then [] @@ -173,7 +176,9 @@ in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end - in redirect [] axioms seqs end + in + redirect [] axioms seqs + end fun indent 0 = "" | indent n = " " ^ indent (n - 1) @@ -193,8 +198,7 @@ indent depth ^ string_of_rich_sequent "\" seq | string_of_inference depth (Cases cases) = indent depth ^ "[\n" ^ - space_implode ("\n" ^ indent depth ^ "|\n") - (map (string_of_case depth) cases) ^ "\n" ^ + space_implode ("\n" ^ indent depth ^ "|\n") (map (string_of_case depth) cases) ^ "\n" ^ indent depth ^ "]" and string_of_subproof depth = cat_lines o map (string_of_inference depth)