# HG changeset patch
# User boehmes
# Date 1258121428 -3600
# Node ID 7be6ee4ee67f53a9ae7af3c42291558b14394369
# Parent  31a129cc0d10bd4f76cd93fdaa6b5937575390a7
parallel solving of Boogie splinters

diff -r 31a129cc0d10 -r 7be6ee4ee67f src/HOL/Boogie/Tools/boogie_split.ML
--- a/src/HOL/Boogie/Tools/boogie_split.ML	Fri Nov 13 15:06:19 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML	Fri Nov 13 15:10:28 2009 +0100
@@ -114,12 +114,15 @@
 local
   val split_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
 
-  fun prep_tac ctxt args facts =
+  fun ALL_GOALS false tac = ALLGOALS tac
+    | ALL_GOALS true tac = PARALLEL_GOALS (HEADGOAL tac)
+
+  fun prep_tac ctxt ((parallel, verbose), subs) facts =
     HEADGOAL (Method.insert_tac facts)
     THEN HEADGOAL (REPEAT_ALL_NEW (Tactic.resolve_tac split_rules))
     THEN unique_case_names (ProofContext.theory_of ctxt)
-    THEN ALLGOALS (SUBGOAL (fn (t, i) =>
-      TRY (sub_tactics_tac ctxt args (case_name_of t) i)))
+    THEN ALL_GOALS parallel (SUBGOAL (fn (t, i) =>
+      TRY (sub_tactics_tac ctxt (verbose, subs) (case_name_of t) i)))
 
   val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
     (Conv.rewr_conv (as_meta_eq @{thm assert_at_def}))))
@@ -136,12 +139,14 @@
           (ProofContext.theory_of ctxt, Thm.prop_of st) names)
         Tactical.all_tac st))
 
-  val verbose_opt = Args.parens (Args.$$$ "verbose") >> K true
+  val options =
+    Args.parens (Args.$$$ "verbose") >> K (false, true) ||
+    Args.parens (Args.$$$ "fast_verbose") >> K (true, true)
   val sub_tactics = Args.$$$ "try" -- Args.colon |-- Scan.repeat1 Args.name
 in
 val setup_split_vc = Method.setup @{binding split_vc}
-  (Scan.lift (Scan.optional verbose_opt false -- Scan.optional sub_tactics [])
-    >> split_vc)
+  (Scan.lift (Scan.optional options (true, false) --
+    Scan.optional sub_tactics []) >> split_vc)
   ("Splits a Boogie-generated verification conditions into smaller problems" ^
    " and tries to solve the splinters with the supplied sub-tactics.")
 end