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

« back to all changes in this revision

Viewing changes to acl2-fns.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

acl2-fns.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

167

167

    'integer)

168

168

   ((or (atom type1) (atom type2)) ; so, type is t since neither is *

169

169

    t)

 

170

   ((cdr (last type1)) ; (not (true-listp type1))

 

171

    (error

 

172

     "Non-atom, non-true-listp type for max-output-type-for-declare-form: ~s"

 

173

     type1))

 

174

   ((cdr (last type2)) ; (not (true-listp type2))

 

175

    (error

 

176

     "Non-atom, non-true-listp type for max-output-type-for-declare-form: ~s"

 

177

     type2))

170

178

   (t (let ((sym1 (car type1))

171

179

            (sym2 (car type2)))

172

180

        (cond

209

217

 

210

218

#+(and (or akcl openmcl) acl2-mv-as-values)

211

219

(defun max-output-type-for-declare-form-lst (type-list1 type-list2)

212

 

  (cond ((or (atom type-list1) (atom type-list2))

 

220

 

 

221

; Type-list1 and type-list2 are known to be true lists (null-terminated

 

222

; lists).

 

223

 

 

224

  (cond ((or (null type-list1) (null type-list2))

213

225

         (cond

214

 

          ((and (atom type-list1) (atom type-list2))

 

226

          ((and (null type-list1) (null type-list2))

215

227

           nil)

216

228

          ((and *acl2-output-type-abort*

217

229

                (or (atom type-list1) (atom type-list2)))

223

235

                   max-output-type-for-declare-form-lst called on lists of~%~

224

236

                   different length:~%~

225

237

                   ~s~%  ~s~%~

226

 

                   Please contact the ACL2 implementors."))))

 

238

                   Please contact the ACL2 implementors."

 

239

                  type-list1 type-list2))))

227

240

        (t (cons (max-output-type-for-declare-form

228

241

                  (car type-list1) (car type-list2))

229

242

                 (max-output-type-for-declare-form-lst

330

343

                 (output-type-for-declare-form-rec-list (cdr forms))))))

331

344

 

332

345

#+(or akcl openmcl)

333

 

(defun output-types-for-declare-form (fn form)

 

346

(defun output-type-for-declare-form (fn form)

334

347

 

335

348

; We return a list of output types, one per value.  So if #-acl2-mv-as-values,

336

349

; then we always return a list of length one.

338

351

  #-acl2-mv-as-values

339

352

  (declare (ignore fn))

340

353

  #-acl2-mv-as-values

341

 

  (list (output-type-for-declare-form-rec form))

 

354

  (list 'values (output-type-for-declare-form-rec form))

342

355

  #+acl2-mv-as-values

343

356

  (let* ((*acl2-output-type-abort* nil) ; protect for call on next line

344

357

         (result (output-type-for-declare-form-rec form))

355

368

              Stobjs-out = ~s~%~

356

369

              Result = ~s~%~

357

370

              Please contact the ACL2 implementors."

358

 

             (list 'output-types-for-declare-form fn '|defun...|)

 

371

             (list 'output-type-for-declare-form fn '|defun...|)

359

372

             stobjs-out result))

360

373

    (cond

361

374

     ((and (consp result)

362

375

           (eq (car result) 'values))

363

 

      (cdr result))

 

376

      result)

364

377

     (*acl2-output-type-abort*

365

 

      '(*))

 

378

      '*)

366

379

     (t

367

 

      (list result)))))

 

380

      (list 'values result)))))

368

381

 

369

382

(defun make-defun-declare-form (fn form

370

383

                                   &optional

371

 

                                   (output-types nil output-types-p))

 

384

                                   (output-type nil output-type-p))

372

385

 

373

386

; See the comment in proclaim-file for why we don't proclaim in more lisps.

374

387

 

375

 

  #-(or akcl openmcl) (declare (ignore fn form output-types output-types-p))

 

388

  #-(or akcl openmcl) (declare (ignore fn form output-type output-type-p))

376

389

  #-(or akcl openmcl) nil

377

390

 

378

391

  #+(or akcl openmcl)

379

 

  (let* ((output-types

380

 

          (if output-types-p

381

 

              output-types

382

 

            (output-types-for-declare-form fn (car (last form))))))

 

392

  (let* ((output-type

 

393

          (if output-type-p

 

394

              output-type

 

395

            (output-type-for-declare-form fn (car (last form))))))

383

396

    (let ((formals (caddr form)))

384

397

      (cond

385

398

       ((null (intersection formals lambda-list-keywords

388

401

                          ,(arg-declarations

389

402

                            formals

390

403

                            (collect-types (cdddr form)))

391

 

                          ,@output-types)

 

404

                          ,output-type)

392

405

 

393

 

; WARNING: Do not replacee (cadr form) by fn below.  These can differ!  Fn is

394

 

; passed to output-types-for-declare-form in order to get its 'stobjs-out, but

 

406

; WARNING: Do not replace (cadr form) by fn below.  These can differ!  Fn is

 

407

; passed to output-type-for-declare-form in order to get its 'stobjs-out, but

395

408

; (cadr form) can be the *1* function for fn.  The mistaken placement of fn

396

409

; below caused a factor of 4 slowdown in GCL in the first lemma5 in

397

410

; books/unicode/utf8-decode.lisp, because the proclaim for function

483

496

               (defun-one-output

484

497

                (eval-or-print (make-defun-declare-form (cadr form)

485

498

                                                        form

486

 

                                                        '(t))

 

499

                                                        '(values t))

487

500

                               stream)

488

501

                nil)

489

502

               (otherwise nil)))

788

801

                  (list 'ev-fncall-guard-er

789

802

                        'funny-fn

790

803

                        ,(cons 'list 'funny-args)

791

 

                        (guard 'funny-fn nil (w *the-live-state*))

 

804

                        (untranslate* (guard 'funny-fn nil (w *the-live-state*))

 

805

                                      t

 

806

                                      (w *the-live-state*))

792

807

 

793

808

; We assume that the primitives don't take state.

794

809

 

• Older »

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