File: variables.lisp

package info (click to toggle)
acl2 7.2dfsg-3
  • links: PTS
  • area: main
  • in suites: stretch
  • size: 198,968 kB
  • ctags: 182,300
  • sloc: lisp: 2,415,261; ansic: 5,675; perl: 5,577; xml: 3,576; sh: 3,255; cpp: 2,835; makefile: 2,440; ruby: 2,402; python: 778; ml: 763; yacc: 709; csh: 355; php: 171; lex: 162; tcl: 44; java: 24; asm: 23; haskell: 17
file content (31 lines) | stat: -rw-r--r-- 884 bytes parent folder | download | duplicates (11) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
 
(in-package "ACL2")

#|

  variables.lisp
  ~~~~~~~~~~~~~~

In this book, we define macros for accessing and updating the variables in our
bakery implementation. The variables are presented as fields of a record
structure.

|#

(include-book "records")

(defmacro choosing (x) `(<- ,x :choosing))
(defmacro status   (x) `(<- ,x :status))
(defmacro current  (x) `(<- ,x :current))
(defmacro pos      (x) `(<- ,x :pos))
(defmacro temp     (x) `(<- ,x :temp))
(defmacro loc      (x) `(<- ,x :loc))
(defmacro indices  (x) `(<- ,x :indices))
(defmacro procs    (x) `(<- ,x :procs))
(defmacro queue    (x) `(<- ,x :queue))
(defmacro maxval   (x) `(<- ,x :maxval))
(defmacro bucket   (x) `(<- ,x :bucket))
(defmacro get-go   (x) `(<- ,x :go))

(defmacro >st (&rest upds) `(update st  ,@upds))
(defmacro >p  (&rest upds) `(update p   ,@upds))
(defmacro >_  (&rest upds) `(update nil ,@upds))