Greetings, and thanks!
Matt Kaufmann <[EMAIL PROTECTED]> writes:
> Howdy --
>
> When using ACL2's proclaiming we get the following, for example (just start up
> /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2 and then :q):
>
> ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-ARG-TYPES)
>
> (T T T (UNSIGNED-BYTE 28) T T T T T T T T T T T T)
>
> ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-RETURN-TYPE)
>
> (VALUES T T)
>
> ACL2>
>
> Using GCL's proclaiming instead (using
> /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2) we get:
>
> ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-ARG-TYPES)
>
> (T T T (INTEGER 0 268435455) T T T T T T T T T T T T)
>
> ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-RETURN-TYPE)
>
> *
>
> ACL2>
>
> So the arg types came out the same. I think you said that any VALUES type is
> treated the same as *, so perhaps we can treat the result types as being "the
> same".
I'm working on a better mv call, so I am interested in cases where I
show * and you show something else. Right now they are equivalent
performance-wise.
I know the reason for most of my '* returns -- there are several
hundred legacy C functions without signature in GCL, and when these
appear in a return position of any function, '* propagates upward.
What might be kind of cool about the current implementation, is that
say one has found such a function, redefines it in lisp and compiles
it, all recursive callers are updated at once!
What also might be of use is that GCL keeps a complete call graph/tree
hierarchy which makes for useful flow analysis. Functions which are
called most frequently (in terms of source lines of code) are easily
determined, as are the most important '*s to fix.
Here for example is how to print out gcl's proclaims list:
(in-package 'si)
(let ((h (make-hash-table :test 'equal)))
(maphash (lambda (x y)
(let ((z (or (gethash (call-sig y) h)
(setf (gethash (call-sig y) h) (list (call-sig y)
nil)))))
(pushnew x (cadr z)))) *call-hash-table*)
(maphash (lambda (x y) (princ `(proclaim (ftype (function
,@y))))(terpri)) h))
Other useful functions here:
(function-src 'foo)
(recompile 'foo)
(call-callees (gethash 'foo *call-hash-table*))
(call-callers (gethash 'foo *call-hash-table*))
(all-callees 'foo nil)
(all-callers 'foo nil)
and, while you might have missed the email, for mutually recursive
functions 'foo and 'bar
(compile (convert-to-state 'foo))
makes them mutually tail-recursive where possible, like in scheme.
Take care,
>
> I could run a test that every type declaration in acl2-proclaims.lisp (used by
> for the first version above) is the same as the type declaration from GCL (the
> second version above), where "same as" means that VALUES results are treated
> as
> * and UNSIGNED-BYTE (etc.) is expanded to INTEGER range types. Is that the
> right test, and if so, does it seem of interest?
>
Any light you can shed on this, especially of a general nature, is
most useful. Soon I'm going to commit an enlargement of
compiler::+useful-c-types+ which should give you identical integer
ranges as opposed to expanded ones at present. As you know, limiting
the expansion limits the expansion of propagated types too.
Take care,
> -- Matt
> Cc: [EMAIL PROTECTED], [EMAIL PROTECTED], gcl-devel@gnu.org
> From: Camm Maguire <[EMAIL PROTECTED]>
> Date: 24 Jun 2006 14:26:47 -0400
> X-SpamAssassin-Status: No, hits=-1.9 required=5.0
> X-UTCS-Spam-Status: No, hits=-215 required=200
>
> P.S. just a note in passing as before stated, it certainly appears
> that gcl and acl2 are both implementing very similar type inferencing
> logic. It would be great some day to consolidate.
>
> Take care,
>
> Matt Kaufmann <[EMAIL PROTECTED]> writes:
>
> > Good morning --
> >
> > Thank you for looking into this.
> >
> > I agree with Bob's answer:
> >
> > >> I think that you should regard any xargs declaration as
> > >> nothing more than a comment to be ignored.
> >
> > But just in case you're simply looking for some intuition about this
> (and since
> > I've written most of this reply already!), I'll send this along in case
> you
> > find it useful. (Feel free to ignore it!)
> >
> > Roughly speaking, the (declare (xargs :guard form)) syntax asserts that
> ACL2
> > expects form to be true whenever the function is called. More
> precisely, ACL2
> > is set up so that only when the above assertion is suitably proved, will
> ACL2
> > invoke Common Lisp to evaluate calls of the function whose arguments
> satisfy
> > the guard.
> >
> > However, Common Lisp itself will ignore such declare forms (that's Bob's
> point,
> > I think).
> >
> > In the case of aset1, the guard does imply that we have an
> (unsigned-byte 31).
> > Maybe that's what you were asking. The rest of this email justifies that
> > claim, but please don't feel obligated to read it, of course!
> >
> > In the definition of aset1 we find:
> >
> > #+acl2-loop-only
> > (declare (xargs :guard (and (array1p name l)
> > (integerp n)
> > (>= n 0)
> > (< n (car (dimensions name l))))))
> >
> > But the definition of array1p implies that (car (dimensions name l)) is
> less
> > than 2^31; hence from the above, so is n. Here are the relevant
> snippets of
> > code.
> >
> > (defun array1p (name l)
> > ....
> > (let ((header-keyword-list (cdr (assoc-eq :header l))))
> > .....
> > (let ((dimensions (cadr (assoc-keyword :dimensions
> header-keyword-list)))
> > .....
> > (and
> > .....
> > (integerp (car dimensions))
> > (integerp maximum-length)
> > (< 0 (car dimensions))
> > (< (car dimensions) maximum-length)
> > (<= maximum-length
> *maximum-positive-32-bit-integer*)
> > ....
> >
> > where:
> >
> > (defconst *maximum-positive-32-bit-integer*
> > (1- (expt 2 31)))
> >
> > (defun dimensions (name l)
> > .....
> > (cadr (assoc-keyword :dimensions
> > (cdr (header name l)))))
> >
> > (defun header (name l)
> > .....
> > (assoc-eq :header l))
> > .....
> >
> > -- Matt
> > Cc: [EMAIL PROTECTED], [EMAIL PROTECTED]
> > From: Camm Maguire <[EMAIL PROTECTED]>
> > Date: 24 Jun 2006 10:45:50 -0400
> > X-SpamAssassin-Status: No, hits=-1.9 required=5.0
> > X-UTCS-Spam-Status: No, hits=-225 required=200
> >
> > Greetings, and thanks! Am looking nto this but had one question. I
> > don't understand the (declare (xargs :guard ...)) syntax. Though
> > aset1 in axioms.lisp is declaimed with an (unsigned-byte 31) arg, this
> > declaration appears to be asserting an integer type. If you had any
> > illumination to spare, it would be most appreciated.
> >
> > Take care,
> >
> > Matt Kaufmann <[EMAIL PROTECTED]> writes:
> >
> > > P.S. I forgot to mention that in
> > >
> > > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
> > >
> > > I did the build with:
> > >
> > > ../build-acl2.jun23
> > >
> > > -- Matt
> > > From: Matt Kaufmann <[EMAIL PROTECTED]>
> > > Subject: [EMAIL PROTECTED]: Re: benchmarking]
> > > To: [EMAIL PROTECTED]
> > > CC: boyer, hunt
> > > Date: 23 Jun 2006 23:59:28 -0500
> > >
> > > Hi, Camm --
> > >
> > > I think that you asked for a comparison of runs using different
> proclaim
> > > approaches. The results are below. The third one didn't work, but
> I'll leave
> > > that directory around for now:
> > >
> > > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
> > >
> > > You're welcome to do what you will with it. Please let me know
> when I can
> > > delete it.
> > >
> > > ============================================================
> > >
> > > Using some sort of hybrid of ACL2 and GCL proclaims:
> > > /projects/hvg/ACL2/v3-0-hons/make-regression.log,
> > > 17438.565u 493.162s 5:02:49.31 98.6% 0+0k 0+0io 3pf+0w
> > > [Minor point: I think about 30 seconds of the above was from
> cleaning books,
> > > not necessary and hence skipped below.]
> > >
> > > ============================================================
> > >
> > > Using GCL proclaims only:
> > > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log,
> > > 17939.093u 560.419s 5:16:23.49 97.4% 0+0k 0+0io 0pf+0w
> > >
> > > ============================================================
> > >
> > > Using ACL2 proclaims only, with
> > > (setq compiler::*compiler-auto-proclaim* nil
> si::*disable-recompile* t):
> > > Build failed.
> > >
> > > Here's the first error I noticed in the log file,
> > > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log:
> > >
> > > .....
> > >
> > > Finished loading axioms.lisp
> > > ;; Compiling axioms.lisp.
> > > ;; End of Pass 1.
> > > ;; End of Pass 2.
> > > axioms.c: In function `LI268':
> > > axioms.c:19663: warning: initialization from incompatible pointer
> type
> > > axioms.c:19720: warning: assignment from incompatible pointer type
> > > axioms.c:19720: warning: passing arg 1 of `make_cons1' from
> incompatible pointer type
> > > axioms.c:19723: warning: initialization from incompatible pointer
> type
> > > axioms.c:19734: warning: assignment from incompatible pointer type
> > > axioms.c:19734: warning: passing arg 1 of `make_cons1' from
> incompatible pointer type
> > > axioms.c: In function `LI428':
> > > axioms.c:28102: warning: initialization from incompatible pointer
> type
> > > axioms.c: In function `L459':
> > > axioms.c:30000: warning: comparison is always true due to limited
> range of data type
> > > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
> Speed=3, (Debug quality ignored)
> > > ;; Finished compiling axioms.o.
> > > Loading axioms.o
> > >
> > > .....
> > >
> > > Then later (as mentioned in earlier email):
> > >
> > > .....
> > >
> > > Loading type-set-b.lisp
> > >
> > > Raw Lisp Break.
> > > Error in LET [or a callee]: Arg or result mismatch in call to
> TYPE-SET-BINARY-+-ALIST-ENTRY
> > >
> > > .....
> > >
> > > I don't really know how to investigate this further, so I don't
> plan to do
> > > anything further here.
> > >
> > > - -- Matt
> > > - ------- Start of forwarded message -------
> > > Date: 23 Jun 2006 22:48:13 -0500
> > > From: Matt Kaufmann <[EMAIL PROTECTED]>
> > > To: [EMAIL PROTECTED]
> > > CC: [EMAIL PROTECTED], [EMAIL PROTECTED]
> > > In-reply-to: <[EMAIL PROTECTED]> (message from
> > > Robert Boyer on Fri, 23 Jun 2006 12:59:55 -0500)
> > > Subject: Re: benchmarking
> > >
> > > [Sorry if you all get this twice; I can't tell if it was sent.]
> > >
> > > Hi, Bob --
> > >
> > > I completed the run shown here
> > > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log
> > > but I failed in the build as shown here
> > > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log
> > > where you'll see:
> > >
> > > Raw Lisp Break.
> > > Error in LET [or a callee]: Arg or result mismatch in call to
> TYPE-SET-BINARY-+-ALIST-ENTRY
> > >
> > > The latter was a run where I started with this change to the
> sources copied
> > > from /projects/hvg/ACL2/v3-0-hons/:
> > >
> > > ;;; #+GCL (setq si::*disable-recompile* t)
> > > ;;; Even more than the above:
> > > (setq compiler::*compiler-auto-proclaim* nil
> si::*disable-recompile* t)
> > >
> > > I have no idea what's wrong; maybe I'll take a look tomorrow.
> > >
> > > - - -- Matt
> > > Date: Fri, 23 Jun 2006 12:59:55 -0500
> > > From: Robert Boyer <[EMAIL PROTECTED]>
> > > CC: [EMAIL PROTECTED], [EMAIL PROTECTED]
> > >
> > > > I will leave /p/bin/xg untouched until I hear you are done
> > > > with it.
> > >
> > > Bob
> > > - ------- End of forwarded message -------
> > > ----------
> > >
> > >
> > >
> > >
> >
> > --
> > Camm Maguire [EMAIL
> PROTECTED]
> >
> ==========================================================================
> > "The earth is but one country, and mankind its citizens." --
> Baha'u'llah
> >
> >
> >
>
> --
> Camm Maguire [EMAIL
> PROTECTED]
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
>
>
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
_______________________________________________
Gcl-devel mailing list
Gcl-devel@gnu.org
http://lists.gnu.org/mailman/listinfo/gcl-devel
