[Gcl-devel] Re: si::proper-list type propagation

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

> Howdy --
> 
> Hmm... I wonder if perhaps you can infer the no-side-effects property
> automatically.
> 

Yes, this is the right way.  I only worry about function definition
and compilation order, and keeping the right info in .o files to be
loaded in a fresh image.  This goes back to the tension involed in
auto-proclaiming functions, which I think is a great idea -- we could
probably do this within defun.  Compiled references to as yet
undefined functions could just blindly place the variables on the C
stack as writted at safety 0 -- the intersection of the called
argument list and the defined argument list will be correctly passed
as long as all are of word-length size (i.e. 4 bytes on 32bit).  this
means no direct char variables between files, nor int on 64bit.  we
already have some restrictions on between file inline arguments.
these are defined in the compiler package:

(defconstant +c-global-arg-types+   `(fixnum)) ;FIXME (long-float short-float) 
later
(defconstant +c-local-arg-types+    (union +c-global-arg-types+ '(fixnum 
character long-float short-float)))
(defconstant +c-local-var-types+    (union +c-local-arg-types+ '(fixnum 
character long-float short-float integer)))


Take care,

> -- Matt
>    Cc: address@hidden, address@hidden, "Paul F. Dietz" <address@hidden>
>    From: Camm Maguire <address@hidden>
>    Date: 25 Feb 2006 14:27:26 -0500
>    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
>    X-UTCS-Spam-Status: No, hits=-232 required=180
> 
>    Greetings!
> 
>    Now that bignum circle-list support it in, I'm wondering about the
>    potential for propagating the si::proper-list type.  The killer of
>    course is that if virtually any function intervenese between the first
>    binding of a proper list and its use, that function could have made it
>    improper regardless of its argument list.  Safety requires some sort
>    of no-side-effects property to compiled functions, which should be
>    great for acl2.  Just thinking out loud here and making a note to
>    myself for the future.
> 
>    take care,
> 
>    Robert Boyer <address@hidden> writes:
> 
>    > After thinking quite a bit more about how to code NTH, I have simply 
> given
>    > up.
>    > 
>    > I just don't know how to handle the circular list case as efficiently as
>    > possible.  Something like the suggested code for LIST-LENGTH might help, 
> but
>    > I don't see how yet.  One could mark the list as in gbc, but I think that
>    > would not be tolerated by the users.  So what is a nondestructive but
>    > really fast way to tell where a circular list starts to circle?
>    > 
>    > Bob
>    > 
>    > 
> -------------------------------------------------------------------------------
>    > 
>    > 
>    > >From the ANSI doc (and implemented this was in GCL I think):
>    > 
>    >  (defun list-length (x)
>    >    (do ((n 0 (+ n 2))           ;Counter.
>    >         (fast x (cddr fast))    ;Fast pointer: leaps by 2.
>    >         (slow x (cdr slow)))    ;Slow pointer: leaps by 1.
>    >        (nil)
>    >      ;; If fast pointer hits the end, return the count.
>    >      (when (endp fast) (return n))
>    >      (when (endp (cdr fast)) (return (+ n 1)))
>    >      ;; If fast pointer eventually equals slow pointer,
>    >      ;;  then we must be stuck in a circular list.
>    >      ;; (A deeper property is the converse: if we are
>    >      ;;  stuck in a circular list, then eventually the
>    >      ;;  fast pointer will equal the slow pointer.
>    >      ;;  That fact justifies this implementation.)
>    >      (when (and (eq fast slow) (> n 0)) (return nil))))
>    > 
>    > 
>    > 
>    > 
>    > 
> 
>    -- 
>    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