Re: [isabelle] Code generation from IArray



Hi Jesus,

> 1. I had to edit "by hand" the obtained module, where functions on
> Isabelle "iarray"s were generated, including an additional import
> statement:
> 
> import Data.Vector
> 
> How could this statement be included "automatically"?

in Imperative-HOL this is done the following way:

> code_include Haskell "Heap"
> {*import qualified Control.Monad;
> import qualified Control.Monad.ST;
> import qualified Data.STRef;
> import qualified Data.Array.ST;
> 
> type RealWorld = Control.Monad.ST.RealWorld;
> type ST s a = Control.Monad.ST.ST s a;
> type STRef s a = Data.STRef.STRef s a;
> type STArray s a = Data.Array.ST.STArray s Integer a;
> 
> newSTRef = Data.STRef.newSTRef;
> readSTRef = Data.STRef.readSTRef;
> writeSTRef = Data.STRef.writeSTRef;
> 
> newArray :: Integer -> a -> ST s (STArray s a);
> newArray k = Data.Array.ST.newArray (0, k);
> 
> newListArray :: [a] -> ST s (STArray s a);
> newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
> 
> newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
> newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
> 
> lengthArray :: STArray s a -> ST s Integer;
> lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
> 
> readArray :: STArray s a -> Integer -> ST s a;
> readArray = Data.Array.ST.readArray;
> 
> writeArray :: STArray s a -> Integer -> a -> ST s ();
> writeArray = Data.Array.ST.writeArray;*}

I. e. you setup a include which includes everything you need and brings
that into its own name space.  This include is always imported, and you
can access the ingredients from generate code then.

> 2. Additionally, in order to compile the obtained code, I had to
> install "cabal" in my computer and install the following library:
> 
> cabal install vector
> 
> http://www.haskell.org/haskellwiki/Numeric_Haskell:_A_Vector_Tutorial#Importing_the_library
> 
> Is "Data.Vector" a "canonical" library? Can it be used "reliably"
> (with respect to future behavior or methods modifications)?

I have no idea how »canonical« this is.  Roughly I know that Haskell
provides also »frozen« arrays which do not allow modifications unless
»thawed« (which then results in a copy at runtime, I guess).  Note that
using includes also enables you to write your own types on top of
existing target language libraries, cf. the setup for Scala in
Imperative_HOL/Heap_Monad.thy

> As an additional question, does anybody know of a suitable OCaml data
> type to which "iarray" can be serialised?

In the worst case, write an include in which you define your own
immutable arrays on top of mutable ones, using an abstract datatype.

Hope this helps,
	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.