← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/acl2s/cgen/with-timeout.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/acl2s/cgen/with-timeout.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(begin-book t :ttags ((:acl2s-timeout)))
 
3
;$ACL2s-Preamble$|#
 
4
 
 
5
;Author: Harsh Raju Chamarthi
 
6
;Acknowledgements: Matt Kaufmann provided significant help.
 
7
 
 
8
(in-package "ACL2")
 
9
 
 
10
(include-book "xdoc/top" :dir :system)
 
11
(defxdoc with-timeout
 
12
  :parents (acl2::cgen)
 
13
  :short  "Evaluate form with a timeout (in seconds)"
 
14
  :long
 
15
  "<p>Evaluate form with a timeout in seconds. </p>
 
16
 
 
17
  <p>The general form is:
 
18
  @({with-timeout duration body timeout-form})
 
19
  </p>
 
20
 
 
21
  <p>
 
22
  @('duration') can be any rational value.  A duration of 0 seconds disables
 
23
  the timeout mechanism, i.e its a no-op. Suppose it is not, and @('duration')
 
24
  seconds elapse during evaluation of <tt>body</tt> then the evaluation is aborted
 
25
  and the value of @('timeout-form') is returned; in the normal case the value
 
26
  of <tt>body</tt> is returned. 
 
27
  </p>
 
28
  <p> The signature of <tt>body</tt> and <tt>timeout-form</tt> should be the same.  </p>
 
29
  
 
30
  <h3>Advanced Notes:</h3>
 
31
  <p>
 
32
  This form should be called either at the top-level or in
 
33
  an environment where state is available and <tt>body</tt> has
 
34
  no free variables other than state.
 
35
  If the timeout-form is a long running computation, 
 
36
  then the purpose of with-timeout is defeated.
 
37
  </p>
 
38
 
 
39
  <code>
 
40
    Usage:
 
41
    (with-timeout 5 (fibonacci 40) :timed-out)
 
42
    :doc with-timeout
 
43
  </code>
 
44
"
 
45
  )
 
46
 
 
47
(defttag :acl2s-timeout)
 
48
 
 
49
 
 
50
(progn!
 
51
 (set-raw-mode t)
 
52
 (load (concatenate 'string (cbd) "with-timeout-raw.lsp")))
 
53
 
 
54
 
 
55
(defmacro-last with-timeout-aux)
 
56
 
 
57
 
 
58
 
 
59
(defmacro with-timeout (duration form timeout-form)
 
60
"can only be called at top-level, that too only forms that are allowed
 
61
to be evaluated inside a function body. To eval defthm, use
 
62
with-timeout-ev instead"
 
63
`(if (equal 0 ,duration) ;if 0 then timeout is disabled
 
64
     ,form
 
65
   (top-level (with-timeout1 ,duration ,form ,timeout-form))))
 
66
 
 
67
 
 
68
;the following is for internal use only. I use it in timing out
 
69
;top-level-test? form, where i manually make a function body
 
70
;corresponding to the top-level-test?-fn, this way I dont have to
 
71
;worry about capturing free variables
 
72
 
 
73
(defmacro with-timeout1 (duration form timeout-form)
 
74
"can only be used inside a function body, and if form has
 
75
free variables other than state, then manually make a function
 
76
which takes those free variables as arguments and at the calling
 
77
context, pass the arguments, binding the free variables.
 
78
See top-level-test? macro for an example"
 
79
`(if (equal 0 ,duration) ;if 0 then timeout is disabled
 
80
    ,form
 
81
  (with-timeout-aux '(,duration ,timeout-form) ,form)))
 
82
 
 
83
(defttag nil) ; optional (books end with this implicitly)
 
84
 
 
85