~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to interface-raw.lisp

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

interface-raw.lisp

1

 

; ACL2 Version 3.0.1 -- A Computational Logic for Applicative Common Lisp

 

1

; ACL2 Version 3.1 -- A Computational Logic for Applicative Common Lisp

2

2

; Copyright (C) 2006  University of Texas at Austin

3

3

 

4

4

; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright

709

709

       untranslate-lst

710

710

       with-error-trace-fn trace$-fn untrace$-fn

711

711

       set-w acl2-unwind-protect

712

 

       compress1 compress2

713

712

       ))

714

713

 

715

714

; Here are the *1* functions.  They should be kept in sync with

907

906

; See comment in intern-in-package-of-symbol for an explanation of this trick.

908

907

            ans)

909

908

        (throw-raw-ev-fncall (list 'pkg-witness-er pkg)))

910

 

    (gv pkg-witness (pkg) nil)))

 

909

    (gv pkg-witness (pkg) (intern *pkg-witness-name* "ACL2"))))

911

910

 

912

911

(defun-*1* numerator (x)

913

912

  (if (rationalp x)

1165

1164

 

1166

1165

)

1167

1166

 

1168

 

(defun-one-output collect-ignore-vars (dcls)

1169

 

  (cond

1170

 

   ((endp dcls) nil)

1171

 

   ((eq (caar dcls) 'ignore)

1172

 

    (append (cdar dcls)

1173

 

            (collect-ignore-vars (cdr dcls))))

1174

 

   (t (collect-ignore-vars (cdr dcls)))))

1175

 

 

1176

1167

(defun-one-output select-stobj (name stobjs terms)

1177

1168

  (cond ((endp stobjs) nil)

1178

1169

        ((eq name (car stobjs)) (car terms))

1315

1306

                            in-theory-fn

1316

1307

                            in-arithmetic-theory-fn

1317

1308

                            push-untouchable-fn

 

1309

                            remove-untouchable-fn

 

1310

                            reset-prehistory-fn

1318

1311

                            set-body-fn

1319

1312

                            table-fn

1320

1313

                            progn-fn

1341

1334

     (t

1342

1335

      (let* ((*1*guard (oneify guard wrld))

1343

1336

 

1344

 

; We throw away most declararations and the doc string, keeping only ignore

1345

 

; declarations.  Note that it is quite reasonable to ignore declarations when

1346

 

; constructing ``slow'' functions.

 

1337

; We throw away most declararations and the doc string, keeping only ignore and

 

1338

; ignorable declarations.  Note that it is quite reasonable to ignore

 

1339

; declarations when constructing ``slow'' functions.

1347

1340

 

1348

1341

             (body (car (last def)))

1349

1342

             (*1*body (oneify body wrld))

1369

1362

; fail_if_live_stobj (defined below), which refers to all the formals; hence

1370

1363

; ignore-vars should be nil if super-stobjs-in is non-nil.

1371

1364

 

1372

 

              (and (not super-stobjs-in) (collect-ignore-vars dcls)))

 

1365

              (and (not super-stobjs-in) (ignore-vars dcls)))

 

1366

             (ignorable-vars (ignorable-vars dcls))

1373

1367

             (guard-checking-on-form

1374

1368

 

1375

1369

; Functions in the ev-rec nest have a gc-off parameter that we generally assume

1454

1448

                                (list declare-stobj-special))

1455

1449

                         ,@(and ignore-vars

1456

1450

                                `((declare (ignore ,@ignore-vars))))

 

1451

                         ,@(and ignorable-vars

 

1452

                                `((declare (ignorable ,@ignorable-vars))))

1457

1453

                         ,@(and super-stobjs-in

1458

1454

                                `((when ,super-stobjs-chk

1459

1455

                                    ,fail_if_live_stobj)))

2656

2652

; is treated as Common Lisp values, then we are not sure that we trust our

2657

2653

; algorithm for creating that declaim form, which relies on output arities

2658

2654

; being correctly stored in the stobjs-out field of the original function (see

2659

 

; output-types-for-declare-form).  But perhaps with a little thought we could

 

2655

; output-type-for-declare-form).  But perhaps with a little thought we could

2660

2656

; do something useful here even in that case.

2661

2657

 

2662

2658

                       (eval (make-defun-declare-form (car def) *1*def))

2665

2661

                    ((and (not ignorep)

2666

2662

                          (equal *main-lisp-package-name*

2667

2663

                                 (symbol-package-name (car def))))

2668

 

                     (interface-er "It is illegal to redefine a ~

2669

 

                                        function in the main Lisp ~

2670

 

                                        package, such as ~x0!"

 

2664

                     (interface-er "It is illegal to redefine a function in ~

 

2665

                                    the main Lisp package, such as ~x0!"

2671

2666

                                   (car def)))

2672

2667

                    ((and (consp ignorep)

2673

2668

                          (eq (car ignorep) 'defstobj))

3888

3883

             (check-none-ideal (cdr trips) (cons (nth 5 trip) acc)))

3889

3884

            (t (check-none-ideal (cdr trips) acc)))))))

3890

3885

 

 

3886

(defun check-state-globals-initialized ()

 

3887

  (let (bad)

 

3888

    (do-symbols

 

3889

     (sym (find-package "ACL2_GLOBAL_ACL2"))

 

3890

     (when (boundp sym)

 

3891

       (let ((acl2-sym (intern (symbol-name sym) "ACL2")))

 

3892

         (when (not

 

3893

                (or (assoc acl2-sym *initial-global-table* :test 'eq)

 

3894

                    (assoc acl2-sym *initial-ld-special-bindings* :test 'eq)))

 

3895

           (push (cons acl2-sym (symbol-value sym))

 

3896

                 bad)))))

 

3897

    (when bad

 

3898

      (error

 

3899

       "The following symbols, perhaps with the values shown, need to~%~

 

3900

        be added to *initial-global-table*:~%~s~%"

 

3901

       bad))))

 

3902

 

3891

3903

(defun-one-output check-acl2-initialization ()

3892

3904

  (check-built-in-constants)

3893

3905

  (check-out-instantiablep (w *the-live-state*))

3894

 

  (check-none-ideal (w *the-live-state*) nil))

 

3906

  (check-none-ideal (w *the-live-state*) nil)

 

3907

  (check-state-globals-initialized))

3895

3908

 

3896

3909

(defun initialize-acl2 (&optional (pass-2-ld-skip-proofsp 'include-book)

3897

3910

                                  (acl2-pass-2-files *acl2-pass-2-files*)

4475

4488

 

4476

4489

       (compile-file os-file :output-file ofile)

4477

4490

       (load-compiled ofile)

4478

 

       (print ofile stream)

 

4491

       (terpri stream)

 

4492

       (prin1 ofile stream)

4479

4493

       (terpri stream)

4480

4494

       (terpri stream)

4481

4495

       (let ((file-date (file-write-date os-file))

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1