Re: [isabelle] Haskell code generation feature request

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        -->
> take            --> Prelude.take
> drop        --> Prelude.drop
> takeWhile    --> Prelude.takeWhile
> dropWhile    --> Prelude.dropWhile
> rev            --> Prelude.reverse
> 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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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