← Back to branch summary

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

« back to all changes in this revision

Viewing changes to proof-checker-b.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:
proof-checker-b.lisp
1
 
; ACL2 Version 6.5 -- A Computational Logic for Applicative Common Lisp
2
 
; Copyright (C) 2014, Regents of the University of Texas
 
1
; ACL2 Version 7.0 -- A Computational Logic for Applicative Common Lisp
 
2
; Copyright (C) 2015, Regents of the University of Texas
3
3
 
4
4
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
5
5
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
1534
1534
         (car alist))
1535
1535
        (t (rassoc-eq-as-car key (cdr alist)))))
1536
1536
 
 
1537
(defconst *ca<d^n>r-alist*
 
1538
 
 
1539
; This alist can be constructed as follows in raw Lisp.  Thus, it associates
 
1540
; each legal cd..dr macro with the number of ds in its name.
 
1541
 
 
1542
; ? (loop for x in
 
1543
; '(cadr           cdar          caar          cddr
 
1544
;   caadr   cdadr  cadar  cddar  caaar  cdaar  caddr  cdddr
 
1545
;   caaadr  cadadr caadar caddar
 
1546
;   cdaadr  cddadr cdadar cdddar
 
1547
;                                caaaar cadaar caaddr cadddr
 
1548
;                                cdaaar cddaar cdaddr cddddr)
 
1549
; collect (cons x (- (length (symbol-name x)) 2)))
 
1550
 
 
1551
  '((CADR . 2) (CDAR . 2) (CAAR . 2) (CDDR . 2)
 
1552
    (CAADR . 3) (CDADR . 3) (CADAR . 3) (CDDAR . 3)
 
1553
    (CAAAR . 3) (CDAAR . 3) (CADDR . 3) (CDDDR . 3)
 
1554
    (CAAADR . 4) (CADADR . 4) (CAADAR . 4) (CADDAR . 4)
 
1555
    (CDAADR . 4) (CDDADR . 4) (CDADAR . 4) (CDDDAR . 4)
 
1556
    (CAAAAR . 4) (CADAAR . 4) (CAADDR . 4) (CADDDR . 4)
 
1557
    (CDAAAR . 4) (CDDAAR . 4) (CDADDR . 4) (CDDDDR . 4)))
 
