merged
authorwenzelm
Mon Mar 30 21:54:15 2009 +0200 (2009-03-30)
changeset 30803d9f4e7a59392
parent 30802 f9e9e800d27e
parent 30800 95cbadcd47fc
child 30804 dbdb74be8dde
child 30808 a3d9cad81ae5
merged
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Mon Mar 30 12:07:59 2009 -0700
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Mon Mar 30 21:54:15 2009 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    val kill: unit -> unit
     1.5    val info: unit -> unit
     1.6    val messages: int option -> unit
     1.7 -  type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string 
     1.8 +  type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
     1.9    val add_prover: string -> prover -> theory -> theory
    1.10    val print_provers: theory -> unit
    1.11    val sledgehammer: string list -> Proof.state -> unit
    1.12 @@ -96,6 +96,12 @@
    1.13    State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
    1.14      active = active, cancelling = cancelling, messages = messages, store = store};
    1.15  
    1.16 +fun empty_state state =
    1.17 +  let
    1.18 +    val State {active = active, cancelling = cancelling, messages = messages, ...} =
    1.19 +      Synchronized.value state
    1.20 +  in (null active) andalso (null cancelling) andalso (null messages) end;
    1.21 +
    1.22  val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
    1.23  
    1.24  
    1.25 @@ -127,7 +133,7 @@
    1.26              (if length store <= message_store_limit then store
    1.27               else #1 (chop message_store_limit store))
    1.28          in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
    1.29 -    | NONE =>state));
    1.30 +    | NONE => state));
    1.31  
    1.32  
    1.33  (* kill excessive atp threads *)
    1.34 @@ -162,12 +168,14 @@
    1.35  fun print_new_messages () =
    1.36    let val to_print = Synchronized.change_result state
    1.37      (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.38 -    (messages, make_state timeout_heap oldest_heap active cancelling [] store))  
    1.39 -  in if null to_print then ()
    1.40 -  else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end;
    1.41 +      (messages, make_state timeout_heap oldest_heap active cancelling [] store))
    1.42 +  in
    1.43 +    if null to_print then ()
    1.44 +    else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
    1.45 +  end;
    1.46  
    1.47  
    1.48 -(* start a watching thread which runs forever -- only one may exist *)
    1.49 +(* start a watching thread -- only one may exist *)
    1.50  
    1.51  fun check_thread_manager () = CRITICAL (fn () =>
    1.52    if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
    1.53 @@ -197,7 +205,7 @@
    1.54              in SOME (map #2 timeout_threads, state') end
    1.55          end
    1.56      in
    1.57 -      while true do
    1.58 +      while not (empty_state state) do
    1.59         (Synchronized.timed_access state time_limit action
    1.60          |> these
    1.61          |> List.app (unregister (false, "Interrupted (reached timeout)"));
    1.62 @@ -211,14 +219,14 @@
    1.63  (* thread is registered here by sledgehammer *)
    1.64  
    1.65  fun register birthtime deadtime (thread, desc) =
    1.66 - (check_thread_manager ();
    1.67 -  Synchronized.change state
    1.68 + (Synchronized.change state
    1.69      (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.70        let
    1.71          val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
    1.72          val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
    1.73          val active' = update_thread (thread, (birthtime, deadtime, desc)) active
    1.74 -      in make_state timeout_heap' oldest_heap' active' cancelling messages store end));
    1.75 +      in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
    1.76 +  check_thread_manager ());
    1.77  
    1.78  
    1.79  
    1.80 @@ -307,7 +315,7 @@
    1.81          val _ = SimpleThread.fork true (fn () =>
    1.82            let
    1.83              val _ = register birthtime deadtime (Thread.self (), desc)
    1.84 -            val result = prover (get_timeout ()) i (Proof.get_goal proof_state) 
    1.85 +            val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
    1.86                handle ResHolClause.TOO_TRIVIAL
    1.87                  => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
    1.88                | ERROR msg
    1.89 @@ -355,7 +363,7 @@
    1.90  val _ =
    1.91    OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
    1.92      (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
    1.93 -      Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
    1.94 +      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
    1.95  
    1.96  end;
    1.97  
     2.1 --- a/src/Pure/General/binding.ML	Mon Mar 30 12:07:59 2009 -0700
     2.2 +++ b/src/Pure/General/binding.ML	Mon Mar 30 21:54:15 2009 +0200
     2.3 @@ -84,8 +84,9 @@
     2.4        let val (qualifier, name) = split_last (Long_Name.explode s)
     2.5        in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
     2.6  
     2.7 -fun qualified_name_of (Binding {qualifier, name, ...}) =
     2.8 -  Long_Name.implode (map #1 qualifier @ [name]);
     2.9 +fun qualified_name_of (b as Binding {qualifier, name, ...}) =
    2.10 +  if is_empty b then ""
    2.11 +  else Long_Name.implode (map #1 qualifier @ [name]);
    2.12  
    2.13  
    2.14  (* system prefix *)