Re: [isabelle] Non-exhaustive case certificates

Hi Florian,

True.  The implementation however is not so general since in my mind I
could never imagine a user case which would make it necessary to provide
anything beyond the internal foundational case certificates as a kind of
protocol between the datatype package and the code generator.  This is
the reason why there is no full-blown user interface for case
certificates (yet).  Indeed two years ago I was thinking about that but
put it aside since it did not seem worth the effort.

Note that I do not ask about a full-blown user interface for case certificates. I just plan to generate and register them on the ML level. All I need is that the case operator is allowed to take extra variables that do not appear in any conclusion.

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

What is your application?
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)

where the new case "other" represents all constructors that have not yet been been added to enum. Due to reflexivity of =, this equation is provable if the cases for the existing constructors A, B, and C are provable. Now, I would like the generated code to be something like

fun my_fun q = (case ... of A => ... | B => ... | C => ...)

and not

fun enum_case a _ _ _ A = a
  | enum_case _ b _ _ B = b
  | enum_case _ _ c _ C = c

fun my_fun q = enum_case ... ... ... (my_fun q) ...

because that would loop and evaluate all cases before deciding.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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