# HG changeset patch # User bulwahn # Date 1291719016 -3600 # Node ID 1c0eefa8d02a2bf8165568d9c3f007923d6f4281 # Parent 3750bdac1327c178c1255605df98b1175065b645# Parent 8275f52ac991bb11f3561c9bec2c65ac8e462274 merged diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/HOL.thy Tue Dec 07 11:50:16 2010 +0100 @@ -29,8 +29,6 @@ "~~/src/Tools/induct.ML" ("~~/src/Tools/induct_tacs.ML") ("Tools/recfun_codegen.ML") - "Tools/async_manager.ML" - "Tools/try.ML" ("Tools/cnf_funcs.ML") "~~/src/Tools/subtyping.ML" begin @@ -1982,10 +1980,6 @@ *} "solve goal by normalization" -subsection {* Try *} - -setup {* Try.setup *} - subsection {* Counterexample Search Units *} subsubsection {* Quickcheck *} diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 07 11:50:16 2010 +0100 @@ -224,7 +224,6 @@ Tools/Metis/metis_translate.ML \ Tools/abel_cancel.ML \ Tools/arith_data.ML \ - Tools/async_manager.ML \ Tools/cnf_funcs.ML \ Tools/dseq.ML \ Tools/inductive.ML \ @@ -344,6 +343,7 @@ Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ + Tools/Sledgehammer/async_manager.ML \ Tools/Sledgehammer/sledgehammer.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Metis.thy --- a/src/HOL/Metis.thy Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/Metis.thy Tue Dec 07 11:50:16 2010 +0100 @@ -12,6 +12,7 @@ ("Tools/Metis/metis_translate.ML") ("Tools/Metis/metis_reconstruct.ML") ("Tools/Metis/metis_tactics.ML") + ("Tools/try.ML") begin definition fequal :: "'a \ 'a \ bool" where [no_atp]: @@ -38,4 +39,10 @@ hide_const (open) fequal hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal +subsection {* Try *} + +use "Tools/try.ML" + +setup {* Try.setup *} + end diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Tue Dec 07 11:50:16 2010 +0100 @@ -8,7 +8,8 @@ theory Sledgehammer imports ATP SMT -uses "Tools/Sledgehammer/sledgehammer_util.ML" +uses "Tools/Sledgehammer/async_manager.ML" + "Tools/Sledgehammer/sledgehammer_util.ML" "Tools/Sledgehammer/sledgehammer_filter.ML" "Tools/Sledgehammer/sledgehammer_atp_translate.ML" "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 11:50:16 2010 +0100 @@ -133,8 +133,9 @@ Type (s, _) => let val s' = shortest_name s in prefix ^ - (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^ - atom_suffix s m + (if T = @{typ string} then "s" + else if String.isPrefix "\\" s' then s' + else substring (s', 0, 1)) ^ atom_suffix s m end | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 11:50:16 2010 +0100 @@ -216,7 +216,22 @@ else () end -fun gen_solver name info rm ctxt irules = + + +(* registry *) + +type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm + +type solver_info = { + env_var: string, + is_remote: bool, + options: Proof.context -> string list, + interface: interface, + reconstruct: string list * SMT_Translate.recon -> Proof.context -> + (int list * thm) * Proof.context, + default_max_relevant: int } + +fun gen_solver name (info : solver_info) rm ctxt irules = let val {env_var, is_remote, options, interface, reconstruct, ...} = info val {extra_norm, translate} = interface @@ -235,21 +250,6 @@ |> pair idxs) end - - -(* registry *) - -type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm - -type solver_info = { - env_var: string, - is_remote: bool, - options: Proof.context -> string list, - interface: interface, - reconstruct: string list * SMT_Translate.recon -> Proof.context -> - (int list * thm) * Proof.context, - default_max_relevant: int } - structure Solvers = Generic_Data ( type T = solver_info Symtab.table diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Tools/Sledgehammer/async_manager.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Tue Dec 07 11:50:16 2010 +0100 @@ -0,0 +1,237 @@ +(* Title: HOL/Tools/Sledgehammer/async_manager.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Central manager for asynchronous diagnosis tool threads. +*) + +signature ASYNC_MANAGER = +sig + val break_into_chunks : string list -> string list + val launch : + string -> Time.time -> Time.time -> string -> (unit -> string) -> unit + val kill_threads : string -> string -> unit + val running_threads : string -> string -> unit + val thread_messages : string -> string -> int option -> unit +end; + +structure Async_Manager : ASYNC_MANAGER = +struct + +(** preferences **) + +val message_store_limit = 20; +val message_display_limit = 5; + + +(** thread management **) + +(* data structures over threads *) + +structure Thread_Heap = Heap +( + type elem = Time.time * Thread.thread; + fun ord ((a, _), (b, _)) = Time.compare (a, b); +); + +fun lookup_thread xs = AList.lookup Thread.equal xs; +fun delete_thread xs = AList.delete Thread.equal xs; +fun update_thread xs = AList.update Thread.equal xs; + + +(* state of thread manager *) + +type state = + {manager: Thread.thread option, + timeout_heap: Thread_Heap.T, + active: (Thread.thread * (string * Time.time * Time.time * string)) list, + canceling: (Thread.thread * (string * Time.time * string)) list, + messages: (string * string) list, + store: (string * string) list} + +fun make_state manager timeout_heap active canceling messages store : state = + {manager = manager, timeout_heap = timeout_heap, active = active, + canceling = canceling, messages = messages, store = store} + +val global_state = Synchronized.var "async_manager" + (make_state NONE Thread_Heap.empty [] [] [] []); + + +(* unregister thread *) + +fun unregister message thread = + Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (case lookup_thread active thread of + SOME (tool, _, _, desc) => + let + val active' = delete_thread thread active; + val now = Time.now () + val canceling' = (thread, (tool, now, desc)) :: canceling + val message' = desc ^ "\n" ^ message + val messages' = (tool, message') :: messages; + val store' = (tool, message') :: + (if length store <= message_store_limit then store + else #1 (chop message_store_limit store)); + in make_state manager timeout_heap active' canceling' messages' store' end + | NONE => state)); + + +(* main manager thread -- only one may exist *) + +val min_wait_time = seconds 0.3; +val max_wait_time = seconds 10.0; + +fun replace_all bef aft = + let + fun aux seen "" = String.implode (rev seen) + | aux seen s = + if String.isPrefix bef s then + aux seen "" ^ aft ^ aux [] (unprefix bef s) + else + aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) + in aux [] end + +(* This is a workaround for Proof General's off-by-a-few sendback display bug, + whereby "pr" in "proof" is not highlighted. *) +val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000") + +fun print_new_messages () = + case Synchronized.change_result global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + (messages, make_state manager timeout_heap active canceling [] + store)) of + [] => () + | msgs as (tool, _) :: _ => + let val ss = break_into_chunks (map snd msgs) in + List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss) + end + +fun check_thread_manager () = Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state + else let val manager = SOME (Toplevel.thread false (fn () => + let + fun time_limit timeout_heap = + (case try Thread_Heap.min timeout_heap of + NONE => Time.+ (Time.now (), max_wait_time) + | SOME (time, _) => time); + + (*action: find threads whose timeout is reached, and interrupt canceling threads*) + fun action {manager, timeout_heap, active, canceling, messages, store} = + let val (timeout_threads, timeout_heap') = + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; + in + if null timeout_threads andalso null canceling then + NONE + else + let + val _ = List.app (Simple_Thread.interrupt o #1) canceling + val canceling' = filter (Thread.isActive o #1) canceling + val state' = make_state manager timeout_heap' active canceling' messages store; + in SOME (map #2 timeout_threads, state') end + end; + in + while Synchronized.change_result global_state + (fn state as {timeout_heap, active, canceling, messages, store, ...} => + if null active andalso null canceling andalso null messages + then (false, make_state NONE timeout_heap active canceling messages store) + else (true, state)) + do + (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action + |> these + |> List.app (unregister "Timed out.\n"); + print_new_messages (); + (*give threads some time to respond to interrupt*) + OS.Process.sleep min_wait_time) + end)) + in make_state manager timeout_heap active canceling messages store end) + + +(* register thread *) + +fun register tool birth_time death_time desc thread = + (Synchronized.change global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + let + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; + val state' = make_state manager timeout_heap' active' canceling messages store; + in state' end); + check_thread_manager ()) + + +fun launch tool birth_time death_time desc f = + (Toplevel.thread true + (fn () => + let + val self = Thread.self () + val _ = register tool birth_time death_time desc self + val message = f () + in unregister message self end); + ()) + + +(** user commands **) + +(* kill threads *) + +fun kill_threads tool workers = Synchronized.change global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + let + val killing = + map_filter (fn (th, (tool', _, _, desc)) => + if tool' = tool then SOME (th, (tool', Time.now (), desc)) + else NONE) active + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; + val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".") + in state' end); + + +(* running threads *) + +fun seconds time = string_of_int (Time.toSeconds time) ^ " s" + +fun running_threads tool workers = + let + val {active, canceling, ...} = Synchronized.value global_state; + + val now = Time.now (); + fun running_info (_, (tool', birth_time, death_time, desc)) = + if tool' = tool then + SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) + else + NONE + fun canceling_info (_, (tool', death_time, desc)) = + if tool' = tool then + SOME ("Trying to interrupt thread since " ^ + seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) + else + NONE + val running = + case map_filter running_info active of + [] => ["No " ^ workers ^ " running."] + | ss => "Running " ^ workers ^ ":" :: ss + val interrupting = + case map_filter canceling_info canceling of + [] => [] + | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss + in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end + +fun thread_messages tool worker opt_limit = + let + val limit = the_default message_display_limit opt_limit; + val tool_store = Synchronized.value global_state + |> #store |> filter (curry (op =) tool o fst) + val header = + "Recent " ^ worker ^ " messages" ^ + (if length tool_store <= limit then ":" + else " (" ^ string_of_int limit ^ " displayed):"); + in + List.app Output.urgent_message (header :: break_into_chunks + (map snd (#1 (chop limit tool_store)))) + end + +end; diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Tools/async_manager.ML --- a/src/HOL/Tools/async_manager.ML Tue Dec 07 10:03:43 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,237 +0,0 @@ -(* Title: HOL/Tools/async_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager for asynchronous diagnosis tool threads. -*) - -signature ASYNC_MANAGER = -sig - val break_into_chunks : string list -> string list - val launch : - string -> Time.time -> Time.time -> string -> (unit -> string) -> unit - val kill_threads : string -> string -> unit - val running_threads : string -> string -> unit - val thread_messages : string -> string -> int option -> unit -end; - -structure Async_Manager : ASYNC_MANAGER = -struct - -(** preferences **) - -val message_store_limit = 20; -val message_display_limit = 5; - - -(** thread management **) - -(* data structures over threads *) - -structure Thread_Heap = Heap -( - type elem = Time.time * Thread.thread; - fun ord ((a, _), (b, _)) = Time.compare (a, b); -); - -fun lookup_thread xs = AList.lookup Thread.equal xs; -fun delete_thread xs = AList.delete Thread.equal xs; -fun update_thread xs = AList.update Thread.equal xs; - - -(* state of thread manager *) - -type state = - {manager: Thread.thread option, - timeout_heap: Thread_Heap.T, - active: (Thread.thread * (string * Time.time * Time.time * string)) list, - canceling: (Thread.thread * (string * Time.time * string)) list, - messages: (string * string) list, - store: (string * string) list} - -fun make_state manager timeout_heap active canceling messages store : state = - {manager = manager, timeout_heap = timeout_heap, active = active, - canceling = canceling, messages = messages, store = store} - -val global_state = Synchronized.var "async_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); - - -(* unregister thread *) - -fun unregister message thread = - Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - (case lookup_thread active thread of - SOME (tool, _, _, desc) => - let - val active' = delete_thread thread active; - val now = Time.now () - val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = desc ^ "\n" ^ message - val messages' = (tool, message') :: messages; - val store' = (tool, message') :: - (if length store <= message_store_limit then store - else #1 (chop message_store_limit store)); - in make_state manager timeout_heap active' canceling' messages' store' end - | NONE => state)); - - -(* main manager thread -- only one may exist *) - -val min_wait_time = seconds 0.3; -val max_wait_time = seconds 10.0; - -fun replace_all bef aft = - let - fun aux seen "" = String.implode (rev seen) - | aux seen s = - if String.isPrefix bef s then - aux seen "" ^ aft ^ aux [] (unprefix bef s) - else - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) - in aux [] end - -(* This is a workaround for Proof General's off-by-a-few sendback display bug, - whereby "pr" in "proof" is not highlighted. *) -val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000") - -fun print_new_messages () = - case Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - (messages, make_state manager timeout_heap active canceling [] - store)) of - [] => () - | msgs as (tool, _) :: _ => - let val ss = break_into_chunks (map snd msgs) in - List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss) - end - -fun check_thread_manager () = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (Toplevel.thread false (fn () => - let - fun time_limit timeout_heap = - (case try Thread_Heap.min timeout_heap of - NONE => Time.+ (Time.now (), max_wait_time) - | SOME (time, _) => time); - - (*action: find threads whose timeout is reached, and interrupt canceling threads*) - fun action {manager, timeout_heap, active, canceling, messages, store} = - let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; - in - if null timeout_threads andalso null canceling then - NONE - else - let - val _ = List.app (Simple_Thread.interrupt o #1) canceling - val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store; - in SOME (map #2 timeout_threads, state') end - end; - in - while Synchronized.change_result global_state - (fn state as {timeout_heap, active, canceling, messages, store, ...} => - if null active andalso null canceling andalso null messages - then (false, make_state NONE timeout_heap active canceling messages store) - else (true, state)) - do - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action - |> these - |> List.app (unregister "Timed out.\n"); - print_new_messages (); - (*give threads some time to respond to interrupt*) - OS.Process.sleep min_wait_time) - end)) - in make_state manager timeout_heap active canceling messages store end) - - -(* register thread *) - -fun register tool birth_time death_time desc thread = - (Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; - in state' end); - check_thread_manager ()) - - -fun launch tool birth_time death_time desc f = - (Toplevel.thread true - (fn () => - let - val self = Thread.self () - val _ = register tool birth_time death_time desc self - val message = f () - in unregister message self end); - ()) - - -(** user commands **) - -(* kill threads *) - -fun kill_threads tool workers = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = - map_filter (fn (th, (tool', _, _, desc)) => - if tool' = tool then SOME (th, (tool', Time.now (), desc)) - else NONE) active - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; - val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".") - in state' end); - - -(* running threads *) - -fun seconds time = string_of_int (Time.toSeconds time) ^ " s" - -fun running_threads tool workers = - let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); - fun running_info (_, (tool', birth_time, death_time, desc)) = - if tool' = tool then - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) - else - NONE - fun canceling_info (_, (tool', death_time, desc)) = - if tool' = tool then - SOME ("Trying to interrupt thread since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) - else - NONE - val running = - case map_filter running_info active of - [] => ["No " ^ workers ^ " running."] - | ss => "Running " ^ workers ^ ":" :: ss - val interrupting = - case map_filter canceling_info canceling of - [] => [] - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss - in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end - -fun thread_messages tool worker opt_limit = - let - val limit = the_default message_display_limit opt_limit; - val tool_store = Synchronized.value global_state - |> #store |> filter (curry (op =) tool o fst) - val header = - "Recent " ^ worker ^ " messages" ^ - (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):"); - in - List.app Output.urgent_message (header :: break_into_chunks - (map snd (#1 (chop limit tool_store)))) - end - -end; diff -r 3750bdac1327 -r 1c0eefa8d02a src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Tue Dec 07 10:03:43 2010 +0100 +++ b/src/HOL/Tools/try.ML Tue Dec 07 11:50:16 2010 +0100 @@ -77,28 +77,33 @@ fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" fun do_try auto timeout_opt st = - case do_methods |> Par_List.map (fn f => f auto timeout_opt st) - |> map_filter I |> sort (int_ord o pairself snd) of - [] => (if auto then () else writeln "No proof found."; (false, st)) - | xs as (s, _) :: _ => - let - val xs = xs |> map swap |> AList.coalesce (op =) - |> map (swap o apsnd commas) - val message = - (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^ - Markup.markup Markup.sendback - ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ - " " ^ s) ^ - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" - in - (true, st |> (if auto then - Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.hilite - [Pretty.str message]]) - else - tap (fn _ => Output.urgent_message message))) - end + let + val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) + in + case do_methods |> Par_List.map (fn f => f auto timeout_opt st) + |> map_filter I |> sort (int_ord o pairself snd) of + [] => (if auto then () else writeln "No proof found."; (false, st)) + | xs as (s, _) :: _ => + let + val xs = xs |> map swap |> AList.coalesce (op =) + |> map (swap o apsnd commas) + val message = + (if auto then "Auto Try found a proof" else "Try this command") ^ + ": " ^ + Markup.markup Markup.sendback + ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" + else "apply") ^ " " ^ s) ^ + "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" + in + (true, st |> (if auto then + Proof.goal_message + (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Markup.hilite + [Pretty.str message]]) + else + tap (fn _ => Output.urgent_message message))) + end + end val invoke_try = fst oo do_try false