From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: <5764c029b688c1c0d24a2e97cd764f@gmail.com> X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 9C20A7EF5E for ; Tue, 26 Jul 2016 10:58:49 +0200 (CEST) IronPort-PHdr: 9a23:KDPSNxOY9Ga59jjb4nMl6mtUPXoX/o7sNwtQ0KIMzox0Kfr+rarrMEGX3/hxlliBBdydsKMczbSN+Pi6EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU0Z/8j7r60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9ZLuh5dsPM59sNGTb6yP+FhFeQZX3waNDUc4MTqs1HtVwqU7XtUBmwSmxtORQbf7QrxXr/1vzv7uOs70y6fa4m+aps9XDDqu6xiTRutjCYcKxY49nvWg4p+lvQf6D2orQZ+zoqcW4qVOeBzZOuJctoQX2tMWoBKXCxMGI6mR4QKBusFe+1fqt+uiUEJqE6bDBWhBqvMzSRJhTeigPJkj+95S1DMglxwFIsF6HiO8NyvOfZNWuzqkvXG5TrGZvJSnzz67d6bIVgavfiQUOcoIoLqwk41GlaA1w3IpA== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=5764c029b688c1c0d24a2e97cd764f@gmail.com; spf=Pass smtp.mailfrom=5764c029b688c1c0d24a2e97cd764f@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f52.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of 5764c029b688c1c0d24a2e97cd764f@gmail.com) identity=pra; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="5764c029b688c1c0d24a2e97cd764f@gmail.com"; x-sender="5764c029b688c1c0d24a2e97cd764f@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of 5764c029b688c1c0d24a2e97cd764f@gmail.com designates 74.125.82.52 as permitted sender) identity=mailfrom; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="5764c029b688c1c0d24a2e97cd764f@gmail.com"; x-sender="5764c029b688c1c0d24a2e97cd764f@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f52.google.com) identity=helo; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="5764c029b688c1c0d24a2e97cd764f@gmail.com"; x-sender="postmaster@mail-wm0-f52.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C8EAC4JZdXhjRSfUpUCoJAgVUqUq02jT8kgxKCZwKBMjwQAQEBAQEBAQERAQEBCAsLCRkvQRABgWAEARIBghMBBRIRDwENARseAwwGAwILBQgCAiYCAiMRAQUBHAYBDAgCHod0AQMXBAqLaI9EgTI+MYs7gWqCWgWEMAoZJw1URIJ2AQEBAQEFAQEBAQEBARgCAQUQcYchCIJNhBgFgySCWgEEjhWLGwGGGIhjiUYOhWuMLYI5MIEPNYJAgVlsgx2DYoFDAQEB X-IPAS-Result: A0C8EAC4JZdXhjRSfUpUCoJAgVUqUq02jT8kgxKCZwKBMjwQAQEBAQEBAQERAQEBCAsLCRkvQRABgWAEARIBghMBBRIRDwENARseAwwGAwILBQgCAiYCAiMRAQUBHAYBDAgCHod0AQMXBAqLaI9EgTI+MYs7gWqCWgWEMAoZJw1URIJ2AQEBAQEFAQEBAQEBARgCAQUQcYchCIJNhBgFgySCWgEEjhWLGwGGGIhjiUYOhWuMLYI5MIEPNYJAgVlsgx2DYoFDAQEB X-IronPort-AV: E=Sophos;i="5.28,423,1464645600"; d="scan'208";a="227970491" Received: from mail-wm0-f52.google.com ([74.125.82.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 Jul 2016 10:58:49 +0200 Received: by mail-wm0-f52.google.com with SMTP id o80so6056747wme.1 for ; Tue, 26 Jul 2016 01:58:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding; bh=WmMu6TfEgetZEVgLRL/M2gD+/Y9sZdGatSrlkMilspo=; b=GgXQC7OGlq7UShxvSuVkz005YCvfyPZiQ+dU+hrEpb2+5unZEqbqK0wzneLLYQy5+q pYh9Tjrq8HDPWS50WORTy0qqrdoQvJpblDQo846fedGfN3pyKItUxKnI+5Xk5C/k7Yhl dkK18xbJRdbCe8PUj7R6IIPStipvS9MT87NsUvVbuL+H72t+RZa+G566WZmcSSxkgkkW Hw0qOMr0eA8tAtp50US3fEVTSP0rbYaMaKCtPDU0OFbkuK89hNv2pb3Go6/wg9LnGDXy OFeAQEJQsA5j0MOkuKg6hJ1OhQx4O4d2pCKxZ8PUul3Gm25Q//h7uBbBDostm/pfIe51 81uw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:subject:to:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-transfer-encoding; bh=WmMu6TfEgetZEVgLRL/M2gD+/Y9sZdGatSrlkMilspo=; b=k0tsEzWFftzzdNgx/Jm9NnK4zLk43n2oSCbOxt8YzFH4SZxvJUCbpI1MdGMhf/FNff Vk5vUw2yus7zx0NS7fBhsMwjouH689CzhmM2886RQufawju/c+GDZv+fdapKtqirHlgF uaLBgGN/MvlcOPPorkdiAK8+maZU8oenWsDfOvuhE9IwMhpPyrN3HmWTi951skd1EU2N Mof/CrrXcnqCrk0XnTNrOyL9jCx8iiX9OwjUoFai4xxNUlYCCC/OveMrqlIs3FRtacI2 UeFAuhsLAV0ZppXGrmEg9JKKcA99G9BHg1N63xAWbfHBiXLRq7/q829Isad3Kbn6K1XM hGHw== X-Gm-Message-State: AEkoouua53r8VxCZXY0ssv42SNt1228jQJN/oxAZnuNs1vU3qAd6qRdVWcYzNbzxiboZrA== X-Received: by 10.194.16.162 with SMTP id h2mr20160049wjd.52.1469523528752; Tue, 26 Jul 2016 01:58:48 -0700 (PDT) Received: from [172.18.118.121] ([81.253.26.206]) by smtp.googlemail.com with ESMTPSA id u72sm31727328wmf.5.2016.07.26.01.58.47 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 26 Jul 2016 01:58:47 -0700 (PDT) To: Alain Frisch , OCaml , Gabriel Scherer References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> Message-ID: Date: Tue, 26 Jul 2016 11:02:04 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Icedove/45.1.0 MIME-Version: 1.0 In-Reply-To: <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] exception Foo = Bar.Baz On 07/25/2016 10:02 PM, Alain Frisch wrote: > On 25/07/2016 16:34, Matej Kosik wrote: >> That means that, at present, one can put something like: >> >> exception Foo = Bar.Baz >> >> inside a _module structure_. >> >> I am currently wondering why we are not allowed (also) to put this into a _module signature_ ? >> Is this a deliberate decision (why?) or merely an omission? > > What would be the use of putting that in a module signature instead of just "exception Foo"? AFAIK, if I put: exception Foo to some module signature, I am saying that: - a given module defines a *new* exception - a given module exports that new exception That is not what I want to say, which is: - a given module defines an alternative name for some *existing* exception - a given module exports this new alternative name of an existing exception. ────────────────────────────────────────────────────────────────────────────── The motivation is the same as in case of our ability to define alternative names to existing - sum-types - record-types where we can put something like type a = B.c = C1 | C2 | ... | Cn (* where C1, C2, C2, ..., Cn are all the constructors of sum-type B.c *) or type a = B.c = {f1:t1; f2:t2; ... ; fn:tn} (* where f1,...,fn are all the fields of the record-type B.c *) in module signature. Recently, I realized that this is actually useful but I lack this kind of mechanism for exceptions. There may be workarounds but I would like to understand why this kind of mechanism is not available (is this intentional or just nobody needed it so there was no motivation to implement it). ────────────────────────────────────────────────────────────────────────────── Some more (although embarassing) details: At present, individual files of Coq plugins are compiled with the following options passed to ocamlc -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I stm -I toplevel -I parsing -I printing -I intf -I engine -I ltac -I tools -I tools/coqdoc -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/setoid_ring -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode -I plugins/btauto -I plugins/ssrmatching -I "/home/me/.opam/4.02.3/lib/camlp5" and I am currently trying to whether it is possible to compile them instead with just something like: -I lib -I API -I $THE_PLUGIN_DIRECTORY where API/API.mli is the thing I am trying to (1) identify https://github.com/matej-kosik/coq/blob/API/API/API.mli https://github.com/matej-kosik/coq/blob/API/API/API.ml if I succeed, then (2) clean up, then (3) document. Obviously, in the API, I do not want to define new exceptions, only aliases to existing ones. (so that plugins can catch the relevant exceptions not fake ones) > (This could perhaps allow the compiler to report more pattern as being useless, but this is of limit > benefit.)