Subject: [clisp-list] array-dimension-limit

From: [email-masked] (Wolfhard Buß)
Date: 30 Aug 2001 19:26:33 +0200

In CLISP 2.27 (released 2001-07-17) for x86-Linux

 most-positive-fixnum  evaluates to  16777215  and
 array-dimension-limit to 16777216

with a consequence

 (typep array-dimension-limit 'fixnum)
 => NIL 

that collides with CLHS, which describes array-dimension-limit as
'a positive _fixnum_, the exact magnitude of which is
implementation-dependent, but which is not less than 1024'.

Is a fix known?

Regards,
Wolfhard.

---

From: Sam Steingold <[email-masked]>
Date: 30 Aug 2001 14:14:01 -0400

> * In message <[email-masked]>
> * On the subject of "[clisp-list] array-dimension-limit"
> * Sent on 30 Aug 2001 19:26:33 +0200
> * Honorable [email-masked] (Wolfhard Buß) writes:
>

yes, we are aware of this.
there are some other constants which exhibit the same problem,
like ARRAY-TOTAL-SIZE-LIMIT.

this is a case of "what's your problem, is the bride too beautiful?"
CLISP does slightly more than is required - it supports arrays to the
full extent of the FIXNUM range, not just to some part of it.
we could, of course, decrease the value of the ARRAY-DIMENSION-LIMIT and
friends, but it would not buy you anything: you will just loose ability
to create arrays [0..MOST-POSITIVE-FIXNUM].

> Is a fix known?

what is your problem?

-- 
Sam Steingold (http://www.podval.org/~sds)
Support Israel's right to defend herself! <http://www.i-charity.com/go/israel>
Read what the Arab leaders say to their people on <http://www.memri.org/>
Someone has changed your life.  Save? (y/n)

---

From: Raymond Toy <[email-masked]>
Date: 30 Aug 2001 14:46:14 -0400

>>>>> "Sam" == Sam Steingold <[email-masked]> writes:

    Sam> this is a case of "what's your problem, is the bride too beautiful?"
    Sam> CLISP does slightly more than is required - it supports arrays to the
    Sam> full extent of the FIXNUM range, not just to some part of it.
    Sam> we could, of course, decrease the value of the ARRAY-DIMENSION-LIMIT and
    Sam> friends, but it would not buy you anything: you will just loose ability
    Sam> to create arrays [0..MOST-POSITIVE-FIXNUM].

With Clisp "2.27 (released 2001-07-17)..." on an Ultrasparc I get:

> (make-array (1+ most-positive-fixnum))
==>
*** - MAKE-ARRAY: dimension 16777216 is not of type `(INTEGER 0 (,ARRAY-DIMENSION-LIMIT))

So how do I make an array with indices [0..most-positive-fixnum]? 

    Sam> what is your problem?

I would say that in ansi mode, array-dimension-limit should be a
fixnum as the CLHS says.  Unless ansi mode really means "kind of ansi
but not always".

Ray

---

From: Sam Steingold <[email-masked]>
Date: 30 Aug 2001 17:37:14 -0400

> * In message <[email-masked]>
> * On the subject of "Re: [clisp-list] array-dimension-limit"
> * Sent on 30 Aug 2001 14:46:14 -0400
> * Honorable Raymond Toy <[email-masked]> writes:
>

I meant [0..most-positive-fixnum-1]
> So how do I make an array with indices [0..most-positive-fixnum]? 

I meant [0..most-positive-fixnum-1] for total size of
MOST-POSITIVE-FIXNUM:
> (length (make-array most-positive-fixnum))
16777215

ARRAY-TOTAL-SIZE-LIMIT is
 "The upper exclusive bound on the array total size of an array."
thus if ARRAY-TOTAL-SIZE-LIMIT == MOST-POSITIVE-FIXNUM, we cannot do
(make-array most-positive-fixnum)

thus the choice is
 (1) disable (make-array most-positive-fixnum)
 (2) break the standard by either
     - ARRAY-TOTAL-SIZE-LIMIT is not fixnum
     - ARRAY-TOTAL-SIZE-LIMIT is the inclusive, not exclusive bound.

I don't like any of the solutions.
Since the whole idea of ARRAY-TOTAL-SIZE-LIMIT being a fixnum is to
allow efficient arithmetics on array indexes and CLISP ignores type
declarations anyway, the current non-compliance should not matter.

-- 
Sam Steingold (http://www.podval.org/~sds)
Support Israel's right to defend herself! <http://www.i-charity.com/go/israel>
Read what the Arab leaders say to their people on <http://www.memri.org/>
A man paints with his brains and not with his hands.

---

From: Raymond Toy <[email-masked]>
Date: 30 Aug 2001 17:48:38 -0400

>>>>> "Sam" == Sam Steingold <[email-masked]> writes:

[weird stuttering deleted]

    Sam> ARRAY-TOTAL-SIZE-LIMIT is
    Sam>  "The upper exclusive bound on the array total size of an array."
    Sam> thus if ARRAY-TOTAL-SIZE-LIMIT == MOST-POSITIVE-FIXNUM, we cannot do
    Sam> (make-array most-positive-fixnum)

    Sam> thus the choice is
    Sam>  (1) disable (make-array most-positive-fixnum)
    Sam>  (2) break the standard by either
    Sam>      - ARRAY-TOTAL-SIZE-LIMIT is not fixnum
    Sam>      - ARRAY-TOTAL-SIZE-LIMIT is the inclusive, not exclusive bound.

CMUCL does (1).  But then it can't allocate 2 GB of data (for 32-bit
elements) anyway.  (Well, you can on x86 FreeBSD where that's the max
heap size, so you couldn't do much after you've allocated the data.)

    Sam> I don't like any of the solutions.
    Sam> Since the whole idea of ARRAY-TOTAL-SIZE-LIMIT being a fixnum is to
    Sam> allow efficient arithmetics on array indexes and CLISP ignores type
    Sam> declarations anyway, the current non-compliance should not matter.

Fair enough.  I've never had a reason to use an array of that size and
even if I did, I probably couldn't wait long enough for the program to
finish.... :-) So lopping off one single element won't bother me at
all.

On a side note, how does Clisp represent fixnums?  Are they boxed up? 

Ray

---

From: Sam Steingold <[email-masked]>
Date: 30 Aug 2001 18:22:24 -0400

> * In message <[email-masked]>
> * Sent on 30 Aug 2001 17:48:38 -0400
> I've never had a reason to use an array of that size and even if I
> did, I probably couldn't wait long enough for the program to

[3]> (time (= most-positive-fixnum (length (make-array most-positive-fixnum))))
Real time: 0.671 sec.
Run time: 0.650936 sec.
Space: 67108868 Bytes
GC: 1, GC time: 0.0100144 sec.
t
[4]>

fast enough for me.

> On a side note, how does Clisp represent fixnums?  Are they boxed up? 

no, fixnums (and some other things, like chars) are immediate.
(CLISP has 24 bit fixnums.)

-- 
Sam Steingold (http://www.podval.org/~sds)
Support Israel's right to defend herself! <http://www.i-charity.com/go/israel>
Read what the Arab leaders say to their people on <http://www.memri.org/>
When we break the law, they fine us, when we comply, they tax us.

---

From: [email-masked] (Wolfhard Buß)
Date: 31 Aug 2001 13:06:13 +0200

> declarations anyway, the current non-compliance should not matter.

There is at least one piece of software, i.e. ACL2, that depends on

 (typep array-total-size-limit 'fixnum)
 => T

So I would like to 'disable (make-array most-positive-fixnum)', to make
clisp's ansi mode a bit more ansi compliant.

I am interested in patches for clisp 2.27 to achieve this. 

Regards,
Wolfhard

---

From: Sam Steingold <[email-masked]>
Date: 31 Aug 2001 11:23:41 -0400

> * In message <[email-masked]>
> * Sent on 31 Aug 2001 13:06:13 +0200

what is ACL2?
how does it depend on this?
could you please provide sources and the error message from CLISP?

-- 
Sam Steingold (http://www.podval.org/~sds)
Support Israel's right to defend herself! <http://www.i-charity.com/go/israel>
Read what the Arab leaders say to their people on <http://www.memri.org/>
All generalizations are wrong.  Including this.

---

From: [email-masked] (Wolfhard Buß)
Date: 31 Aug 2001 15:34:50 +0200

Regards,
Wolfhard

---

From: Raymond Toy <[email-masked]>
Date: 31 Aug 2001 11:11:03 -0400

>>>>> "Wolfhard" == Wolfhard Buß <[email-masked]> writes:

    >> declarations anyway, the current non-compliance should not matter.

    Wolfhard> There is at least one piece of software, i.e. ACL2, that depends on

    Wolfhard>  (typep array-total-size-limit 'fixnum)
    Wolfhard>  => T

Why does it care and what is ACL2?

I have to say I don't understand why any piece of code (other than the
lisp internals) would really care that array-total-size-limit is or is
not a fixnum.

Ray

---

From: [email-masked] (Wolfhard Buß)
Date: 31 Aug 2001 19:40:14 +0200

Raymond Toy <[email-masked]> writes:

>     Wolfhard> There is at least one piece of software, i.e. ACL2,
>     Wolfhard> that depends on
> 

ACL2: 'A Computational Logic for Applicative Common Lisp' [1] is 'An
Industrial Strength Theorem Prover for a Logic Based on Common Lisp' [2],
a small applicative subset of CLtL2.
ACL2 is an automated reasoning system used to verify Hardware and Software
systems.
bignums are not a data type in ACL and because of the close connection
between ACL and the underlying Common Lisp there is no place for arrays 
with possibly bignum elements.  No place in a formal language which is
the base of a logic.

The implementation depends on the fixnum array-total-size-limit. It's
probably conceptually impossible to change this. 

Fixing clisp's ansi mode is the way to go.

You may look at the sources yourself.

Regards,
Wolfhard

Footnotes: 
[1]  http://www.cs.utexas.edu/users/moore/acl2/

[2]  http://www.cs.utexas.edu/users/moore/publications/

---

From: Raymond Toy <[email-masked]>
Date: 31 Aug 2001 14:25:27 -0400

>>>>> "Wolfhard" == Wolfhard Buß <[email-masked]> writes:

    Wolfhard> Raymond Toy <[email-masked]> writes:
    Wolfhard> There is at least one piece of software, i.e. ACL2,
    Wolfhard> that depends on
    >> lisp internals) would really care that array-total-size-limit is or is

    Wolfhard> bignums are not a data type in ACL and because of the close connection
    Wolfhard> between ACL and the underlying Common Lisp there is no place for arrays 
    Wolfhard> with possibly bignum elements.  No place in a formal language which is
    Wolfhard> the base of a logic.

I don't understand how arrays with bignum elements is related to
array-total-size-limit not being a fixnum.  Do you mean arrays with a
bignum number of elements?

    Wolfhard> The implementation depends on the fixnum array-total-size-limit. It's
    Wolfhard> probably conceptually impossible to change this. 

But why?  Why not just delete the offending code in ACL2 that figures
out that array-total-size-limit is not a fixnum?

    Wolfhard> Fixing clisp's ansi mode is the way to go.

    Wolfhard> You may look at the sources yourself.

Thanks for the reference, but it's very unlikely that I will.

Ray

---

From: [email-masked] (Don Cohen)
Date: Fri, 31 Aug 2001 15:15:07 -0700

> You may look at the sources yourself.
 ...
 > [2]  http://www.cs.utexas.edu/users/moore/publications/

Obviously I have not read the sources since you posted this.
I have enjoyed reading the tutorials and some other doc, though.
I don't see anything about fixnums at all in the doc.
In fact "numbers" are described as rationals or complex rationals.

Of course, the doc also lists a number of common lisp implementations 
in which acl2 runs and the list does not include clisp!
So I guess you must be trying to extend that list.  In which case it's
not all that surprising that some code might have be to changed.
I bet if you ask the authors of acl2 they can tell you what's the best
thing to change.  I can believe that they won't want to change acl2 in
order to comply with the failure of a lisp implementation to conform
to ansi, but I'd be surprised if they haven't had to do this already
for most of the other implementations on the list.

---

From: [email-masked] (Wolfhard Buß)
Date: Sat Sep 1 04:17:05 2001

> bignum number of elements?
 
You're right, (= array-total-size-limit (1+ most-positive-fixnum)) implies that
indices are fixnum, and that shouldn't be an issue in a system for reasoning 
about ACL expressions without bignums. 

> out that array-total-size-limit is not a fixnum?

Why not fixing clisp's ansi mode? :)

Wolfhard

---

From: [email-masked] (Wolfhard Buß)
Date: Sat Sep 1 04:17:06 2001

> In fact "numbers" are described as rationals or complex rationals.

Right. Rationals are described with integers. Integers are currently
implemented as a subset of the fixnums of the underlying Common Lisp.

BTW, acl2r implements reals as nonstandard-reals.

Wolfhard

---

From: [email-masked] (Don Cohen)
Date: Sat Sep 1 09:12:06 2001

> implemented as a subset of the fixnums of the underlying Common Lisp.
I don't understand where fixnums enter the picture at all.
I'd expect that acl would use the type integer, not fixnum.
This is better for most purposes related to logic, since you prefer to
reason about integers rather than fixnums.  I'd find it hard to
believe, for instance, that arrays are not allowed to hold arbitrary
integers.

 > >     Wolfhard> bignums are not a data type in ACL and because of
         the close connection 

I agree that bignums should not be a data type in ACL, but for the
same reason, neither should fixnums.  Integers should be the type used
in either case.  (For instance, integers are closed under addition, 
while bignums and fixnums are not.)  Of course, having not read or
written the code, I don't know for sure what is implemented.  
I'm only arguing about what makes sense.  
(But I'm also willing to bet that this is what is implemented.)

 > >     Wolfhard> probably conceptually impossible to change this. 
Do you have any evidence of that?
Perhaps you're just getting an error from clisp because something is
checking the type of an array size.  Perhaps just changing the type
from fixnum to integer would solve the problem.

 > Why not fixing clisp's ansi mode? :)
Clearly this problem can be fixed in different places.  If you can
find some compelling arguments for NOT changing the application (ACL)
then I'd like to hear them.  I've not heard any so far.
The main argument for changing the application in this case is that
it would extend the range of the application (which would then be able
to deal with new cases, while still dealing with all of the old ones),
whereas changing the lisp implementation (at least in the easy way of
simply decreasing the array index limit) would have the reverse effect
of making the lisp implementation no longer handle cases that it could
before, without enabling it to deal with any new cases.

---

From: [email-masked] (Wolfhard Buß)
Date: Mon Sep 3 06:09:03 2001

I wrote:

> Integers are currently implemented as a subset of the fixnums of
> the underlying Common Lisp.

Nonsense. ACL2 integers are the _integers_ of the underlying CL.
Apologies for the confusion.

[email-masked] (Don Cohen) writes:

> I'd find it hard to believe, for instance, that arrays are not
> allowed to hold arbitrary integers.

I was talking about indices.
The immutable applicative one or two-dimensional arrays of ACL2
may hold arbitrary objects.

>  Wolfhard> The implementation depends on the fixnum
>  Wolfhard> array-total-size-limit. It's 
 
> Do you have any evidence of that?

 (or (typep array-dimension-limit 'fixnum)
     (error "We assume that ARRAY-DIMENSION-LIMIT is a fixnum.  CLTL2 ~
             requires this.  ACL2 will not work in this Common Lisp."))

>  Raymond> But why?  Why not just delete the offending code in ACL2 that
>  Raymond> figures out that array-total-size-limit is not a fixnum?

>  Wolfhard> Why not fixing clisp's ansi mode? :)

> then I'd like to hear them.  I've not heard any so far.

Work. Economy. Fix clisp's ansi mode, and I don't have to change the
application wrt array-dimension-limit and the community is happy 
because of clisp with ansi mode.

However, thanks for responding.

Wolfhard

---

From: [email-masked] (Don Cohen)
Date: Mon Sep 3 08:03:01 2001

> Apologies for the confusion.
Good.  As I expected.

 >              requires this.  ACL2 will not work in this Common Lisp."))

This is not very good evidence that it's conceptually hard to change.
You might, for instance, comment out the error and see what goes
wrong.  Or you might just ask the authors of acl2 what would have
to be fixed to generalize this fixnum to integer.

 > because of clisp with ansi mode.
Conversely, fix acl2 and you don't have to fix clisp.  This argument 
doesn't seem to favor one over the other.
I admit that I'd expect it to be easy to change clisp, and you could 
certainly do this on your own local copy.  But I'd also expect that
acl2 would be easy to fix, and that would be preferable for the reason
in my last message.

---

From: Christophe Rhodes <[email-masked]>
Date: Mon Sep 3 08:12:01 2001

> doesn't seem to favor one over the other.

Oh, yes it does.

Standards-compliance in a mode that aims to be standard-compliant is a
good thing.

Christophe
-- 
Jesus College, Cambridge, CB5 8BL                           +44 1223 510 299
http://www-jcsu.jesus.cam.ac.uk/~csr21/                  (defun pling-dollar 
(str schar arg) (first (last +))) (make-dispatch-macro-character #\! t)
(set-dispatch-macro-character #\! #\$ #'pling-dollar)

---

From: Marco Antoniotti <[email-masked]>
Date: Mon Sep 3 10:11:02 2001

> X-Authentication-Warning: edgedsp4.rtp.ericsson.se: toy set sender to [email-masked] using -f
> Cc: [email-masked]
> From: Raymond Toy <[email-masked]>
> User-Agent: Gnus/5.0808 (Gnus v5.8.8) XEmacs/21.5 (artichoke)
> Content-Type: text/plain; charset=iso-8859-1
> Sender: [email-masked]
> X-BeenThere: [email-masked]
> X-Mailman-Version: 2.0.5
> Precedence: bulk
> List-Help: <mailto:[email-masked]?subject=help>
> List-Post: <mailto:[email-masked]>
> List-Subscribe: <http://lists.sourceforge.net/lists/listinfo/clisp-list>,
> 	<mailto:[email-masked]?subject=subscribe>
> List-Id: CLISP user discussion <clisp-list.lists.sourceforge.net>
> List-Unsubscribe: <http://lists.sourceforge.net/lists/listinfo/clisp-list>,
> 	<mailto:[email-masked]?subject=unsubscribe>
> List-Archive: <http://lists.sourceforge.net/archives//clisp-list/>
> Date: 31 Aug 2001 11:11:03 -0400
> X-Filter-Version: 1.7 (cat)
> X-MIME-Autoconverted: from quoted-printable to 8bit by cat.nyu.edu id f7VIv0a26659
> Content-Length: 1367
> 

(deftype my-index-type ()
  `(integer 42 ,array-total-size-limit))

In theory a CL implementation could (and CMUCL can) recognize that
MY-INDEX-TYPE is a type spec that can fit in a FIXNUM.

Cheers

-- 
Marco Antoniotti ========================================================
NYU Courant Bioinformatics Group        tel. +1 - 212 - 998 3488
719 Broadway 12th Floor                 fax  +1 - 212 - 995 4122
New York, NY 10003, USA                 http://bioinformatics.cat.nyu.edu
                    "Hello New York! We'll do what we can!"
                           Bill Murray in `Ghostbusters'.