Re: [isabelle] Non-exhaustive case certificates

Hi Andreas,

> I am currently working on the problem that you cannot use different
> implementations for 'a set or ('a, 'b) mapping in a single application
> without getting into trouble with sort constraints. To get an extensible
> solution to that, I define extensible enumerations, i.e., something like
> datatype enum = A | B | C
> but with the possibility to add further constructors to enum later on.
> With this, one of course loses exhaustiveness theorems, but it seems to
> work for my application. Nevertheless, I would like to do case
> distinctions on enum in code equations using a case expression like
> my_fun q = (case ... of A => ... | B => ... | C => ... | other => my_fun q)

OK, convinced.

Indeed, when looking at the code in code.ML (functions case_certificate
and add_cert), it does not seem so difficult to extend it in a manner
that arguments to a case combinator can be ignored.  However it would
require some generalization which I personally do not have resources
now.  Maybe you would like to give it a try?  The first step would be to
extend code.ML accordingly and then look what consequences this has for
the derived modules in src/Tools/Code.

>> Does it go beyond pure esthetic concerns?
> In principle, case certificates are *always* esthetic because they do not enhance the expressivity of the code generator. One could always replace any case expression by a definition of a specialised constant via pattern matching and then hope that the ML or Haskell compiler inlines the artificial function as a case expression again. Nevertheless, they do exist in their present form, because it is much nicer to use case expressions in code equations than to define a separate constant for each occurrence.

Not wholly.  It is also a matter of evaluation order.  This is the
reason why e.g. NBE generated explicit cases.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.