clarified Query_Operation.register: avoid hard-wired parallel policy;
authorwenzelm
Mon Aug 12 17:57:51 2013 +0200 (2013-08-12)
changeset 529828e78bd316a53
parent 52981 c7afd884dfb2
child 52983 92d98cc6cec2
clarified Query_Operation.register: avoid hard-wired parallel policy;
sledgehammer: more conventional parallel exception handling -- print just one interrupt;
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/Pure/PIDE/query_operation.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 12 17:17:49 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 12 17:57:51 2013 +0200
     1.3 @@ -496,42 +496,43 @@
     1.4  val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register_parallel sledgehammerN
     1.8 -    (fn st => fn [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] =>
     1.9 -      (case try Toplevel.proof_of st of
    1.10 -        SOME state =>
    1.11 -          let
    1.12 -            val ctxt = Proof.context_of state
    1.13 +  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
    1.14 +    (case try Toplevel.proof_of st of
    1.15 +      SOME state =>
    1.16 +        let
    1.17 +          val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
    1.18 +          val ctxt = Proof.context_of state
    1.19  
    1.20 -            val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
    1.21 -            val override_params =
    1.22 -              ([("timeout", [timeout_arg]),
    1.23 -                ("blocking", ["true"])] @
    1.24 -              (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
    1.25 -               then [("isar_proofs", [isar_proofs_arg])] else []) @
    1.26 -              (if debug then [("debug", ["false"])] else []) @
    1.27 -              (if verbose then [("verbose", ["false"])] else []) @
    1.28 -              (if overlord then [("overlord", ["false"])] else []))
    1.29 -              |> map (normalize_raw_param ctxt)
    1.30 +          val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
    1.31 +          val override_params =
    1.32 +            ([("timeout", [timeout_arg]),
    1.33 +              ("blocking", ["true"])] @
    1.34 +            (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
    1.35 +             then [("isar_proofs", [isar_proofs_arg])] else []) @
    1.36 +            (if debug then [("debug", ["false"])] else []) @
    1.37 +            (if verbose then [("verbose", ["false"])] else []) @
    1.38 +            (if overlord then [("overlord", ["false"])] else []))
    1.39 +            |> map (normalize_raw_param ctxt)
    1.40  
    1.41 -            val i = the_default 1 (Int.fromString subgoal_arg)
    1.42 +          val i = the_default 1 (Int.fromString subgoal_arg)
    1.43  
    1.44 -            val {provers, ...} =
    1.45 -              get_params Normal ctxt
    1.46 -                (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
    1.47 +          val {provers, ...} =
    1.48 +            get_params Normal ctxt
    1.49 +              (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
    1.50  
    1.51 -            fun run prover =
    1.52 -              let
    1.53 -                val prover_params = ("provers", [prover]) :: override_params
    1.54 -                val sledgehammer_params = get_params Normal ctxt prover_params
    1.55 -                val minimize = minimize_command prover_params i
    1.56 -                val (_, (_, state')) =
    1.57 -                  state
    1.58 -                  |> Proof.map_context (Config.put sledgehammer_result_request true)
    1.59 -                  |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
    1.60 -              in Config.get (Proof.context_of state') sledgehammer_result end
    1.61 +          fun run prover =
    1.62 +            let
    1.63 +              val prover_params = ("provers", [prover]) :: override_params
    1.64 +              val sledgehammer_params = get_params Normal ctxt prover_params
    1.65 +              val minimize = minimize_command prover_params i
    1.66 +              val (_, (_, state')) =
    1.67 +                state
    1.68 +                |> Proof.map_context (Config.put sledgehammer_result_request true)
    1.69 +                |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
    1.70 +            in output_result (Config.get (Proof.context_of state') sledgehammer_result) end
    1.71  
    1.72 -          in map (fn prover => fn () => run prover) provers end
    1.73 -      | NONE => error "Unknown proof context"));
    1.74 +          val _ = Par_Exn.release_all (Par_List.map (Exn.interruptible_capture run) provers);
    1.75 +        in () end
    1.76 +    | NONE => error "Unknown proof context"));
    1.77  
    1.78  end;
     2.1 --- a/src/Pure/PIDE/query_operation.ML	Mon Aug 12 17:17:49 2013 +0200
     2.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Aug 12 17:57:51 2013 +0200
     2.3 @@ -7,14 +7,14 @@
     2.4  
     2.5  signature QUERY_OPERATION =
     2.6  sig
     2.7 -  val register_parallel: string -> (Toplevel.state -> string list -> (unit -> string) list) -> unit
     2.8 -  val register: string -> (Toplevel.state -> string list -> string) -> unit
     2.9 +  val register: string ->
    2.10 +    ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
    2.11  end;
    2.12  
    2.13  structure Query_Operation: QUERY_OPERATION =
    2.14  struct
    2.15  
    2.16 -fun register_parallel name f =
    2.17 +fun register name f =
    2.18    Command.print_function name
    2.19      (fn {args = instance :: args, ...} =>
    2.20          SOME {delay = NONE, pri = 0, persistent = false, strict = false,
    2.21 @@ -22,23 +22,19 @@
    2.22              let
    2.23                fun result s = Output.result [(Markup.instanceN, instance)] s;
    2.24                fun status m = result (Markup.markup_only m);
    2.25 +              fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
    2.26                fun toplevel_error exn =
    2.27                  result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
    2.28  
    2.29                val _ = status Markup.running;
    2.30 -              val outputs =
    2.31 -                Multithreading.interruptible (fn () => f state args) ()
    2.32 -                  handle exn (*sic!*) => (toplevel_error exn; []);
    2.33 -              val _ = outputs |> Par_List.map (fn out =>
    2.34 -                (case Exn.capture (restore_attributes out) () (*sic!*) of
    2.35 -                  Exn.Res s => result (Markup.markup (Markup.writelnN, []) s)
    2.36 -                | Exn.Exn exn => toplevel_error exn));
    2.37 +              fun run () = f {state = state, args = args, output_result = output_result};
    2.38 +              val _ =
    2.39 +                (case Exn.capture (*sic!*) (restore_attributes run) () of
    2.40 +                  Exn.Res () => ()
    2.41 +                | Exn.Exn exn => toplevel_error exn);
    2.42                val _ = status Markup.finished;
    2.43              in () end)}
    2.44        | _ => NONE);
    2.45  
    2.46 -fun register name f =
    2.47 -  register_parallel name (fn st => fn args => [fn () => f st args]);
    2.48 -
    2.49  end;
    2.50  
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:17:49 2013 +0200
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:57:51 2013 +0200
     3.3 @@ -575,17 +575,17 @@
     3.4  (** PIDE query operation **)
     3.5  
     3.6  val _ =
     3.7 -  Query_Operation.register "find_theorems"
     3.8 -    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
     3.9 -      if can Toplevel.context_of st then
    3.10 -        let
    3.11 -          val state =
    3.12 -            if context_arg = "" then proof_state st
    3.13 -            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    3.14 -          val opt_limit = Int.fromString limit_arg;
    3.15 -          val rem_dups = allow_dups_arg = "false";
    3.16 -          val criteria = read_query Position.none query_arg;
    3.17 -        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
    3.18 -      else error "Unknown context");
    3.19 +  Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
    3.20 +    if can Toplevel.context_of st then
    3.21 +      let
    3.22 +        val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
    3.23 +        val state =
    3.24 +          if context_arg = "" then proof_state st
    3.25 +          else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    3.26 +        val opt_limit = Int.fromString limit_arg;
    3.27 +        val rem_dups = allow_dups_arg = "false";
    3.28 +        val criteria = read_query Position.none query_arg;
    3.29 +      in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
    3.30 +    else error "Unknown context");
    3.31  
    3.32  end;