# [isabelle] Code Optimization

```Hi,

```
if I understand correctly, the attribute 'code_unfold' introduces something like a (pre)compiler optimization, that is, some easy-to-reason-about but inefficient code is replaced by a more efficient one.
```
```
Now, there are maybe different "efficiency"-concerns for different programming languages. Lets take the example of 'concat(map xs)'. In theory List we have
```
lemma concat_map_code[code_unfold]:
"concat(map f xs) = concat_map f xs" ...

where 'concat_map' is defined by

primrec
concat_map :: "('a => 'b list) => 'a list => 'b list"
where
"concat_map f [] = []" |
"concat_map f (x#xs) = f x @ concat_map f xs"

```
While I think that this is perfectly okay (and maybe even preferable in order to exploit lazyness) for Haskell, for a strict language (like OCaml) I would prefer the following implementation:
```
primrec
rev_append :: "'a list => 'a list => 'a list"
where
"rev_append [] ys = ys" |
"rev_append (x#xs) ys = rev_append xs (x#ys)"

primrec
concat_map' :: "('a => 'b list) => 'b list => 'a list => 'b list"
where
"concat_map' f res [] = rev res" |
"concat_map' f res (x#xs) = concat_map' f (rev_append (f x) res) xs"

```
lemma rev_append_rev: "rev_append xs ys = rev xs @ ys" by (induct xs arbitrary: ys) auto
```
lemma concat_map'_conv: "concat_map' f xs ys = rev xs @ concat(map f ys)"
by (induct ys arbitrary: xs) (simp_all add: rev_append_rev)

lemma concat_map_code_strict[code_unfold]:
"concat(map f xs) = concat_map' f [] xs"
unfolding concat_map'_conv by simp

```
So my question is: Is it possible to introduce different 'code_unfolds' for different target languages?
```
cheers

chris

```

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