[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]]
|
From: |
Camm Maguire |
|
Subject: |
[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]] |
|
Date: |
29 Jun 2006 17:38:11 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings, and thanks for noting this!
1) To iterate, basically all functions would need to be compiled at
least twice. We start with a return type of nil, and repeat until
consistency.
2) What about optional argument tail recursion? I.e. an optional
argument state function?
Take care,
Matt Kaufmann <address@hidden> writes:
> Hi --
>
> Regarding mutual recursion:
>
> I haven't followed all of the ongoing thread about compilation, so the
> following remarks may be off-base. But it seems to me unfortunate to require
> anything about argument or output correspondence in order to make type
> inferences about mutually recursive functions. In the case of ACL2, we mark
> mutually recursive function nests explicitly (search for "mutual-recursion" in
> the sources). So it would be easy for ACL2 to tell GCL which functions are
> mutually recursive, though I don't know if that's helpful to you or if it's a
> general enough solution for other Lisp users. So maybe instead of the "state"
> approach, you could just recompile when signatures change until you reach a
> fixed point (or just punt with * in signatures when some number of iterations
> is exceeded)?
>
> For example, the following ACL2 source functions are, I believe, mutually
> recursive, but they have very different signatures (and some return one value
> while others do not).
>
> (defun ev-fncall-rec-logical (fn args w big-n safe-mode gc-off latches
> hard-error-returns-nilp)
> ...)
> (defun ev-fncall-rec (fn args w big-n safe-mode gc-off latches
> hard-error-returns-nilp)
> ...)
> (defun ev-rec (form alist w big-n safe-mode gc-off latches
> hard-error-returns-nilp)
> ...)
> (defun ev-rec-lst (lst alist w big-n safe-mode gc-off latches
> hard-error-returns-nilp)
> ...)
> (defun ev-rec-acl2-unwind-protect (form alist w big-n safe-mode gc-off
> latches hard-error-returns-nilp)
> ...)
> (defun ev-fncall (fn args state latches hard-error-returns-nilp)
> ...)
> (defun ev (form alist state latches hard-error-returns-nilp)
> ...)
> (defun ev-lst (lst alist state latches hard-error-returns-nilp)
> ...)
> (defun ev-fncall-w (fn args w safe-mode gc-off hard-error-returns-nilp)
> ...)
> (defun ev-fncall-guard-er-msg (fn guard stobjs-in args w extra-msg)
> ...)
> (defun ev-fncall-guard-er (fn args w latches safep)
> ...)
> (defun ev-fncall-msg (val wrld)
> ...)
> (defun untranslate1 (term iff-flg binop-tbl preprocess-fn wrld)
> ...)
> (defun untranslate-cons1 (term binop-tbl preprocess-fn wrld)
> ...)
> (defun untranslate-cons (term binop-tbl preprocess-fn wrld)
> ...)
> (defun untranslate-if (term iff-flg binop-tbl preprocess-fn wrld)
> ...)
> (defun untranslate-into-case-clauses (key term iff-flg binop-tbl
> preprocess-fn
> wrld)
> ...)
> (defun untranslate-into-cond-clauses (term iff-flg binop-tbl preprocess-fn
> wrld)
> ...)
> (defun untranslate1-lst (lst iff-flg binop-tbl preprocess-fn wrld)
> ...)
>
> Thanks --
> -- Matt
> Cc: address@hidden, address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 29 Jun 2006 11:15:49 -0400
> X-SpamAssassin-Status: No, hits=-1.9 required=5.0
> X-UTCS-Spam-Status: No, hits=-115 required=200
>
> Greetings, and thanks so much for this very helpful and infomative
> comparison!
>
> I'm still going through this list, but regarding mutual recursion, I'd
> like to point out this session:
>
>
> =============================================================================
> cd v3-0-hons-gcl-proclaim
> ./saved_acl2
> GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43
> Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd)
> Binary License: GPL due to GPL'ed components: (BFD UNEXEC)
> Modifications of this banner must retain notice of a compatible license
> Dedicated to the memory of W. Schelter
>
> Use (help) to get some basic information on how to use GCL.
>
> Temporary directory for compiler files set to /tmp/
>
> ACL2 Version 3.0 built June 25, 2006 14:59:57.
> Copyright (C) 2006 University of Texas at Austin
> ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
> are welcome to redistribute it under certain conditions. For details,
> see the GNU General Public License.
>
> Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
> MODIFIED for hons and such.
>
> See the documentation topic note-3-0 for recent changes.
> Note: We have modified the prompt in some underlying Lisps to further
> distinguish it from the ACL2 prompt.
>
> NOTE!! Proof trees are disabled in ACL2. To enable them in emacs,
> look under the ACL2 source directory in interface/emacs/README.doc;
> and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
> command loop. Look in the ACL2 documentation under PROOF-TREE.
>
> ACL2 Version 3.0. Level 1. Cbd
> "/v/filer3/projects-hunt/hvg/ACL2/v3-0-hons-gcl-proclaim/".
> Type :help for help.
> Type (good-bye) to quit completely out of ACL2.
>
> ACL2 !>:q
>
> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
> ACL2>(in-package 'si)
>
> #<"SYSTEM" package>
>
> SYSTEM>(maphash (lambda (x y)
> (when (eq '* (cadr (call-sig y)))
> (let* ((e (all-callees x nil))
> (r (all-callers x nil))
> (i (intersection e r)))
> (when (and (remove x i)
> (every (lambda (z) (equal (call-sig
> (gethash z
> *call-hash-table*)) (call-sig y))) i))
> (print (list x i)))))) *call-hash-table*)
>
> (ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
> (ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
> (ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST))
> (ACL2::GET-INDUCTION-CANDS-LST
> (ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST))
> (ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF))
> (ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF))
> (ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC))
> (ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST))
> (ACL2::MEMBER-TERM (ACL2::MEMBER-COMPLEMENT-TERM ACL2::MEMBER-TERM))
> (ACL2::MEMBER-COMPLEMENT-TERM
> (ACL2::MEMBER-TERM ACL2::MEMBER-COMPLEMENT-TERM))
> NIL
>
> SYSTEM>(call-sig (gethash 'acl2::member-term *call-hash-table*))
>
> ((T T) *)
>
> SYSTEM>(convert-to-state 'acl2::member-term)
>
> ACL2::MEMBER-TERM4313
>
> SYSTEM>(function-src 'ACL2::MEMBER-TERM4313)
>
> (LAMBDA (ACL2::LIT ACL2::CL STATE)
> (DECLARE (FIXNUM STATE))
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK ACL2::MEMBER-TERM4313
> (MACROLET
> ((ACL2::MEMBER-COMPLEMENT-TERM (ACL2::LIT ACL2::CL)
> (LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 0))
> (ACL2::MEMBER-TERM (ACL2::LIT ACL2::CL)
> (LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 1)))
> (CASE STATE
> (0
> (FUNCALL (LAMBDA (ACL2::LIT ACL2::CL)
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK ACL2::MEMBER-COMPLEMENT-TERM
> (LET* ()
> (IF (ATOM ACL2::LIT)
> (ACL2::MEMBER-COMPLEMENT-TERM1 ACL2::LIT
> ACL2::CL)
> (IF (EQ 'QUOTE (CAR ACL2::LIT))
> (ACL2::MEMBER-COMPLEMENT-TERM1
> ACL2::LIT ACL2::CL)
> (IF (LET
> ((#:G15388
> (EQ (CAR ACL2::LIT) 'EQUAL)))
> (IF #:G15388 #:G15388
> (EQ (CAR ACL2::LIT) 'ACL2::IFF)))
> (ACL2::MEMBER-COMPLEMENT-TERM2
> (CAR ACL2::LIT)
> (CAR (CDR ACL2::LIT))
> (CAR (CDR (CDR ACL2::LIT)))
> ACL2::CL)
> (IF (EQ (CAR ACL2::LIT) 'NOT)
> (ACL2::MEMBER-TERM
> (CAR (CDR ACL2::LIT)) ACL2::CL)
> (ACL2::MEMBER-COMPLEMENT-TERM1
> ACL2::LIT ACL2::CL))))))))
> ACL2::LIT ACL2::CL))
> (OTHERWISE
> (FUNCALL (LAMBDA (ACL2::LIT ACL2::CL)
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK ACL2::MEMBER-TERM
> (LET* ()
> (BLOCK ACL2::MEMBER-TERM
> (LET* ()
> (IF (ATOM ACL2::LIT)
> (ACL2::MEMBER-EQ ACL2::LIT ACL2::CL)
> (IF (EQ 'QUOTE (CAR ACL2::LIT))
> (ACL2::MEMBER-EQUAL ACL2::LIT
> ACL2::CL)
> (IF
> (LET
> ((#:G15387
> (EQ (CAR ACL2::LIT) 'EQUAL)))
> (IF #:G15387 #:G15387
> (EQ (CAR ACL2::LIT) 'ACL2::IFF)))
> (ACL2::MEMBER-TERM2
> (CAR ACL2::LIT)
> (CAR (CDR ACL2::LIT))
> (CAR (CDR (CDR ACL2::LIT)))
> ACL2::CL)
> (IF (EQ (CAR ACL2::LIT) 'NOT)
> (ACL2::MEMBER-COMPLEMENT-TERM
> (CAR (CDR ACL2::LIT)) ACL2::CL)
> (ACL2::MEMBER-EQUAL ACL2::LIT
> ACL2::CL))))))))))
> ACL2::LIT ACL2::CL))))))
> NIL
> ACL2::MEMBER-TERM4313
>
> SYSTEM>(compile 'ACL2::MEMBER-TERM4313)
>
> ;; Compiling /tmp/gazonk_7059_0.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_7059_0.o.
> Loading /tmp/gazonk_7059_0.o
> Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T
> (INTEGER -2147483648
> 2147483647))
> T), recompiling
> ACL2::MEMBER-COMPLEMENT-TERM
> Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T
> (INTEGER -2147483648
> 2147483647))
> T), recompiling
> ACL2::MEMBER-TERM
> ;; Compiling /tmp/gazonk_7059_ymjCh7.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_7059_ymjCh7.o.
> Loading /tmp/gazonk_7059_ymjCh7.o
> start address -T 0xadd8f58 Finished loading /tmp/gazonk_7059_ymjCh7.o
> Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
> recompiling ACL2::SOME-ELEMENT-MEMBER-COMPLEMENT-TERM
> Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
> recompiling ACL2::ADD-LITERAL
> Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
> recompiling ACL2::ADD-LITERAL-AND-PT
> ;; Compiling /tmp/gazonk_7059_sxyINA.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_7059_sxyINA.o.
> Loading /tmp/gazonk_7059_sxyINA.o
> start address -T 0xadda7a0 Finished loading /tmp/gazonk_7059_sxyINA.o
> start address -T 0xadc24e0 Finished loading /tmp/gazonk_7059_0.o
> #<compiled-function ACL2::MEMBER-TERM4313>
> NIL
> NIL
>
> SYSTEM>
>
> =============================================================================
>
> The questions are:
>
> 1) what is the proper mutual recursion detection mechanism --
> i.e. if we only require that the arg types of the mutual recursion
> members match, then we get the following list:
>
> (ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF
> (ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST
> ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF))
> (ACL2::DISTRIBUTE-FIRST-IF
> (ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF ACL2::NORMALIZE
> ACL2::NORMALIZE-LST))
> (ACL2::NORMALIZE
> (ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST
> ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF))
> (ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
> (ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
> (ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC
> (ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC-LIST
> ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC))
> (ACL2::TS-INTERSECTION-FN
> (ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN
> ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN))
> (ACL2::TS-UNION-FN
> (ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN
> ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN))
> (ACL2::EVAL-TYPE-SET
> (ACL2::TS-UNION-FN ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN
> ACL2::EVAL-TYPE-SET-LST))
> (ACL2::CONTAINS-CONSTRAINED-CONSTANTP
> (ACL2::CONTAINS-CONSTRAINED-CONSTANTP
> ACL2::CONTAINS-CONSTRAINED-CONSTANTP-LST))
> (ACL2::FREE-OR-BOUND-VARS
> (ACL2::FREE-OR-BOUND-VARS-LST ACL2::FREE-OR-BOUND-VARS))
> (COMPILER::T1EXPR (COMPILER::T1ORDINARY COMPILER::T1EXPR))
> (ACL2::FFNNAMES-SUBSETP
> (ACL2::FFNNAMES-SUBSETP ACL2::FFNNAMES-SUBSETP-LISTP))
> (ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST))
> (ACL2::GET-INDUCTION-CANDS-LST
> (ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST))
> (ACL2::ALMOST-QUOTEP1
> (ACL2::ALMOST-QUOTEP1-LISTP ACL2::ALMOST-QUOTEP1))
> (ACL2::MULT-RELIEVE-FC-HYPS
> (ACL2::MULT-RELIEVE-FC-HYPS ACL2::MULT-RELIEVE-ALL-FC-HYPS))
> (ACL2::FIND-FIRST-NON-LOCAL-NAME
> (ACL2::FIND-FIRST-NON-LOCAL-NAME-LST
> ACL2::FIND-FIRST-NON-LOCAL-NAME))
> (ACL2::ALL-CALLS (ACL2::ALL-CALLS-LST ACL2::ALL-CALLS))
> (ACL2::FFNNAMEP-MOD-MBE
> (ACL2::FFNNAMEP-MOD-MBE-LST ACL2::FFNNAMEP-MOD-MBE))
> (ACL2::EV-REC
> (ACL2::EV-REC-ACL2-UNWIND-PROTECT ACL2::EV-REC ACL2::EV-REC-LST
> ACL2::EV-FNCALL-REC ACL2::EV-FNCALL-REC-LOGICAL))
> (ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF))
> (ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF))
> (ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC))
> (ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST))
> (ACL2::COLLECT-FFNNAMES
> (ACL2::COLLECT-FFNNAMES-LST ACL2::COLLECT-FFNNAMES))
>
>
> =============================================================================
> SYSTEM>(mapcar (lambda (x) (call-sig (gethash x *call-hash-table*)))
> '(ACL2::NOTE-CERTIFICATION-WORLD ACL2::NOTE-CERTIFICATION-WORLD-LST))
>
> (((T T T T T T) *) ((T T T T T T) (VALUES T T T)))
>
> SYSTEM>(compile (convert-to-state 'ACL2::NOTE-CERTIFICATION-WORLD))
>
> ;; Compiling /tmp/gazonk_7059_0.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_7059_0.o.
> Loading /tmp/gazonk_7059_0.o
> Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T
> T
> (INTEGER
> -2147483648
> 2147483647))
> (VALUES T T
> T)),
> recompiling ACL2::NOTE-CERTIFICATION-WORLD
> Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T
> T
> (INTEGER
> -2147483648
> 2147483647))
> (VALUES T T
> T)),
> recompiling ACL2::NOTE-CERTIFICATION-WORLD-LST
> ;; Compiling /tmp/gazonk_7059_8mFHt7.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_7059_8mFHt7.o.
> Loading /tmp/gazonk_7059_8mFHt7.o
> start address -T 0xadc2710 Finished loading /tmp/gazonk_7059_8mFHt7.o
> start address -T 0xadbd000 Finished loading /tmp/gazonk_7059_0.o
> #<compiled-function ACL2::NOTE-CERTIFICATION-WORLD4331>
> NIL
> NIL
>
>
> =============================================================================
>
> 2) How does one unwind the state function when any of its elements are
> redefined? At one point I was thinking of passing the state
> integer straight from the caller and relying on the existing
> fast-link redirect mechanism to redeirect the call to the newly
> redefined function from the compiled code of the caller -- this
> however misses all the implicit calls from the other members of the
> mutual recursion group, as they are now just wrappers to a
> self-recursive state function. Now I'm thinking the cleanest
> solution is to simply redefine all the group members when any one
> of them are redefined.
>
> More explicitly:
>
> (defun foo (x) (unless (< x 0) (not (bar (1- x)))))
> (defun bar (x) (unless (< x 0) (not (foo (1- x)))))
>
> convert-to-state ->
>
> (defun foo4351 (X STATE)
> (DECLARE (FIXNUM STATE))
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK FOO4351
> (MACROLET
> ((BAR (X) (LIST 'FOO4351 X 0)) (FOO (X) (LIST 'FOO4351 X 1)))
> (CASE STATE
> (0
> (FUNCALL (LAMBDA (X)
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK BAR
> (LET* ()
> (IF (NOT (< X 0)) (PROGN (NOT (FOO (- X 1))))))))
> X))
> (OTHERWISE
> (FUNCALL (LAMBDA (X)
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (DECLARE (OPTIMIZE (SAFETY 0)))
> (BLOCK FOO
> (LET* ()
> (BLOCK FOO
> (LET* ()
> (IF (NOT (< X 0))
> (PROGN (NOT (BAR (- X 1))))))))))
> X))))))
>
> (defun foo (X) (BLOCK FOO (FOO4351 X 1)))
> (defun bar (X) (BLOCK BAR (FOO4351 X 0)))
>
> If then any of foo or bar are redefined, the other one needs to be
> redefined to its origianl source.
>
> Eventually this should be an automatic part of do-recompile.
>
> I don't know if any performance sensitive code of yours is in this
> form, but if so this should definitely be an improvement. Tha takr
> benchmark is dramatically accelerated.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > Howdy --
> >
> > Attached is a file that I used to explore discrepancies between ACL2 and
> GCL in
> > auto-generation of function type declarations. You probably don't need
> to look
> > at it unless you want to tweak it to get a more refined comparison (I
> don't
> > think I'll have time to do more of this for awhile but I can add
> comments to
> > the code and/or answer questions if you want to play with the code) or
> see
> > detailed results -- I'll summarize key things of interest to you just
> below.
> >
> > First, here's the most interesting thing I found: a compiler bug that
> appears
> > to be due to a mistaken automatic proclaim involving
> multiple-value-prog1.
> >
> > sundance:~> /p/bin/xg
> > GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43
> > Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd)
> > Binary License: GPL due to GPL'ed components: (BFD UNEXEC)
> > Modifications of this banner must retain notice of a compatible license
> > Dedicated to the memory of W. Schelter
> >
> > Use (help) to get some basic information on how to use GCL.
> >
> > Temporary directory for compiler files set to /tmp/
> >
> > >(defun buggy ()
> > (multiple-value-prog1
> > (values 3 4)
> > 5))
> >
> > BUGGY
> >
> > >(buggy)
> >
> > 3
> > 4
> >
> > >(compile 'buggy)
> >
> > ;; Compiling /tmp/gazonk_25691_0.lsp.
> > ;; End of Pass 1.
> > ;; End of Pass 2.
> > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> > ;; Finished compiling /tmp/gazonk_25691_0.o.
> > Loading /tmp/gazonk_25691_0.o
> > start address -T 0xac70fe0 Finished loading /tmp/gazonk_25691_0.o
> > #<compiled-function BUGGY>
> > NIL
> > NIL
> >
> > >(buggy)
> >
> > 3
> >
> > >(get 'buggy 'si:proclaimed-return-type)
> >
> > T
> >
> > >
> >
> > The only other thing you are likely to find interesting is the
> following, where
> > I suspect that the return type could also correctly be deduced as T
> rather than
> > as the weaker *.
> >
> > (compile (defun weak (name) (setf (get name 'abc) nil)))
> >
> > ;; Compiling /tmp/gazonk_25691_0.lsp.
> > ;; End of Pass 1.
> > ;; End of Pass 2.
> > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> > ;; Finished compiling /tmp/gazonk_25691_0.o.
> > Loading /tmp/gazonk_25691_0.o
> > start address -T 0xac795d8 Finished loading /tmp/gazonk_25691_0.o
> > #<compiled-function WEAK>
> > NIL
> > NIL
> >
> > >(get 'weak 'si:proclaimed-return-type)
> >
> > *
> >
> > >
> >
> > Note that I deliberately coerced every declaration that implies fixnum
> into
> > simply 'fixnum for purposes of limiting discrepancies to interesting
> cases. So
> > for example, if ACL2 deduced an type of (integer 0 1000) for some
> function
> > argument and GCL had (signed-byte 28) for thta same argument, then this
> would
> > not be considered a discrepancy (both would be treated as fixnum).
> >
> > Most of the file is the analysis of input type discrepancies (see
> "Resulting
> > value of *args-mismatches*:") and output type discrepancies (see
> "Resulting
> > value of *output-mismatches*:"). Here are the parts of that that I
> think you
> > might find a little interesting, but there's nothing else major.
> >
> > + Many are marked with "; Mutual recursion", meaning that GCL made a
> weaker
> > inference than ACL2, but the function is mutually recursive with others
> > (specifically, defined using (mutual-recursion (defun ...) (defun ...)
> ...)
> > in the ACL2 sources), so maybe this isn't news to you.
> >
> > + Many are marked with "GCL is missing STRING declaration (maybe not
> > important?)", or substitute other types for STRING. My guess on an
> > explanation is that you simply don't bother inferring types that don't
> do the
> > compiler any good.
> >
> > + There is a bug in the ACL2 3.0 sources, since fixed (thanks to Bob
> Boyer),
> > such that functions calling intern (or functions calling THOSE
> functions,
> > etc.) are returning two values instead of the intended single value.
> > Mismatches due to this bug are marked with "[Intern]" and are probably
> of no
> > interest to you.
> >
> > + In a few cases GCL gets a type where ACL2 does not (marked with "GCL
> nicely
> > propagates where ACL2 does not:" or "Nice job by GCL").
> >
> > + One GCL type inference was wrong due to the compiler bug mentioned
> early in
> > this email (search for "problem with multiple-value-prog1").
> >
> > + One GCL type inference was weak due to the weak handling of setf shown
> > earlier in this email.
> >
>
> --
> Camm Maguire address@hidden
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah