Email Gateway (Aug 22 2022 at 15:53): Email Gateway (Aug 22 2022 at 15:53):From: Wenda Li <wl302@cam.ac.uk>
Dear code generation experts,
When porting some of my code from Isabelle2016 to Isabelle2016-1 (as well as the latest repository version:5be0b0604d71), I found that the following piece of code was no longer working:
code_reflect Foo
datatypes rat=“_"
And the error message said “Cannot export abstract constructor(s): Frct”.
I understand the idea of abstract constructors that are usually not allowed on the right-hand side of a code equation. Nevertheless, I am a little baffled here and was wondering what is the standard way to circumvent the situation?
Best,
Wenda
Email Gateway (Aug 22 2022 at 15:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Wenda,
try something like
code_reflect Foo
datatypes rat
functions …
where … stands for the operations you actually want to refer to in later
Isabelle/ML sections.
In the upcoming Isabelle release, a new concept called »Computations«
has been implemented. You might want to study the corresponding
sections in the Tutorial on Code Generation; maybe this is a suitable
replacement for your current application of code_reflect.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 16:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I have a similar problem. I tried what you suggested, and the
code_reflect itself worked fine, but when I actually tried to run the
code with "value", I got a compiler error saying that "Frct" couldn't be
found. (the same for "nat", "poly", etc.)Leaving out "nat", "poly" etc. completely doesn't work either, because
then I get errors like "Foo.nat does not unify with nat".
code_reflect always has been notoriously difficult to use.
What is the context of your application? Would computations be a
suiteful device instead?
Best,
Florian
Manuel
On 21/08/17 19:41, Florian Haftmann wrote:
Hi Wenda,
code_reflect Foo
datatypes rat=“_"And the error message said “Cannot export abstract constructor(s): Frct”.
I understand the idea of abstract constructors that are usually not allowed on the right-hand side of a code equation. Nevertheless, I am a little baffled here and was wondering what is the standard way to circumvent the situation?
try something like
code_reflect Foo
datatypes rat
functions …where … stands for the operations you actually want to refer to in later
Isabelle/ML sections.In the upcoming Isabelle release, a new concept called »Computations«
has been implemented. You might want to study the corresponding
sections in the Tutorial on Code Generation; maybe this is a suitable
replacement for your current application of code_reflect.Cheers,
Florian
Email Gateway (Aug 22 2022 at 16:04):From: Manuel Eberl <eberlm@in.tum.de>
I wanted to solve linear recurrences. Essentiall, I want to evaluate
something like "solve_lhr [1,2,3,4::complex] [1,1,1::complex]" using the
"value" command. This returns essentially some lists of complex numbers
and polynomials.
Unfortunately, that takes about 40 seconds in Isabelle, though the
exported Haskell code takes only a few milliseconds, so I wanted to see
what I can do with code_reflect.
Manuel
Email Gateway (Aug 22 2022 at 16:04):From: Wenda Li <wl302@cam.ac.uk>
Previously (i.e., in Isabelle2016), I was using code_reflect + Code_Runtime.static_holds_conv to efficiently evaluate ground terms inside a decision procedure. As Code_Runtime.static_holds_conv is no longer available, I am currently trying to achieve the same thing through code_reflect + computation_check. I was wondering if this is the correct direction?
Wenda
Email Gateway (Aug 22 2022 at 16:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Wenda,
you should not need code_reflect any longer, which was never intended as
an »acceleration device« but had to be used for that in lack of better
tools. »computation_check« should be sufficient, following chapter §6
of the tutorial on code generation in Isabelle2017 (currently available
as RC2).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 16:05):From: Manuel Eberl <eberlm@in.tum.de>
I have a similar problem. I tried what you suggested, and the
code_reflect itself worked fine, but when I actually tried to run the
code with "value", I got a compiler error saying that "Frct" couldn't be
found. (the same for "nat", "poly", etc.)
Leaving out "nat", "poly" etc. completely doesn't work either, because
then I get errors like "Foo.nat does not unify with nat".
Manuel
Last updated: Apr 23 2024 at 12:29 UTC