1558
 
 
1559
(defun car/cdr^n (n term)
 
1560
 
 
1561
; This function assumes that term is a nest of n or more nested calls of car
 
1562
; and/or cdr, and returns the term obtained by stripping n such calls.
 
1563
 
 
1564
  (cond
 
1565
   ((zp n) term)
 
1566
   ((or (variablep term)
 
1567
;       (fquotep term)
 
1568
        (not (member-eq (car term) '(car cdr))))
 
1569
    (er hard 'car/cdr^n
 
1570
        "Illegal call: ~x0.~|If you encountered this call in the ~
 
1571
         proof-checker, please contact the ACL2 implemntors."
 
1572
        `(car/cdr^n ,n ,term)))
 
1573
   (t (car/cdr^n (1- n) (fargn term 1)))))
 
1574
 
1537
1575
(defun expand-address (addr raw-term term abbreviations iff-flg
1538
1576
                            accumulated-addr-r wrld)
1539
1577
 
1884
1922
               ((implies iff)
1885
1923
                (expand-address-recurse :new-iff-flg t))
1886
1924
               (t
1887
 
                (mv-let
1888
 
                 (fn guts)
1889
 
                 (car-cdr-nest term)
1890
 
                 (cond
1891
 
                  (fn
1892
 
                   (expand-address-recurse
1893
 
                    :ans (append (make-list (- (length (symbol-name fn)) 2)
1894
 
                                            :initial-element 1)
1895
 
                                 rest-addr)
1896
 
                    :new-term guts))
1897
 
                  (t (expand-address-recurse))))))))))))
 
1925
                (let ((pair (and (consp raw-term)
 
1926
                                 (assoc-eq (car raw-term) *ca<d^n>r-alist*))))
 
1927
                  (cond
 
1928
                   (pair
 
1929
                    (expand-address-recurse
 
1930
                     :ans (append (make-list (cdr pair)
 
1931
                                             :initial-element 1)
 
1932
                                  rest-addr)
 
1933
                     :new-term (car/cdr^n (cdr pair) term)))
 
1934
                   (t (expand-address-recurse))))))))))))
1898
1935
 
1899
1936
(defmacro dv-error (str alist)
1900
1937
  `(pprogn (print-no-change
3281
3318
(define-pc-macro al (&rest args)
3282
3319
  (value (cons :apply-linear args)))
3283
3320
 
 
3321
#+acl2-legacy-doc
3284
3322
(defun pc-help-fn (name state)
3285
3323
  ;; Adapted in part from doc-fn.
3286
3324
  (declare (xargs :guard (and (symbolp name)
3327
3365
                          (newline channel state)
3328
3366
                          (end-doc channel state))))))))))
3329
3367
 
 
3368
#+acl2-legacy-doc
3330
3369
(defmacro state-only (triple)
3331
3370
  `(mv-let (erp val state)
3332
3371
           ,triple
3333
3372
           (declare (ignore erp val))
3334
3373
           state))
3335
3374
 
 
3375
(define-pc-macro doc (&optional name)
 
3376
  (let ((name (or name (make-official-pc-command 'doc))))
 
3377
    (cond ((and (equal (assoc-eq :doc (ld-keyword-aliases state))
 
3378
                       '(:DOC 1 XDOC))
 
3379
                (function-symbolp 'colon-xdoc-initialized (w state)))
 
3380
           (value `(lisp (if (colon-xdoc-initialized state)
 
3381
                             (xdoc ',name)
 
3382
                           (pprogn
 
3383
                            (fms0 "Note: Using built-in :doc command.  To use ~
 
3384
                                   :xdoc command, exit the proof-checker and ~
 
3385
                                   run :doc in the top-level loop.~|~%")
 
3386
                            (doc ',name))))))
 
3387
          (t (value `(lisp (doc ',name)))))))
 
3388
 
 
3389
#+acl2-legacy-doc
3336
3390
(define-pc-help help (&optional instr)
3337
3391
  (let ((comm (make-official-pc-command (if args
3338
3392
                                            (if (consp instr) (car instr) instr)
3339
3393
                                          'help))))
3340
3394
    (state-only (pc-help-fn comm state))))
3341
3395
 
 
3396
#-acl2-legacy-doc
 
3397
(define-pc-macro help (&optional name)
 
3398
  (cond ((not (symbolp name))
 
3399
         (pprogn
 
3400
          (print-no-change "The argument for :HELP requires a symbol, but ~x0 ~
 
3401
                            is not a symbol."
 
3402
                           (list (cons #\0 name)))
 
3403
          (value :fail)))
 
3404
        (t (let ((name (if (equal (symbol-name name) "ALL")
 
3405
                           'proof-checker-commands
 
3406
                         (make-official-pc-command (or name 'help)))))
 
3407
             (value `(doc ,name))))))
 
3408
 
 
3409
#+acl2-legacy-doc
3342
3410
(defun pc-help!-fn (name state)
3343
3411
  ;; Adapted in part from doc-fn.
3344
3412
  (declare (xargs :guard (and (symbolp name)
3381
3449
                        (newline channel state)
3382
3450
                        (more-fn t state)))))))))
3383
3451
 
 
3452
#+acl2-legacy-doc
3384
3453
(define-pc-help help! (&optional instr)
3385
3454
  (let ((comm (make-official-pc-command (if instr
3386
3455
                                            (if (consp instr) (car instr) instr)
3387
3456
                                          'help))))
3388
3457
    (state-only (pc-help!-fn comm state))))
3389
3458
 
 
3459
#+acl2-legacy-doc
3390
3460
(define-pc-macro help-long (&rest args)
3391
3461
  (value (cons 'help! args)))
3392
3462
 
 
3463
#+acl2-legacy-doc
3393
3464
(define-pc-help more ()
3394
3465
  (state-only (more-fn 0 state)))
3395
3466
 
 
3467
#+acl2-legacy-doc
3396
3468
(define-pc-help more! ()
3397
3469
  (state-only (more-fn t state)))
3398
3470
 
3517
3589
                        (cdr pair))
3518
3590
                    0))))
3519
3591
           (cond
 
3592
            ((not (natp repeat))
 
3593
             (print-no-change2
 
3594
              "The :REPEAT argument provided to S (or a command that invoked ~
 
3595
               S), which was ~x0, is illegal. ~ It must be T or a natural ~
 
3596
               number."
 
3597
              (list (cons #\0 repeat))))
 
3598
            ((not (natp local-backchain-limit))
 
3599
             (print-no-change2
 
3600
              "The :BACKCHAIN-LIMIT argument provided to S (or a command that ~
 
3601
               invoked S), which was ~x0, is illegal.  It must be NIL or a ~
 
3602
               natural number."
 
3603
              (list (cons #\0 local-backchain-limit))))
3520
3604
            ((not (or normalize rewrite))
3521
3605
             (print-no-change2 "You may not specify in the S command that ~
3522
3606
                                neither IF normalization nor rewriting is to ~
4228
4312
                     (goal-names (goals t))
4229
4313
                     must-succeed-flg))))
4230
4314
 
 
4315
#+acl2-legacy-doc
4231
4316
(defun print-help-separator (state)
4232
4317
  (io? proof-checker nil state
4233
4318
       nil
4234
4319
       (fms0 "~%==============================~%")))
4235
4320
 
 
4321
#+acl2-legacy-doc
4236
4322
(defun print-pc-help-rec (lst state)
4237
4323
  (declare (xargs :guard (true-listp lst)))
4238
4324
  (if (null lst)
4245
4331
      (print-help-separator state)
4246
4332
      (print-pc-help-rec (cdr lst) state)))))
4247
4333
 
 
4334
#+acl2-legacy-doc
4248
4335
(defun print-all-pc-help-fn (filename state)
4249
4336
  (mv-let (chan state)
4250
4337
          (open-output-channel filename :character state)
4261
4348
                                                'pc-acl2 state)))
4262
4349
                    state)))))
4263
4350
 
 
4351
#+acl2-legacy-doc
4264
4352
(defmacro print-all-pc-help (&optional filename)
4265
4353
  `(print-all-pc-help-fn ,(or filename "pc-help.out") state))
4266
4354
 
4786
4874
                              instr-list
4787
4875
                              '(signal value) ; quit-conditions
4788
4876
                              t ; pc-print-prompt-and-instr-flg, suitable for :pso
 
4877
                              nil ; in-verify-flg
4789
4878
                              state)
4790
4879
                     (pprogn
4791
4880
                      (cond (outputp (io? prove nil state