[isabelle] Some Remarks to Code Generation



Hi!

I am currently using the code generation facility (mostly for Scala).
All in all it works very well so far, the generated code compiles, I have tried data type refinement, code equation replacement, etc. 

So thank you for this great feature!

There are some minor oddities I stumbled on, however, some of which might be worth a change in the library:

A) I was a bit shocked that after proving every function to be total in Isabelle and using proven code equations for refinement, I could make the generated code loop quite easily.

I don't think this is discussed in the code equation chapter of the code generation tutorial.

I stumbled upon it while giving some (admittedly very stupid) equation for an "equal_class.equal" implementation and first thought it would only be a corner case, as equality is handled in a quite special way.

As it turns out it is quite easy to prove a code equation that obviously leads to non-terminating execution.
I guess it is non-trivial to find out if code equations screw you over, so there is not much that can be done here...

B) Code_Integer uses reference equality on BigInt in Scala. That seems to be a bad idea… I had a hard time figuring out why my code did not behave as expected and it turned out that some zeros were not equal to zero (same with some ones). Replacing the equality in the generated code with "inta.equals(int)" fixed all my problems.

I don't know how to adjust the part in Code_Integer to fix the code generator instead, so any advise there would be helpful.

C) Tail recursion. I got stack overflows (with increased stack size) from many of my own functions and some of the library functions. I solved mine by data type refinement and code equations, which leaves the ones in the library.

I think there was a discussion involving fold variants some time ago and which was more "canonical".
The situation now seems to be that there is fold, foldl and foldr in List.thy:

> primrec fold :: "('a => 'b => 'b) => 'a list => 'b => 'b"
> where
>   fold_Nil:  "fold f [] = id"
> | fold_Cons: "fold f (x # xs) = fold f xs o f x" -- {* natural argument order *}
> 
> primrec foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
> where
>   foldr_Nil:  "foldr f [] = id"
> | foldr_Cons: "foldr f (x # xs) = f x o foldr f xs" -- {* natural argument order *}
> 
> primrec foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
> where
>   foldl_Nil:  "foldl f a [] = a"
> | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"

Of these three, only foldl is tail recursive. My generated code had to tackle _extremely large_ parameters, so it was a good benchmark to test for tail recursion…

Most notably the rev function on lists is not tail recursive, as its code equations are based on fold:

> lemma rev_conv_fold [code]:
>   "rev xs = fold Cons xs []"
>   by (simp add: fold_Cons_rev)

I see no good reason for this as rev is the most basic of all tail recursive functions, so I replaced its code equations:

> declare rev_conv_fold [code del]
> 
> lemma rev_foldl_general:
>   "rev m @ n = foldl (λl e. e # l) n m"
>   by (induct m, auto) (metis fold_Cons_rev foldr_conv_fold foldr_conv_foldl rev_rev_ident)
> 
> lemma rev_foldl [code]:
>   "rev = foldl (λl e. e # l) []"
>   by (rule ext, fold rev_foldl_general) simp


The parameters needed to be flipped, which is not perfect, but I did no longer get stack overflows from rev.

The other function I noticed was map, which is of course a totally different story. It also produced stack overflows for me, so I had to replace it, yet I don't think this is a good idea in general, as map is just not tail recursive.

> fun rev_map where
>   "rev_map f = foldl (λl e. f e # l) []"
> 
> theorem rev_map_eq:
>   "rev_map f l = rev (map f l)"
>   by (induct l rule: rev_induct) auto
> 
> declare map.simps [code del]
> 
> lemma map_tail [code]:
>   "map f l = rev (rev_map f l)"
>   by (metis rev_map_eq rev_swap)

Thanks again for an overall amazing and extremely powerful feature!

Patrick Michel
Software Technology Group
University of Kaiserslautern






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.