[isabelle] Haskell code generation feature request

Hi Florian,

Would it be possible to set up List.thy so that it uses more of the Haskell prelude list functions? Here's the mapping I'm thinking of (some of these mappings may already be set up, but I know that at least (op @) and rev aren't):

op @		--> (Prelude.++)

filter			--> Prelude.filter
concat		--> Prelude.concat
foldl			--> Prelude.foldl
foldr --> Prelude.foldr (* ...with last two arguments swapped. What to do when foldr is curried? *)
hd			--> Prelude.head
tl			--> Prelude.tail
last			--> Prelude.last
butlast		--> Prelude.init
map		--> Prelude.map
take			--> Prelude.take
drop		--> Prelude.drop
takeWhile	--> Prelude.takeWhile
dropWhile	--> Prelude.dropWhile
rev			--> Prelude.reverse
zip			--> Prelude.zip
upt			-->  (\m n -> [m..(n-1)])
replicate		--> Prelude.replicate

Another alternative would be to have a special "Haskell_Prelude" theory that contains these adaptations.


Attachment: smime.p7s
Description: S/MIME cryptographic signature

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