TimeLimit replaced by interrupt_timeout
authorwebertj
Mon Jan 23 17:29:52 2006 +0100 (2006-01-23 ago)
changeset 1876097aaecb84afe
parent 18759 2f55e3e47355
child 18761 4a58895f704c
TimeLimit replaced by interrupt_timeout
src/HOL/Tools/refute.ML
src/Pure/IsaMakefile
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml-interrupt-timeout.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj-interrupt-timeout.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Jan 23 15:23:31 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jan 23 17:29:52 2006 +0100
     1.3 @@ -923,8 +923,6 @@
     1.4  (* {...}     : parameters that control the translation/model generation      *)
     1.5  (* t         : term to be translated into a propositional formula            *)
     1.6  (* negate    : if true, find a model that makes 't' false (rather than true) *)
     1.7 -(* Note: exception 'TimeOut' is raised if the algorithm does not terminate   *)
     1.8 -(*       within 'maxtime' seconds (if 'maxtime' >0)                          *)
     1.9  (* ------------------------------------------------------------------------- *)
    1.10  
    1.11  	(* theory -> params -> Term.term -> bool -> unit *)
    1.12 @@ -1014,9 +1012,9 @@
    1.13  			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
    1.14  				^ Sign.string_of_term (sign_of thy) t);
    1.15  			if maxtime>0 then (
    1.16 -				TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
    1.17 +				interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))
    1.18  					wrapper ()
    1.19 -				handle TimeLimit.TimeOut =>
    1.20 +				handle Interrupt =>
    1.21  					writeln ("\nSearch terminated, time limit ("
    1.22  						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
    1.23  						^ ") exceeded.")
     2.1 --- a/src/Pure/IsaMakefile	Mon Jan 23 15:23:31 2006 +0100
     2.2 +++ b/src/Pure/IsaMakefile	Mon Jan 23 17:29:52 2006 +0100
     2.3 @@ -45,9 +45,10 @@
     2.4    Isar/session.ML Isar/skip_proof.ML Isar/specification.ML Isar/term_style.ML	\
     2.5    Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML             \
     2.6    ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML                         \
     2.7 -  ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                          \
     2.8 +  ML-Systems/polyml-interrupt-timeout.ML ML-Systems/polyml.ML                   \
     2.9    ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML                   \
    2.10    ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML                       \
    2.11 +  ML-Systems/smlnj-interrupt-timeout.ML                                         \
    2.12    ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML                       \
    2.13    ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML                         \
    2.14    ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML          \
     3.1 --- a/src/Pure/ML-Systems/mosml.ML	Mon Jan 23 15:23:31 2006 +0100
     3.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Jan 23 17:29:52 2006 +0100
     3.3 @@ -98,16 +98,8 @@
     3.4  (* bounded time execution *)
     3.5  
     3.6  (* FIXME proper implementation available? *)
     3.7 -
     3.8 -structure TimeLimit : sig
     3.9 -   exception TimeOut
    3.10 -   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
    3.11 -end = struct
    3.12 -   exception TimeOut
    3.13 -   fun timeLimit t f x =
    3.14 -      f x;
    3.15 -end;
    3.16 -
    3.17 +fun interrupt_timeout time f x =
    3.18 +  f x;
    3.19  
    3.20  (* ML command execution *)
    3.21  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Mon Jan 23 17:29:52 2006 +0100
     4.3 @@ -0,0 +1,44 @@
     4.4 +(*  Title:      Pure/ML-Systems/polyml-interrupt-timeout.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tjark Weber, Makarius
     4.7 +    Copyright   2006
     4.8 +
     4.9 +Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
    4.10 +*)
    4.11 +
    4.12 +local
    4.13 +
    4.14 +  val alarm_active = ref false;
    4.15 +
    4.16 +  val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ =>
    4.17 +    let val active = ! alarm_active in
    4.18 +      alarm_active := false;
    4.19 +      if active then
    4.20 +        Process.interruptConsoleProcesses ()
    4.21 +      else
    4.22 +        ()
    4.23 +    end));
    4.24 +
    4.25 +in
    4.26 +
    4.27 +  (* Time.time -> ('a -> 'b) -> 'a -> 'b *)
    4.28 +
    4.29 +  fun interrupt_timeout time f x =
    4.30 +  let
    4.31 +    fun deactivate_alarm () = (
    4.32 +      alarm_active := false;
    4.33 +      Posix.Process.alarm Time.zeroTime
    4.34 +    )
    4.35 +  in
    4.36 +    alarm_active := true;
    4.37 +    Posix.Process.alarm time;
    4.38 +    let val result = f x in
    4.39 +      deactivate_alarm ();
    4.40 +      result
    4.41 +    end handle exn => (
    4.42 +      deactivate_alarm ();
    4.43 +      raise exn
    4.44 +    )
    4.45 +  end;
    4.46 +
    4.47 +end;
     5.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Jan 23 15:23:31 2006 +0100
     5.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Jan 23 17:29:52 2006 +0100
     5.3 @@ -62,8 +62,12 @@
     5.4  
     5.5  (* bounded time execution *)
     5.6  
     5.7 +(* FIXME proper implementation for Cygwin available? *)
     5.8 +fun interrupt_timeout time f x =
     5.9 +  f x;
    5.10 +
    5.11  unless_cygwin
    5.12 -  use "ML-Systems/polyml-time-limit.ML";
    5.13 +  use "ML-Systems/polyml-interrupt-timeout.ML";
    5.14  
    5.15  
    5.16  (* prompts *)
     6.1 --- a/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 15:23:31 2006 +0100
     6.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 17:29:52 2006 +0100
     6.3 @@ -269,6 +269,12 @@
     6.4  end;
     6.5  
     6.6  
     6.7 +(* bounded time execution *)
     6.8 +
     6.9 +(* FIXME proper implementation available? *)
    6.10 +fun interrupt_timeout time f x =
    6.11 +  f x;
    6.12 +
    6.13  
    6.14  (** interrupts **)      (*Note: may get into race conditions*)
    6.15  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Mon Jan 23 17:29:52 2006 +0100
     7.3 @@ -0,0 +1,11 @@
     7.4 +(*  Title:      Pure/ML-Systems/smlnj-interrupt-timeout.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Tjark Weber, Makarius
     7.7 +    Copyright   2006
     7.8 +
     7.9 +Bounded time execution (similar to SML/NJ's TimeLimit structure).
    7.10 +*)
    7.11 +
    7.12 +fun interrupt_timeout time f x =
    7.13 +  TimeLimit.timeLimit time f x
    7.14 +    handle TimeLimit.TimeOut => raise SML90.Interrupt;
     8.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Jan 23 15:23:31 2006 +0100
     8.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jan 23 17:29:52 2006 +0100
     8.3 @@ -59,6 +59,11 @@
     8.4  | _ => use "ML-Systems/cpu-timer-gc.ML");
     8.5  
     8.6  
     8.7 +(* bounded time execution *)
     8.8 +
     8.9 +use "ML-Systems/smlnj-interrupt-timeout.ML";
    8.10 +
    8.11 +
    8.12  (*prompts*)
    8.13  fun ml_prompts p1 p2 =
    8.14    (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);