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.

Cheers,
Andreas

--
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.edu
http://pp.info.uni-karlsruhe.de
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.