← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/matthews-vroon/support/partial-clock-functions/efficient-simulator.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/workshops/2004/matthews-vroon/support/partial-clock-functions/efficient-simulator.lisp
 
1
(in-package "ACL2")
 
2
(include-book "partial-clock-functions")
 
3
 
 
4
(verify-guards omega)
 
5
 
 
6
; note that this is admitted as an executable function. this is possible because:
 
7
; 1) we never change the original copy of mstate, so it fits with the rules of stobjs
 
8
; 2) acl2 allows functions that call partial functions to be declared executable.
 
9
; but because we do call a partial function inside steps-to-cutpoint-exec, any attempt
 
10
; to actually execute it result in an error;
 
11
(defun steps-to-cutpoint-exec (mstate)
 
12
  (declare (xargs :stobjs (mstate)))
 
13
  (let ((steps (steps-to-cutpoint-tail 0 (copy-from-mstate mstate))))
 
14
    (if (and (natp steps)        ;the number of steps is a natural number.
 
15
             (with-copy-of-stobj ;running a copy of our machine state forward steps steps
 
16
              mstate             ;gives us a cutpoint.
 
17
              (mv-let (result mstate)
 
18
                      (let ((mstate (run steps mstate)))
 
19
                        (mv (at-cutpoint mstate) mstate))
 
20
                      result)))
 
21
        steps
 
22
      (omega))))
 
23
 
 
24
(defthm o-p-steps-to-cutpoint-exec
 
25
  (o-p (steps-to-cutpoint-exec mstate))
 
26
  :hints (("goal" :in-theory (enable steps-to-cutpoint-exec))))
 
27
 
 
28
(defthm steps-to-cutpoint-exec-steps-to-cutpoint
 
29
 (implies (mstatep mstate)
 
30
          (equal (steps-to-cutpoint-exec mstate)
 
31
                 (steps-to-cutpoint mstate)))
 
32
 :hints (("goal" :in-theory (enable steps-to-cutpoint))))
 
33
 
 
34
(in-theory (disable steps-to-cutpoint-exec))
 
35
 
 
36
(defun dummy-mstate (mstate)
 
37
  (declare (xargs :stobjs (mstate)))
 
38
  (update-progc -1 mstate))
 
39
 
 
40
(defun next-cutpoint-exec (mstate)
 
41
  (declare (xargs :stobjs (mstate)
 
42
                  :measure (steps-to-cutpoint-exec mstate)
 
43
                  :guard (and (mstatep mstate)
 
44
                              (natp (steps-to-cutpoint-exec mstate)))))
 
45
  (if (mbt (and (mstatep mstate)
 
46
                (natp (steps-to-cutpoint-exec mstate))))
 
47
      (if (at-cutpoint mstate)
 
48
          mstate
 
49
        (let ((mstate (next mstate)))
 
50
          (next-cutpoint-exec mstate)))
 
51
    (dummy-mstate mstate)))
 
52
 
 
53
 
 
54
; (defexec next-cutpoint-exec (mstate)
 
55
;   (declare (xargs :stobjs (mstate)
 
56
;                   :measure (steps-to-cutpoint-exec mstate)
 
57
;                   :guard (and (mstatep mstate)
 
58
;                               (natp (steps-to-cutpoint-exec mstate))))
 
59
;          (exec-xargs :default-value (dummy-mstate mstate)))
 
60
; (mbe :exec (if (at-cutpoint mstate)
 
61
;                  mstate
 
62
;                (let ((mstate (next mstate)))
 
63
;                  (next-cutpoint-exec mstate)))
 
64
;        :logic (cond ((at-cutpoint mstate) mstate)
 
65
;                     ((or (not (natp (steps-to-cutpoint-exec mstate)))
 
66
;                          (not (mstatep mstate)))
 
67
;                      (dummy-mstate mstate))
 
68
;                     (t (let ((mstate (next mstate)))
 
69
;                          (next-cutpoint-exec mstate))))))
 
70
 
 
71
(defthm next-cutpoint-exec-cutpoint-exec
 
72
 (implies (and (mstatep mstate)
 
73
               (natp (steps-to-cutpoint-exec mstate)))
 
74
          (equal (next-cutpoint-exec mstate)
 
75
                 (next-cutpoint mstate)))
 
76
 :hints (("goal" :in-theory (e/d (next-cutpoint run)
 
77
                                 (next-cutpoint-intro-next)))))
 
78
 
 
79
(in-theory (disable next-cutpoint-exec))
 
80
 
 
81
(defun cutpoint-to-cutpoint-exec (mstate)
 
82
  (declare (xargs :stobjs (mstate)
 
83
                  :guard (and (at-cutpoint mstate)
 
84
                              (not (at-exitpoint mstate)))))
 
85
  (let ((mstate (next mstate)))
 
86
    (next-cutpoint-exec mstate)))
 
87
 
 
88
(defthm cutpoint-to-cutpoint-exec-cutpoint-to-cutpoint
 
89
 (implies (and (mstatep mstate)
 
90
               (at-cutpoint mstate)
 
91
               (not (at-exitpoint mstate)))
 
92
          (equal (cutpoint-to-cutpoint-exec mstate)
 
93
                 (cutpoint-to-cutpoint mstate)))
 
94
 :hints (("goal" :in-theory (enable cutpoint-to-cutpoint))))
 
95
 
 
96
(in-theory (disable cutpoint-to-cutpoint-exec))
 
97
 
 
98
(defun fast-cutpoint-to-cutpoint (mstate)
 
99
  (declare (xargs :stobjs (mstate)
 
100
                  :measure (cutpoint-measure mstate)
 
101
                  :guard (at-cutpoint mstate)))
 
102
  (if (mbt (at-cutpoint mstate))
 
103
      (if (at-exitpoint mstate)
 
104
          mstate
 
105
        (let ((mstate (cutpoint-to-cutpoint-exec mstate)))
 
106
          (fast-cutpoint-to-cutpoint mstate)))
 
107
    (dummy-mstate mstate)))
 
108
 
 
109
#|==================================================================|#
 
 
b'\\ No newline at end of file'