← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/fty/fixequiv.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/fty/fixequiv.lisp
302
302
                (fixequivs-from-explicit-args fn (cdr args) gutsformals formals hints state))
303
303
        (fixequivs-from-explicit-args fn (cdr args) gutsformals formals hints state)))))
304
304
 
305
 
(defun deffixequiv-expand-hint-fn (fn stable-under-simplificationp id clause)
306
 
  (b* (((unless (and stable-under-simplificationp
307
 
                     ;; Checks whether we're at a top-level induction
308
 
                     (equal (car id) '(0 1))))
 
305
(defun deffixequiv-expand-hint-fn (fn stable-under-simplificationp id clause world)
 
306
  (b* ((forcing-roundp (not (eql 0 (acl2::access acl2::clause-id id :forcing-round))))
 
307
       ((when forcing-roundp) nil)
 
308
       (pool-lst (acl2::access acl2::clause-id id :pool-lst))
 
309
       (top-levelp (not pool-lst))
 
310
       (single-inductionp (equal pool-lst '(1)))
 
311
       ((unless (or top-levelp single-inductionp))
 
312
        nil)
 
313
       ((when (and top-levelp (acl2::recursivep fn world)))
 
314
        `(:computed-hint-replacement t
 
315
          :induct (,fn . ,(fgetprop fn 'acl2::formals t world))))
 
316
       ((unless stable-under-simplificationp)
309
317
        nil)
310
318
       (concl (car (last clause)))
311
319
       (hint
336
344
    hint))
337
345
 
338
346
(defmacro deffixequiv-expand-hint (fn)
339
 
  `(deffixequiv-expand-hint-fn ',fn stable-under-simplificationp id clause))
 
347
  `(deffixequiv-expand-hint-fn ',fn stable-under-simplificationp id clause world))
 
348
 
 
349
(defun deffixequiv-default-hints (fnname world)
 
350
  (let ((entry (cdr (assoc 'deffixequiv (table-alist 'std::default-hints-table world)))))
 
351
    (subst fnname 'fnname entry)))
 
352
 
 
353
(defmacro set-deffixequiv-default-hints (hint)
 
354
  `(table std::default-hints-table 'deffixequiv ',hint))
 
355
 
 
356
(set-deffixequiv-default-hints
 
357
 ((deffixequiv-expand-hint fnname)))
 
358
 
340
359
 
341
360
(defun deffixequiv-fn (fn kw-args state)
342
361
  (b* ((__function__ 'deffixequiv)
353
372
       (args (cdr (assoc :args kwd-alist)))
354
373
       (hints (if (assoc :hints kwd-alist)
355
374
                  (cdr (assoc :hints kwd-alist))
356
 
                ;; try new default hint
357
 
                `((deffixequiv-expand-hint ,fn))))
 
375
                (deffixequiv-default-hints fn world)))
358
376
       ((when (and (not args) (not guts)))
359
377
        (raise "Deffixequiv requires either explicit types for the arguments ~
360
378
                to be considered, or for the function to have DEFINE info, ~
463
481
             (caar fixequiv-al) (cdar fixequiv-al) gutslist)
464
482
            (mutual-fixequivs->inductive-fix-thms (cdr fixequiv-al) gutslist))))
465
483
 
466
 
(defun mutual-fixequivs->fix-thm (fixequiv-al defines-entry kwd-alist)
 
484
(defun defgutslist->names (x)
 
485
  (if (atom x)
 
486
      nil
 
487
    (cons (std::defguts->name (car x))
 
488
          (defgutslist->names (cdr x)))))
 
489
 
 
490
 
 
491
(defun deffixequiv-mutual-default-default-hint (fnname id world)
 
492
  (let ((fns (acl2::recursivep fnname world)))
 
493
    (and (eql 0 (acl2::access acl2::clause-id id :forcing-round))
 
494
         (equal '(1) (acl2::access acl2::clause-id id :pool-lst))
 
495
         `(:computed-hint-replacement
 
496
           ((and stable-under-simplificationp
 
497
                 (std::expand-calls . ,fns)))
 
498
           :in-theory (disable . ,fns)))))
 
499
 
 
500
(defun deffixequiv-mutual-default-hints (fnname world)
 
501
  (let ((entry (cdr (assoc 'deffixequiv-mutual (table-alist 'std::default-hints-table world)))))
 
502
    (subst fnname 'fnname entry)))
 
503
 
 
504
(defmacro set-deffixequiv-mutual-default-hints (hint)
 
505
  `(table std::default-hints-table 'deffixequiv-mutual ',hint))
 
506
 
 
507
(set-deffixequiv-mutual-default-hints
 
508
 ((deffixequiv-mutual-default-default-hint 'fnname id world)))
 
509
 
 
510
 
 
511
 
 
512
 
 
513
(defun mutual-fixequivs->fix-thm (fixequiv-al defines-entry kwd-alist world)
467
514
  (b* ((thm-macro (std::defines-guts->flag-defthm-macro defines-entry))
468
 
       (hints (cdr (assoc :hints kwd-alist))))
 
515
       (gutslist (std::defines-guts->gutslist defines-entry))
 
516
       (fns (defgutslist->names gutslist))
 
517
       (hints-look (assoc :hints kwd-alist))
 
518
       (hints (if hints-look
 
519
                  (cdr hints-look)
 
520
                (deffixequiv-mutual-default-hints (car fns) world))))
469
521
    `(with-output :stack :pop
470
522
       (,thm-macro
471
523
        ,@(mutual-fixequivs->inductive-fix-thms
472
 
           fixequiv-al (std::defines-guts->gutslist defines-entry))
 
524
           fixequiv-al gutslist)
473
525
        :hints ,hints))))
474
526
  
475
527
(defun fixequivs->const/cong-thms (fixequivs)
544
596
       (fns/fixequivs (if args
545
597
                          (mutual-fixequivs-from-explicit-args fn-args univ-args gutslist state)
546
598
                        (mutual-fixequivs-from-defines fn-omit univ-omit gutslist state))))
547
 
    (cons (mutual-fixequivs->fix-thm fns/fixequivs defines-entry kwd-alist)
 
599
    (cons (mutual-fixequivs->fix-thm fns/fixequivs defines-entry kwd-alist world)
548
600
          (mutual-fixequivs->const/cong-thms fns/fixequivs))))
549
601
 
550
602
(defmacro deffixequiv-mutual (name &rest keys)