Re: [isabelle] Non-exhaustive case certificates
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
> 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.
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
What is your application?
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 => ...)
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
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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