[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: |
12 Jul 2006 23:28:19 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings! Been thinking about this:
Matt Kaufmann <address@hidden> writes:
> Hi --
>
> Please see below.
>
> Cc: address@hidden, address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 29 Jun 2006 17:38:11 -0400
> X-SpamAssassin-Status: No, hits=-1.9 required=5.0
> X-UTCS-Spam-Status: No, hits=-125 required=200
>
> 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.
>
> That makes sense. I figure it's the price someone would pay for getting
> excellent automatic proclaims.
>
foo.lisp
(defun foo (x) (if (< x 0) 2 (bar (1- x))))
bar.lisp
(defun bar (x) (if (< x 0) 'bar (foo (1- x))))
If nil is the return type assumed for bar/foo during the compile of
foo/bar, then the compiled return type of foo is inferred as fixnum,
which means that it will return the address of whatever bar returns,
which is incorrect. Only when both functions are loaded nto the same
image can a recompile be triggered to set the return type of 'foo to
t, which means that there is a time during which 'foo is incorrectly
compiled. More simply, such is the case if only foo is compiled and
'bar is interpreted.
So I don't see how we can safely deduce mutually recursive return
types away from '* until both compiled functions are loaded int the
same image. At that point, I suppose we could iterate setting all
members of the group to nil at first as opposed to the state function
approach, but I don't see what this gains over the state function.
> 2) What about optional argument tail recursion? I.e. an optional
> argument state function?
>
> Sorry; I'm afraid I don't understand the question.
>
The big gain in the state function is that there is typically much tail
recursion produced. I've just modified GCL to allow tail recursion
with optional arguments, so in principle now the mutual recursion
members need not have the same signature to see this benefit.
Of course, one downside to the state function is that it might be
confusing.
Take care,
> Take care,
>
> Thanks --
> -- Matt
> 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
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
| [Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]],
Camm Maguire <=