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

[Camm Maguire]

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