[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 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

  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)

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?



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