# Re: [isabelle] Code generator setup for lazy lists

```On Wed, Sep 14, 2011 at 8:21 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
> Dear all,
>
> I am wondering how I can efficiently implement a conversion function list_of
> between the subset of finite lists from the type of possibly infinite lists
> (as defined in AFP-Coinductive) and ordinary lists from the HOL image.
>
> At present, the code equations for list_of are as follows in the AFP:
>
> list_of LNil = []
> list_of (LCons x xs) = (if lfinite xs then x # list_of xs else undefined)
>
> This way, the finiteness test is executed once for every element of the
> list, which makes conversion quadratic in the length of the list. Now, I
> would like to execute the finiteness test at most a constant number of times
> by exploiting that finiteness is preserved through all recursive calls. I
> hope that I can do this with the code generator's support for invariants.

Hi Andreas,

defining any new types or using invariants, you could just define an
auxiliary function to use with code generation for list_of.

My first idea was to define a variation of list_of that returns an
option type instead of using the "undefined" value:

definition opt_list_of :: "'a llist => 'a list option"
where [code del]: "opt_list_of xs = (if lfinite xs then Some
(list_of xs) else None)"

The code equations for opt_list_of are more efficient than the
standard ones for list_of, because they replace the expensive lfinite
test with a simple pattern match:

lemma opt_list_of_code [code]:
"opt_list_of LNil = Some Nil"
"opt_list_of (LCons x xs) =
(case opt_list_of xs of None => None | Some xs' => Some (x # xs'))"
unfolding opt_list_of_def by simp_all

Now you can declare a code equation for list_of so that it calls opt_list_of:

lemma list_of_code [code]:
"list_of xs = (case opt_list_of xs of None => undefined | Some xs' => xs')"
unfolding list_of_def opt_list_of_def by simp

My second idea is to define a function list_of_aux that uses an
accumulating parameter to store the list of elements seen so far:

definition list_of_aux :: "'a list => 'a llist => 'a list" where
"list_of_aux xs ys = (if lfinite ys then rev xs @ list_of ys else undefined)"

lemma list_of_aux_code [code]:
"list_of_aux xs LNil = rev xs"
"list_of_aux xs (LCons y ys) = list_of_aux (y # xs) ys"
unfolding list_of_aux_def by simp_all

lemma list_of_eq_list_of_aux [code]:
"list_of = list_of_aux []"
unfolding fun_eq_iff list_of_def list_of_aux_def by simp

I suppose that list_of_aux is more efficient than opt_list_of, since
it is actually tail-recursive.

Hope this helps,

- Brian

```

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