Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Haskell code generation feature request

Email Gateway (Aug 18 2022 at 15:28):

From: John Matthews <matthews@galois.com>
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.

Thanks,
-john
smime.p7s

Email Gateway (Aug 18 2022 at 15:28):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,

Would it be possible to set up List.thy so that it uses more of the
Haskell prelude list functions?

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

I see no obstacle for the second option. The philosophy is that the
default setup does impose as little deviation from the core calculus as
possible, and the user must import adaptation theories explicitly, e.g.
for target language integers. An exception are setups which lead to a
considerable improvement of readability and interoperability but still
maintain an isomorphism (pairs, unit, lists, options; fst, snd).

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

If you like to setup such a theory, I can offer to include it into the
distribution. Concerning the foldr and upt issue, you can use Haskell
lambda terms:

code_const upt
(Haskell "(\\m n ->/ [m..(n-1)])")

This target language syntax is a little bit tedious.

Hope this helps,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC