Email Gateway (Aug 18 2022 at 14:34): Email Gateway (Aug 18 2022 at 14:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
So my question is: Is it possible to introduce different 'code_unfolds'
for different target languages?
this is not possible. In case you need different preprocessor setups,
you can provide separate theories which tweak the standard setup by
means of code_unfold / code_unfold del, and (not) import them as desired.
Personally I am sceptical whether such specialised optimisations are
worth the effort -- but don't take this remark too seriously.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:48):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Last updated: Apr 19 2024 at 01:05 UTC