From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: MON KEY Newsgroups: gmane.emacs.bugs Subject: bug#6878: bool-vectors of length 0 signal error when aref/aset the 0th element Date: Thu, 19 Aug 2010 13:06:58 -0400 Message-ID: References: NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1282237755 19101 80.91.229.12 (19 Aug 2010 17:09:15 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 19 Aug 2010 17:09:15 +0000 (UTC) Cc: Chong Yidong , Andreas Schwab , 6878@debbugs.gnu.org To: Stefan Monnier Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Thu Aug 19 19:09:13 2010 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([199.232.76.165]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Om8c4-0006iy-Vc for geb-bug-gnu-emacs@m.gmane.org; Thu, 19 Aug 2010 19:09:13 +0200 Original-Received: from localhost ([127.0.0.1]:57097 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1Om8c4-0002Wj-5V for geb-bug-gnu-emacs@m.gmane.org; Thu, 19 Aug 2010 13:09:12 -0400 Original-Received: from [140.186.70.92] (port=39161 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1Om8bt-0002VT-P5 for bug-gnu-emacs@gnu.org; Thu, 19 Aug 2010 13:09:02 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.69) (envelope-from ) id 1Om8bs-00077O-5V for bug-gnu-emacs@gnu.org; Thu, 19 Aug 2010 13:09:01 -0400 Original-Received: from debbugs.gnu.org ([140.186.70.43]:50269) by eggs.gnu.org with esmtp (Exim 4.69) (envelope-from ) id 1Om8bs-00077K-36 for bug-gnu-emacs@gnu.org; Thu, 19 Aug 2010 13:09:00 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.69) (envelope-from ) id 1Om8Z0-00089b-AB; Thu, 19 Aug 2010 13:06:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: MON KEY Original-Sender: debbugs-submit-bounces@debbugs.gnu.org Resent-To: owner@debbugs.gnu.org Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Thu, 19 Aug 2010 17:06:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 6878 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: Original-Received: via spool by 6878-submit@debbugs.gnu.org id=B6878.128223755331337 (code B ref 6878); Thu, 19 Aug 2010 17:06:02 +0000 Original-Received: (at 6878) by debbugs.gnu.org; 19 Aug 2010 17:05:53 +0000 Original-Received: from localhost ([127.0.0.1] helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.69) (envelope-from ) id 1Om8Yr-00089O-5O for submit@debbugs.gnu.org; Thu, 19 Aug 2010 13:05:53 -0400 Original-Received: from mail-ew0-f44.google.com ([209.85.215.44]) by debbugs.gnu.org with esmtp (Exim 4.69) (envelope-from ) id 1Om8Yp-00089J-JG for 6878@debbugs.gnu.org; Thu, 19 Aug 2010 13:05:52 -0400 Original-Received: by ewy22 with SMTP id 22so1392765ewy.3 for <6878@debbugs.gnu.org>; Thu, 19 Aug 2010 10:06:58 -0700 (PDT) Original-Received: by 10.216.0.206 with SMTP id 56mr88437web.33.1282237618372; Thu, 19 Aug 2010 10:06:58 -0700 (PDT) Original-Received: by 10.216.65.140 with HTTP; Thu, 19 Aug 2010 10:06:58 -0700 (PDT) In-Reply-To: X-Google-Sender-Auth: 1ZXavvbSbfw-MQDx4qRwJznBbBM X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.11 Precedence: list Resent-Date: Thu, 19 Aug 2010 13:06:02 -0400 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 3) X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Original-Sender: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.bugs:39638 Archived-At: On Thu, Aug 19, 2010 at 11:51 AM, Stefan Monnier wrote: >> Prove it! > > Easy! formally, he said: > > =E2=88=80 n =E2=89=A5 0 =E2=88=A7 n < 0. (aref (make-bool-vector 0 t) n)= =E2=88=88 { nil, t } > > And since there is no such `n', this is trivially true. > More specifically, "n =E2=89=A5 0 =E2=88=A7 n < 0" is a falsehood, and fr= om false you > can conclude anything you wish. Among other things you can just > a trivially prove: > > =E2=88=80 n =E2=89=A5 0 =E2=88=A7 n < 0. the sky is green > The problem with the above semantic vodoo is that it doesn't reflect the contents of the manual either: ,---- (info "(elisp)bool-vectors") | | A bool-vector is much like a vector, except that it stores only the | values `t' and `nil'. If you try to store any non-`nil' value into an | element of the bool-vector, the effect is to store `t' there. | `---- Informally, your formal proof is valid only so long as we suspend belief in the manual and the sources which the manual is intended to inform, specifically the place where it doesn't say that 0 length bool-vectors don't have a value at index 0. IOW your proofs universal qualifer relies on an empty domain where the manual would suggest otherwise. Since there is no "formal Emacs Lisp specification", and since we are not discussing the formal realm of denotational semantics nor first order logic w/ regards to a formal Emacs Lisp specification your proof is indeed only trivially applicable. Here is what I think the manual should say: at info node "Bool-Vector Type" ,---- | | A "bool-vector" is a special type of one-dimensional array. An elment | of a bool-vector which is accesible by its non-zero index must only be | `t' or `nil'. | `---- at info node "Bool-vectors" ,---- | | A bool-vector is a special type of vector which stores only the values `t= ' | and `nil'. If you try to store any non-`nil' value into an element of th= e | bool-vector, the effect is to store `t' there. As with all arrays, | bool-vector indices start from 0. Emacs allows creation of a bool-vector = of | length 0 however its length cannot be changed once the bool-vector is cre= ated. | An error is singaled if you try to access the 0 index of a bool-vector of | length 0. Bool-vectors are constants when evaluated. | `---- -- /s_P\