← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/util/defs.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/centaur/vl/util/defs.lisp
235
235
       :exec (if (hons-get a alist) t nil)))
236
236
 
237
237
 
238
 
(define all-equalp (a x)
239
 
  :parents (utilities)
240
 
  :short "@(call all-equalp) determines if every members of @('x') is equal to
241
 
@('a')."
242
 
 
243
 
  :long "<p>In the logic, we define @('all-equalp') in terms of
244
 
@('replicate').</p>
245
 
 
246
 
<p>We usually leave this enabled and prefer to reason about @('replicate')
247
 
instead.  On the other hand, we also sometimes disable it and reason about it
248
 
recursively, so we do prove a few theorems about it.</p>
249
 
 
250
 
<p>For better execution speed, we use a recursive definition that does no
251
 
consing.</p>"
252
 
  :enabled t
253
 
 
254
 
  (mbe :logic
255
 
       (equal (list-fix x) (replicate (len x) a))
256
 
       :exec
257
 
       (if (consp x)
258
 
           (and (equal a (car x))
259
 
                (all-equalp a (cdr x)))
260
 
         t))
261
 
 
262
 
  :guard-hints(("Goal" :in-theory (enable all-equalp replicate)))
263
 
 
264
 
  ///
265
 
  (defrule all-equalp-when-atom
266
 
    (implies (atom x)
267
 
             (all-equalp a x)))
268
 
 
269
 
  (defrule all-equalp-of-cons
270
 
    (equal (all-equalp a (cons b x))
271
 
           (and (equal a b)
272
 
                (all-equalp a x)))
273
 
    :enable replicate)
274
 
 
275
 
  (local (in-theory (disable all-equalp)))
276
 
 
277
 
  (defrule car-when-all-equalp
278
 
    (implies (all-equalp a x)
279
 
             (equal (car x)
280
 
                    (if (consp x) a nil))))
281
 
 
282
 
  (defrule all-equalp-of-cdr-when-all-equalp
283
 
    (implies (all-equalp a x)
284
 
             (all-equalp a (cdr x))))
285
 
 
286
 
  (defrule all-equalp-of-append
287
 
    (equal (all-equalp a (append x y))
288
 
           (and (all-equalp a x)
289
 
                (all-equalp a y)))
290
 
    :induct (len x))
291
 
 
292
 
  (defrule all-equalp-of-rev
293
 
    (equal (all-equalp a (rev x))
294
 
           (all-equalp a x))
295
 
    :induct (len x))
296
 
 
297
 
  (defrule all-equalp-of-replicate
298
 
    (equal (all-equalp a (replicate n b))
299
 
           (or (equal a b)
300
 
               (zp n)))
301
 
    :enable replicate)
302
 
 
303
 
  (defrule all-equalp-of-take
304
 
    (implies (all-equalp a x)
305
 
             (equal (all-equalp a (take n x))
306
 
                    (or (not a)
307
 
                        (<= (nfix n) (len x)))))
308
 
    :enable acl2::take-redefinition)
309
 
 
310
 
  (defrule all-equalp-of-nthcdr
311
 
    (implies (all-equalp a x)
312
 
             (all-equalp a (nthcdr n x)))
313
 
    :enable nthcdr)
314
 
 
315
 
  (defrule member-equal-when-all-equalp
316
 
    (implies (all-equalp a x)
317
 
             (iff (member-equal b x)
318
 
                  (and (consp x)
319
 
                       (equal a b))))
320
 
    :induct (len x)))
321
 
 
322
 
 
323
238
 
324
239
(define remove-equal-without-guard (a x)
325
240
  :parents (utilities)
821
736
                 (not (atom (cdr x))))))
822
737
 
823
738
 
824
 
 
825
 
(defun tuplep (n x)
826
 
  (declare (xargs :guard (natp n)))
827
 
  (mbe :logic (and (true-listp x)
828
 
                   (equal (len x) n))
829
 
       :exec (and (true-listp x)
830
 
                  (eql (length x) n))))
831
 
 
832
 
(deflist cons-listp (x)
833
 
  (consp x)
834
 
  :elementp-of-nil nil)
835
 
 
836
 
(deflist cons-list-listp (x)
837
 
  (cons-listp x)
838
 
  :elementp-of-nil t)
