src/Tools/try.ML
changeset 43020 abb5d1f907e4
parent 43018 121aa59b4d17
child 43021 5910dd009d0e
     1.1 --- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -6,16 +6,28 @@
     1.4  
     1.5  signature TRY =
     1.6  sig
     1.7 +  type tool =
     1.8 +    string * (bool Unsynchronized.ref
     1.9 +              * (bool -> Proof.state -> bool * (string * Proof.state)))
    1.10 +
    1.11 +  val tryN : string
    1.12    val auto_time_limit: real Unsynchronized.ref
    1.13  
    1.14 -  val register_tool :
    1.15 -    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
    1.16 -    -> theory
    1.17 +  val register_tool : tool -> theory -> theory
    1.18 +  val get_tools : theory -> tool list
    1.19 +  val try_tools : Proof.state -> (string * string) option
    1.20  end;
    1.21  
    1.22  structure Try : TRY =
    1.23  struct
    1.24  
    1.25 +type tool =
    1.26 +  string * (bool Unsynchronized.ref
    1.27 +            * (bool -> Proof.state -> bool * (string * Proof.state)))
    1.28 +
    1.29 +val tryN = "try"
    1.30 +
    1.31 +
    1.32  (* preferences *)
    1.33  
    1.34  val auto_time_limit = Unsynchronized.ref 4.0
    1.35 @@ -31,24 +43,42 @@
    1.36  
    1.37  structure Data = Theory_Data
    1.38  (
    1.39 -  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
    1.40 +  type T = tool list
    1.41    val empty = []
    1.42    val extend = I
    1.43    fun merge data : T = AList.merge (op =) (K true) data
    1.44  )
    1.45  
    1.46 +val get_tools = Data.get
    1.47 +
    1.48  val register_tool = Data.map o AList.update (op =)
    1.49  
    1.50 +(* try command *)
    1.51 +
    1.52 +fun try_tools state =
    1.53 +  get_tools (Proof.theory_of state)
    1.54 +  |> Par_List.get_some
    1.55 +         (fn (name, (_, tool)) =>
    1.56 +             case try (tool false) state of
    1.57 +               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    1.58 +             | _ => NONE)
    1.59 +
    1.60 +val _ =
    1.61 +  Outer_Syntax.improper_command tryN
    1.62 +      "try a combination of automatic proving and disproving tools" Keyword.diag
    1.63 +      (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    1.64 +
    1.65  
    1.66 -(* automatic testing *)
    1.67 +(* automatic try *)
    1.68  
    1.69 -fun run_tools tools state =
    1.70 -  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
    1.71 -        |> Par_List.get_some (fn tool =>
    1.72 -                                 case try tool state of
    1.73 -                                   SOME (true, state) => SOME state
    1.74 -                                 | _ => NONE)
    1.75 -        |> the_default state
    1.76 +fun auto_try state =
    1.77 +  get_tools (Proof.theory_of state)
    1.78 +  |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
    1.79 +  |> Par_List.get_some (fn tool =>
    1.80 +                           case try (tool true) state of
    1.81 +                             SOME (true, (_, state)) => SOME state
    1.82 +                           | _ => NONE)
    1.83 +  |> the_default state
    1.84  
    1.85  (* Too large values are understood as milliseconds, ensuring compatibility with
    1.86     old setting files. No users can possibly in their right mind want the user
    1.87 @@ -62,8 +92,7 @@
    1.88  
    1.89  val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
    1.90    if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
    1.91 -    TimeLimit.timeLimit (smart_seconds (!auto_time_limit))
    1.92 -        (run_tools (Data.get (Proof.theory_of state))) state
    1.93 +    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
    1.94      handle TimeLimit.TimeOut => state
    1.95    else
    1.96      state))