[isabelle] Code Optimization
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
Now, there are maybe different "efficiency"-concerns for different
programming languages. Lets take the example of 'concat(map xs)'. In
theory List we have
"concat(map f xs) = concat_map f xs" ...
where 'concat_map' is defined by
concat_map :: "('a => 'b list) => 'a list => 'b list"
"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:
rev_append :: "'a list => 'a list => 'a list"
"rev_append  ys = ys" |
"rev_append (x#xs) ys = rev_append xs (x#ys)"
concat_map' :: "('a => 'b list) => 'b list => 'a list => 'b list"
"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)
"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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and