# [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.*