Re: [isabelle] Imperative_HOL: code generator setup for Haskell



Hi Christian,

> 1) In Heap_Monad.thy there is a Haskell preamble including
> 
> lengthArray :: STArray s a -> ST s Integer;
> lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
> 
> Shouldn't that be the above +1? I thought in Haskell the bounds state
> the lowest and highest *index* of an array. So an array created with
> bound (0, k) should have length k+1. Maybe I'm wrong?

well, experimentally the second position of getBounds seems indeed to be
the *length*, not the highest index.  You may want to make two, three
examples to convince yourself.

	Florian

-- 

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.