839
 
 
840
 
 
841
 
 
842
 
 
843
 
 
844
739
(defsection and*
845
740
  :parents (utilities)
846
741
  :short "@('and*') is like @('and') but is a (typically disabled) function."
910
805
 
911
806
 
912
807
 
913
 
 
914
 
(defsection keys-boundp
915
 
  :parents (utilities)
916
 
  :short "@(call keys-boundp) determines if every key in @('keys') is bound in
917
 
the alist @('alist')."
918
 
 
919
 
  (defund keys-boundp-fal (keys alist)
920
 
    (declare (xargs :guard t))
921
 
    (if (atom keys)
922
 
        t
923
 
      (and (hons-get (car keys) alist)
924
 
           (keys-boundp-fal (cdr keys) alist))))
925
 
 
926
 
  (defund keys-boundp-slow-alist (keys alist)
927
 
    (declare (xargs :guard t))
928
 
    (if (atom keys)
929
 
        t
930
 
      (and (hons-assoc-equal (car keys) alist)
931
 
           (keys-boundp-slow-alist (cdr keys) alist))))
932
 
 
933
 
  (defund keys-boundp (keys alist)
934
 
    (declare (xargs :guard t :verify-guards nil))
935
 
    (mbe :logic
936
 
         (if (atom keys)
937
 
             t
938
 
           (and (hons-assoc-equal (car keys) alist)
939
 
                (keys-boundp (cdr keys) alist)))
940
 
         :exec
941
 
         (if (atom keys)
942
 
             t
943
 
           (if (and (acl2::worth-hashing keys)
944
 
                    (acl2::worth-hashing alist))
945
 
               (with-fast-alist alist (keys-boundp-fal keys alist))
946
 
             (keys-boundp-slow-alist keys alist)))))
947
 
 
948
 
  (local (in-theory (enable keys-boundp
949
 
                            keys-boundp-fal
950
 
                            keys-boundp-slow-alist)))
951
 
 
952
 
  (defrule keys-boundp-fal-removal
953
 
    (equal (keys-boundp-fal keys alist)
954
 
           (keys-boundp keys alist)))
955
 
 
956
 
  (defrule keys-boundp-slow-alist-removal
957
 
    (equal (keys-boundp-slow-alist keys alist)
958
 
           (keys-boundp keys alist)))
959
 
 
960
 
  (verify-guards keys-boundp)
961
 
 
962
 
  (defrule keys-boundp-when-atom
963
 
    (implies (atom keys)
964
 
             (equal (keys-boundp keys alist)
965
 
                    t)))
966
 
 
967
 
  (defrule keys-boundp-of-cons
968
 
    (equal (keys-boundp (cons a keys) alist)
969
 
           (and (hons-get a alist)
970
 
                (keys-boundp keys alist))))
971
 
 
972
 
  (defrule keys-boundp-of-list-fix
973
 
    (equal (keys-boundp (list-fix x) alist)
974
 
           (keys-boundp x alist)))
975
 
 
976
 
  (defrule keys-boundp-of-append
977
 
    (equal (keys-boundp (append x y) alist)
978
 
           (and (keys-boundp x alist)
979
 
                (keys-boundp y alist))))
980
 
 
981
 
  (defrule keys-boundp-of-rev
982
 
    (equal (keys-boundp (rev x) alist)
983
 
           (keys-boundp x alist)))
984
 
 
985
 
  (defrule keys-boundp-of-revappend
986
 
    (equal (keys-boundp (revappend x y) alist)
987
 
           (and (keys-boundp x alist)
988
 
                (keys-boundp y alist)))))
989
 
 
990
 
 
991
 
(defsection impossible
992
 
  :parents (utilities)
993
 
  :short "Prove that some case is unreachable using @(see guard)s."
994
 
 
995
 
  :long "<p>Logically, @('(impossible)') just returns @('nil').</p>
996
 
 
997
 
<p>But @('impossible') has a guard of @('nil'), so whenever you use it in a
998
 
function, you will be obliged to prove that it cannot be executed when the
999
 
guard holds.</p>
1000
 
 
1001
 
<p>What good is this?  One use is to make sure that every possible case in a
1002
 
sum type has been covered.  For instance, you can write:</p>
1003
 
 
1004
 
@({
1005
 
 (define f ((x whatever-p))
1006
 
   (case (type-of x)
1007
 
     (:foo (handle-foo ...))
1008
 
     (:bar (handle-bar ...))
1009
 
     (otherwise (impossible))))
1010
 
})
1011
 
 
1012
 
<p>This is a nice style in that, if we later extend @('x') so that its type can
1013
 
also be @(':baz'), then the guard verification will fail and remind us that we
1014
 
need to extend @('f') to handle @(':baz') types as well.</p>
1015
 
 
1016
 
<p>If somehow @('(impossible)') is ever executed (e.g., due to program mode
1017
 
code that is violating guards), it just causes a hard error.</p>"
1018
 
 
1019
 
  (defun impossible ()
1020
 
    (declare (xargs :guard nil))
1021
 
    (er hard 'impossible "Provably impossible")))
1022
 
 
1023
 
 
1024
808
;; kind of a terrible function name
1025
809
(define vl-width-from-difference ((a integerp))
1026
810
  :returns (width posp :rule-classes :type-prescription)