From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA25950; Fri, 8 Oct 2004 18:35:16 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA25939 for ; Fri, 8 Oct 2004 18:35:15 +0200 (MET DST) Received: from caduceus.jf.intel.com (fmr06.intel.com [134.134.136.7]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i98GZElr014815; Fri, 8 Oct 2004 18:35:15 +0200 Received: from talaria.jf.intel.com (talaria.jf.intel.com [10.7.209.7]) by caduceus.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-outer.mc,v 1.15 2004/01/30 18:16:28 root Exp $) with ESMTP id i98GYaF5014342; Fri, 8 Oct 2004 16:34:36 GMT Received: from orsmsxvs041.jf.intel.com (orsmsxvs041.jf.intel.com [192.168.65.54]) by talaria.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-inner.mc,v 1.11 2004/07/29 22:51:53 root Exp $) with SMTP id i98GPkVu022419; Fri, 8 Oct 2004 16:26:29 GMT Received: from orsmsx331.amr.corp.intel.com ([192.168.65.56]) by orsmsxvs041.jf.intel.com (SAVSMTP 3.1.2.35) with SMTP id M2004100809351213410 ; Fri, 08 Oct 2004 09:35:12 -0700 Received: from orsmsx407.amr.corp.intel.com ([192.168.65.50]) by orsmsx331.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.0); Fri, 8 Oct 2004 09:35:11 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Are you sure the new "=" of 3.08 is good ? Date: Fri, 8 Oct 2004 09:35:11 -0700 Message-ID: <012676D607FCF54E986746512C22CE7D0FE7B8@orsmsx407> Thread-Topic: [Caml-list] Are you sure the new "=" of 3.08 is good ? Thread-Index: AcStT03b5ljQZz9PThqHU5EZT7ZQ7gABBxzg From: "Harrison, John R" To: "Xavier Leroy" Cc: "caml-list" X-OriginalArrivalTime: 08 Oct 2004 16:35:11.0700 (UTC) FILETIME=[C7F81940:01C4AD54] X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang) X-Miltered: at concorde with ID 4166C1C2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 johnh:01 follwing:01 provers:01 high-level:01 subgraphs:01 constr:01 constr:01 generic:01 raffalli:01 christophe:01 equality:01 equality:01 behaviour:01 instantiated:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk | > I was assuming two things about equal: | > - scan of block from left to right | > - a test on adress equality on pointer before follwing the pointer=20 | > (which is now wrong in 3.08). |=20 | That was true of the old implementation, but has never been guaranteed. For LCF-style theorem provers, I think it's quite important that when comparing terms (or similar tree structures) for equality, there should be a quick "yes" when two high-level subgraphs are pointer eq. For example, Constr(small_1,big) =3D Constr(small_2,big) (where small_1 =3D small_2) should return "true" without recursing down "big". This often comes up when generic theorems are instantiated and one then checks that the instantiation does make certain terms match up. I guess like Christophe Raffalli I had just assumed this would be the case based on long experience with ML-family languages, rather than through any explicit discussion in the documentation. Can you clarify what we need to do in order to guarantee this behaviour? John. ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners