Email Gateway (Aug 18 2022 at 19:24): Email Gateway (Aug 18 2022 at 19:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
Case certificates must always be exhaustive!
Exhaustive with respect to what?
exhaustive in the sense that the number of discriminators must be
equal to the number of constructors (in the sense of the code generator).
I do not see why
code certificates need to be exhaustive with respect to the logic other
than restrictions in the code generator implementation.
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.
The best documentation for case certificates available is indeed if you
follow the implementation of Code.add_case.
What is your application? Does it go beyond pure esthetic concerns? I
would be relucant to touch the trusted code base of code.ML if there is
not a striking reason (neglecting questions of effort estimation at the
moment).
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:25):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 19:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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 likedatatype 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 likemy_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.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:32):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear all,
suppose I have a type with a number of constructors, but only some of them are
meant to be used for code generation. For example:
datatype foo = A | B | C | D
definition test
where "test x = 4 + (case x of A => 0 | B => 1 | C => 2 | D => 3)"
In the exported code for test, the case expression is translated into a case
expression of the target language. In particular, it does not use foo_case.
However, when I restrict foo to some subset of constructors, say
code_datatype A B C
then export_code on test generates the error message
*** "Test.foo.D" is not a constructor, on left hand side of equation:
*** case D of A => ?f1.0 | B => ?f2.0 | C => ?f3.0 | D => ?f4.0 == ?f4.0
*** At command "export_code"
This error message seems to stem from the case certificate that the datatype
declaration registered in the code generator. I'd like to replace that after the
code_datatype declaration with something like
lemma new_foo_case_cert:
assumes "CASE == foo_case a b c d"
shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
using assms by auto
setup {*
Code.add_case @{thm new_foo_case_cert}
*}
This version raises the exception option, other variations yield "bad case
certificate". How do I need to phrase the case certificate such that the code
generator accepts it?
If this is impossible, I'd like to know why. If it is just a matter of adapting
the code generator implementation, I'd be happy to assist in implementing this.
Andreas
Email Gateway (Aug 18 2022 at 19:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
However, when I restrict foo to some subset of constructors, say
code_datatype A B C
then export_code on test generates the error message
*** "Test.foo.D" is not a constructor, on left hand side of equation:
*** case D of A => ?f1.0 | B => ?f2.0 | C => ?f3.0 | D => ?f4.0 == ?f4.0
*** At command "export_code"
This has nothing to do with the case certificate, but stems from the
code equations for »foo_case«. The case certificate should be thrown
away on »code_datatype«, so code generation falls back on the
corresponding code equations.
So do something like:
lemma [code, code del]:
"foo_case = foo_case" ..
lemma [code]:
"foo_case … = …"
"foo_case … = …"
"foo_case … = …"
…
"foo_case … = …"
If you still want proper case expressions, add a case certificate manually.
lemma new_foo_case_cert:
assumes "CASE == foo_case a b c d"
shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
using assms by auto
setup {*
Code.add_case @{thm new_foo_case_cert}
*}
What is suspicicious is that »d« never occurs in the conclusion. I
guess they should read »a d« etc.
Cheers,
Florian
Email Gateway (Aug 18 2022 at 19:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I forgot:
Case certificates must always be exhaustive!
Florian
Email Gateway (Aug 18 2022 at 19:37):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Florian,
thanks for the clarifiction.
If you still want proper case expressions, add a case certificate manually.
Yes, I do want them, because otherwise ML evaluates all parameters too foo_case,
which might raise an exception. And I do not want to add closures everywhere.
Case certificates must always be exhaustive!
Exhaustive with respect to what? The lemma below is exhaustive with respect to
the code generator setup -- there are three code_datatype constructors and there
is one conclusion for each). I do not see why code certificates need to be
exhaustive with respect to the logic other than restrictions in the code
generator implementation.
lemma new_foo_case_cert:
assumes "CASE == foo_case a b c d"
shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
using assms by auto
setup {*
Code.add_case @{thm new_foo_case_cert}
*}What is suspicicious is that »d« never occurs in the conclusion. I guess they
should read »a d« etc.
I do not fully understand your remark, but let me explain in a bit more detail:
foo_case is not changed by the code_datatype command. Logically, type foo still
has 4 constructors, so the case combinator needs to have 4 parameters for the
cases, which are a, b, c, and d in the above lemma. However, the code generator
only knows about three constructors A, B, and C. As soon as I try to prove a
case certificate with 4 conclusions, I get a "bad case certificate" error. For
example:
lemma new_foo_case_cert:
assumes "CASE == foo_case a b c d"
shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c) &&& (CASE D = d)"
using assms by auto
setup {* Code.add_case @{thm new_foo_case_cert} *}
I also tried the following version without success:
lemma new_foo_case_cert:
assumes "CASE == foo_case a b c"
shows "(CASE d A == a) &&& (CASE d B == b) &&& (CASE d C == c)"
So what is the right form of the certificate?
Note that I cannot define a specialised case combinator such as
foo_case' a b c = foo_case a b c 3
and use the symmetric equation as code_unfold, because other constants might
need different specialised case combinators and the code generator supports only
one.
Andreas
Last updated: Apr 25 2024 at 20:15 UTC