From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.3 required=5.0 tests=SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id D6022BC6C for ; Thu, 31 Jan 2008 14:29:03 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGJcoUfAXQInh2dsb2JhbACQKwEBAQgKKZoV X-IronPort-AV: E=Sophos;i="4.25,285,1199660400"; d="scan'208";a="6779316" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 31 Jan 2008 14:29:02 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m0VDSuYs014171 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 31 Jan 2008 14:29:02 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah4FACdcoUfUTWUFZGdsb2JhbACQHQEYBAUIH5oc X-IronPort-AV: E=Sophos;i="4.25,285,1199660400"; d="scan'208";a="8572791" Received: from mx1.wp.pl ([212.77.101.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 31 Jan 2008 14:28:57 +0100 Received: (wp-smtpd smtp.wp.pl 27052 invoked from network); 31 Jan 2008 14:28:54 +0100 Received: from poczta-19.free.wp-sa.pl (HELO localhost) ([10.1.1.98]) (envelope-sender ) by smtp.wp.pl (WP-SMTPD) with SMTP for ; 31 Jan 2008 14:28:54 +0100 Date: Thu, 31 Jan 2008 14:28:54 +0100 From: "Dawid Toton" To: "caml-list" Subject: Attach an invariant to a type Message-ID: <47a1cd167921b@wp.pl> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-2 Content-Transfer-Encoding: 8bit Content-Disposition: inline X-Mailer: Interfejs WWW nowej poczty Wirtualnej Polski X-User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.8.0.12) Gecko/20071127 Red Hat/1.5.0.12-0.8.el4 Firefox/1.5.0.12 pango-text Organization: Nowa Poczta Wirtualnej Polski S.A. http://www.wp.pl/ X-WP-IP: 137.73.5.196 X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A. X-WP-SPAM: NO 0000000 [MUOU] X-Miltered: at concorde with ID 47A1CD18.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; translated:01 klik:98 assert:01 assert:01 int:01 int:01 let:03 let:03 adr:04 i'd:06 invariant:08 invariant:08 equivalent:09 exist:13 should:13 What should I do if I have need for the following? Does already exist any equivalent solution? I'd like to write: type subindex = int invariant x -> (x>=10)&&(x<=100) let doit (a:subindex) (b:subindex) = let result = some_operation a b in (result:subindex) And it should be translated to: type subindex = int let subindex_invariant x = (x>=10)&&(x<=100) let doit (a:subindex) (b:subindex) = assert (subindex_invariant a); assert (subindex_invariant b); let result = some_operation a b in assert (subindex_invariant result); (result:subindex) Am I going right direction at all? ---------------------------------------------------- Promocyjne oferty biletów lotniczych! Praga, Rzym, Paryż, Mediolan już od 499zł - Kliknij: http://klik.wp.pl/?adr=http%3A%2F%2Fsamoloty.wp.pl%2Fpromocje%2F&sid=202