← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/codewalker/if-tracker.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/projects/codewalker/if-tracker.lisp
 
1
; Copyright (C) 2014, ForrestHunt, Inc.
 
2
; Written by J Moore
 
3
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
4
 
 
5
; (certify-book "if-tracker")
 
6
 
 
7
; IF-TRACKER Normalization
 
8
; J Strother Moore
 
9
; June 2013
 
10
 
 
11
; We introduce IF-TRACKER as a constrained function with the property:
 
12
 
 
13
;  (equal (if-tracker rtests (if a b c))
 
14
;         (if a
 
15
;             (if-tracker (cons a rtests) b)          ; (HIDE a)!
 
16
;             (if-tracker (cons (not a) rtests) c)))  ; (HIDE (not a))!
 
17
 
 
18
; Of course, if this were a rewrite rule, the a and the (not a) in the first
 
19
; arguments of the IF-TRACKER terms would be immediately rewritten to T and NIL
 
20
; (assuming a is Boolean) because of the governing test on a.  Thus, in actual
 
21
; applications, we HIDE those two terms.
 
22
 
 
23
; However, in the course of simplifying IF-TRACKER terms we sometimes produce
 
24
; terms like:
 
25
 
 
26
; (IF-TRACKER rtests (foo (bar (IF a b c))))
 
27
 
 
28
; where the IF is buried and thus the rule above is not applied.
 
29
 
 
30
; We wish to lift the IFs out of the second argument of IF-TRACKER and then
 
31
; apply the IF-TRACKER property (with the indicated terms hidden).  We do this
 
32
; with a metafunction.  The metafunction is not very efficient, but is easily
 
33
; proved correct.
 
34
 
 
35
 
 
36
 
 
37
(in-package "ACL2")
 
38
 
 
39
(encapsulate ((if-tracker (rtests term) t))
 
40
             (local (defun if-tracker (rtests term)
 
41
                      (declare (ignore rtests term))
 
42
                      t))
 
43
             (defthm if-tracker-ignores-rtests
 
44
               (implies (syntaxp (not (quotep rtests)))
 
45
                        (equal (if-tracker rtests term)
 
46
                               (if-tracker  nil term)))))
 
47
 
 
48
(defun find-first-test (flg x)
 
49
  (if flg
 
50
      (cond
 
51
       ((variablep x) nil)
 
52
       ((fquotep x) nil)
 
53
       ((eq (ffn-symb x) 'IF)
 
54
        (let ((temp (find-first-test t (fargn x 1))))
 
55
          (cond ((null temp) (fargn x 1))
 
56
                (t temp))))
 
57
       (t (find-first-test nil (fargs x))))
 
58
      (cond ((endp x) nil)
 
59
            (t (or (find-first-test t (car x))
 
60
                   (find-first-test nil (cdr x)))))))
 
61
 
 
62
(defun reduce-if-with-test (flg test val x)
 
63
  (if flg
 
64
      (cond ((variablep x) x)
 
65
            ((fquotep x) x)
 
66
            ((and (eq (ffn-symb x) 'IF)
 
67
                  (equal (fargn x 1) test))
 
68
             (if val
 
69
                 (reduce-if-with-test t test val (fargn x 2))
 
70
                 (reduce-if-with-test t test val (fargn x 3))))
 
71
            (t (cons (ffn-symb x)
 
72
                     (reduce-if-with-test nil test val (cdr x)))))
 
73
      (cond ((endp x) nil)
 
74
            (t (cons (reduce-if-with-test t test val (car x))
 
75
                     (reduce-if-with-test nil test val (cdr x)))))))
 
76
 
 
77
(defun lift-first-test-through-if-tracker (term)
 
78
  (cond
 
79
   ((and (not (variablep term))
 
80
         (not (fquotep term))
 
81
         (eq (ffn-symb term) 'IF-TRACKER))
 
82
    (let ((a (find-first-test t (fargn term 2)))
 
83
          (rtests-term (fargn term 1)))
 
84
      (cond
 
85
       (a (list 'IF
 
86
                a
 
87
                (list 'IF-TRACKER
 
88
                      (list 'CONS (list 'HIDE a) rtests-term)
 
89
                      (reduce-if-with-test t a t (fargn term 2)))
 
90
                (list 'IF-TRACKER
 
91
                      (list 'cons
 
92
                            (list 'HIDE (list 'NOT a))
 
93
                            rtests-term)
 
94
                      (reduce-if-with-test t a nil (fargn term 2)))))
 
95
       (t term))))
 
96
   (t term)))
 
97
 
 
98
(defevaluator if-tracker-evl if-tracker-evl-lst
 
99
  ((CONS x y)
 
100
   (HIDE x)
 
101
   (NOT p)
 
102
   (IF-TRACKER rtests term)
 
103
   (IF a b c)))
 
104
 
 
105
(defthm reduce-if-with-test-correct
 
106
  (and (implies (and flg
 
107
                     (pseudo-termp x)
 
108
                     (iff (if-tracker-evl test a) val))
 
109
                (equal (if-tracker-evl (reduce-if-with-test flg test val x)
 
110
                            a)
 
111
                       (if-tracker-evl x a)))
 
112
       (implies (and (not flg)
 
113
                     (pseudo-term-listp x)
 
114
                     (iff (if-tracker-evl test a) val))
 
115
                (equal (if-tracker-evl-lst (reduce-if-with-test flg test val x)
 
116
                                a)
 
117
                       (if-tracker-evl-lst x a))))
 
118
  :hints (("Goal"
 
119
           :in-theory (enable IF-TRACKER-EVL-CONSTRAINT-0)
 
120
           :induct (reduce-if-with-test flg test val x))))
 
121
 
 
122
(defthm lift-first-test-through-if-tracker-correct
 
123
  (implies (pseudo-termp x)
 
124
           (equal (if-tracker-evl x a)
 
125
                  (if-tracker-evl (lift-first-test-through-if-tracker x) a)))
 
126
  :hints (("Goal" :expand ((:free (x) (hide x)))))
 
127
  :rule-classes ((:meta :trigger-fns (if-tracker))))
 
128
 
 
129
(in-theory (disable if-tracker-ignores-rtests))
 
130
 
 
131
#||
 
132
 
 
133
(defun steppe (x)
 
134
 
 
135
; Pretend this is the step function on an IFEQ, where the pc is (car x) and the
 
136
; stack is (cdr x).
 
137
 
 
138
  (cons (if (equal (car (cdr x)) 0) (+ 1 (car x)) (+ 2 (car x)))
 
139
        (if (evenp (car (cdr x)))
 
140
            (cddr x)
 
141
            (cdddr x))))
 
142
 
 
143
(thm (implies (and (integerp (car x))
 
144
                   (integerp (car (cdr x))))
 
145
              (if-tracker nil (car (steppe x))))
 
146
     :otf-flg t)
 
147
||#
 
148
 
 
149
 
 
150
 
 
151