← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/std/util/returnspecs.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/std/util/returnspecs.lisp
143
143
   return-type   ; t when omitted
144
144
   hyp           ; t when omitted
145
145
   hints         ; nil when omitted
 
146
   hintsp        ; t if hints were provided
146
147
   rule-classes  ; :rewrite when omitted
147
148
   thm-name      ; NIL (to generate a name) or the name for the theorem
148
149
   )
154
155
                   :return-type t
155
156
                   :hyp t
156
157
                   :hints nil
 
158
                   :hintsp nil
157
159
                   :rule-classes :rewrite
158
160
                   :thm-name nil))
159
161
 
288
290
        ;; bozo not really a very good place to check for this.
289
291
        (raise "Error in ~x0: invalid keyword ~x1 used as a :hyp." fnname hyp)
290
292
        *default-returnspec*)
291
 
       (hints (if (assoc :hints kwd-alist)
292
 
                  (cdr (assoc :hints kwd-alist))
293
 
                nil))
 
293
       ((mv hints hintsp)
 
294
        (if (assoc :hints kwd-alist)
 
295
            (mv (cdr (assoc :hints kwd-alist)) t)
 
296
          (mv nil nil)))
294
297
       (rule-classes (if (assoc :rule-classes kwd-alist)
295
298
                         (cdr (assoc :rule-classes kwd-alist))
296
299
                       :rewrite))
325
328
                     :rule-classes rule-classes
326
329
                     :hyp hyp
327
330
                     :hints hints
 
331
                     :hintsp hintsp
328
332
                     :thm-name thm-name)))
329
333
 
330
334
(defun parse-returnspecs-aux (fnname x world)
480
484
     (concatenate 'string "RETURN-TYPE-OF-" (symbol-name name) multi-suffix)
481
485
     name)))
482
486
 
 
487
(defun returnspec-default-default-hint (fnname id world)
 
488
  (and (eql (len (acl2::recursivep fnname world)) 1) ;; singly recursive
 
489
       (let* ((pool-lst (acl2::access acl2::clause-id id :pool-lst)))
 
490
         (and (eql 0 (acl2::access acl2::clause-id id :forcing-round))
 
491
              (cond ((not pool-lst)
 
492
                     (let ((formals (look-up-formals fnname world)))
 
493
                       `(:induct (,fnname . ,formals)
 
494
                         :in-theory (disable (:d ,fnname)))))
 
495
                    ((equal pool-lst '(1))
 
496
                     `(:computed-hint-replacement
 
497
                       ((and stable-under-simplificationp
 
498
                             (expand-calls ,fnname)))
 
499
                       :in-theory (disable (:d ,fnname)))))))))
 
500
 
 
501
(defun returnspec-default-hints (fnname world)
 
502
  (let ((entry (cdr (assoc 'returnspec (table-alist 'std::default-hints-table world)))))
 
503
    (subst fnname 'fnname entry)))
 
504
 
 
505
(defmacro set-returnspec-default-hints (hint)
 
506
  `(table std::default-hints-table 'returnspec ',hint))
 
507
 
 
508
(set-returnspec-default-hints
 
509
 ((returnspec-default-default-hint 'fnname acl2::id world)))
 
510
 
483
511
(defun returnspec-single-thm (name name-fn x badname-okp world)
484
512
  "Returns EVENTS"
485
513
  ;; Only valid to call AFTER the function has been submitted, because we look
493
521
       (binds `(,x.name (,name-fn . ,formals)))
494
522
       (formula (returnspec-thm-body name-fn binds x world))
495
523
       ((when (eq formula t)) nil)
496
 
       (hints x.hints))
 
524
       (hints (if x.hintsp x.hints
 
525
                (returnspec-default-hints name-fn world))))
497
526
    `((defthm ,(returnspec-generate-name name x t badname-okp)
498
527
        ,formula
499
528
        :hints ,hints
508
537
  (b* (((returnspec x) x)
509
538
       (formula (returnspec-thm-body name-fn binds x world))
510
539
       ((when (equal formula t)) nil)
511
 
       (hints x.hints))
 
540
       (hints (if x.hintsp
 
541
                  x.hints
 
542
                (returnspec-default-hints name-fn world))))
512
543
    `((defthm ,(returnspec-generate-name name x nil badname-okp)
513
544
        ,formula
514
545
        :hints ,hints