Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation from IArray

view this post on Zulip Email Gateway (Aug 19 2022 at 12:04):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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.

  1. 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
signature.asc

Last updated: Apr 23 2024 at 16:19 UTC