Re: [Caml-list] exception Foo = Bar.Baz

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com>]

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.)