Email Gateway (Aug 22 2022 at 19:42): Email Gateway (Aug 22 2022 at 19:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,
that is more or less all you can do at the moment.
There has been a thread on the dev mailing list dealing with the issue
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-January/006552.html
which AFAIKS came to the same conclusion.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:52):From: Dominique Unruh <unruh@ut.ee>
Hello,
I ran into a case where the code generation produces invalid ML code
(with the default code generator setup).
The problem seems to be related to ML code for type classes which under
certain circumstances leads to a polymorphic value (instead of a
polymorphic function) for representation of the type class. And
polymorphic values aren't really polymorphic in ML. The attached theory
shows this. (Tested with 2019-RC0)
It gives an error as follows:
Error: Type mismatch in type constraint.
Value: {uniformity = uniformity_lista} : {uniformity: 'a}
Constraint: 'a list uniformity
Reason:
Can't unify 'a to ('a list * 'a list) filter
(Type variable is free in surrounding scope)
{uniformity = uniformity_lista} : 'a list uniformity
At (line 15 of "generated code")
Exception- Fail "Static Errors" raised
How can I change my code setup so that the code compiles? (Without
changing the class hierarchy.)
Best wishes,
Dominique.
Scratch.thy
Email Gateway (Aug 22 2022 at 19:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,
there are some borderline cases in code generation which do not work out
of the box indeed. Your example involving filters is problematic since
filters are not executable in general at all, so resolving the
dictionary issue won't help. Do you have a less synthetic example at hand?
Cheers,
Florian
signature.asc
Last updated: Apr 20 2024 at 04:19 UTC