Email Gateway (Aug 22 2022 at 14:43): Email Gateway (Aug 22 2022 at 14:43):From: Artur Gomes <gomesa@tcd.ie>
Hi there,
After making a few steps forward from my last email yesterday, with help of
Makarius, I got no more error messages of exception size raised. Now I'm
using
the 2016-1 version with Isabelle/ML 64bit version.
Now I'm bringing a new question hoping for some feedback, as what I'm doing
right now is new for me and I'm still learning.
I'm using haskabelle to translate some haskell code and what I have so far
is
a bunch of datatypes, written in overall 280 lines, and as an example, the
most complicated bit of formal spec, obtained through haskabelle is
something
like the following function definition that involves four or five other
functions, in a total of 95 lines.
function fun1 :: "some -> inputs -> and -> outputs"
and fun2 :: "some -> inputs -> and -> outputs" and
and fun3 :: "some -> inputs -> and -> outputs" and
and fun4 :: "some -> inputs -> and -> outputs" and
where
"they call each other in some parts"
| "fun1 calls fun2"
| "fun2 calls fun3"
| "fun3 calls fun4"
| "fun4 calls fun1"
I know that as they call each other they can't be declared one after each
other. So, my question is.. Is there any way of splitting those function
definitions? Basically, this is what is taking most of the time, like
several
minutes with the pieces in pink/purple, and high speed fan working in my
laptop. I presume that even if I use the cloud service from college, it
would
still be a hard work.
I tried to shrink a bit the datatypes and reduce the amount of cases for
testing purposes, but still, it is being really hard to get feedback from
Isabelle.
Is there something else I could do that would help me with this?
Many thanks.
Regards,
Last updated: Nov 21 2024 at 12:39 UTC