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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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