Re: [isabelle] Haskell code generation for Imperative/HOL



A small update:

one can use

code_printing code_module "RunST" â (Haskell)
âimport qualified Control.Monad.ST; 
import qualified System.IO.Unsafe;
runST = System.IO.Unsafe.unsafePerformIO . Control.Monad.ST.stToIO;â

to make the generated code compile. However, this seems a bit odd to use
the unsafePerformIO-operation where there is the safe runST in Haskell.

Cheers,
RenÃ

PS: The problem appears both in Isabelle2016 and Isabelle2016-1-RC0

> Am 20.10.2016 um 23:50 schrieb Thiemann, Rene <Rene.Thiemann at uibk.ac.at>:
> 
> Dear all,
> 
> I just played a bit around with Imperative/HOL and got into the following problem:
> 
> I want to use imperative HOL to run some imperative code within a functional program to increase the efficiency of some intermediate computation. So, in particular I need a function similar to Isabelle's âexecuteâ
> or Haskellâs ârunSTâ. 
> 
> The following theory describes the problems I ran into, and I would be grateful for any hints.
> 
> Cheers,
> RenÃ
> 
> theory Head_Imperative
>  imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"  
>  "$AFP/Show/Show_Instances"
>  "~~/src/HOL/Library/Code_Target_Numeral"
>  "~~/src/HOL/Library/Code_Char"
> begin
> 
> (* example monadic function: compute the head of a list via arrays *)
> definition "head (xs :: nat list) = do {
>   a <- Array.of_list xs;
>   Array.nth a 0}" 
> 
> lemma head_sound_as_effect: "xs â [] â effect (head xs) h (snd (Array.alloc xs h)) (hd xs)" 
>  unfolding head_def 
>  (* there clearly is a better proof by using the framework lemmas,
>     but this is not the problem *)
>  by (cases h, cases xs, auto simp: execute_simps effect_def
>    Heap_Monad.heap_def Array.set_def Array.get_def
>   Array.alloc_def o_def Let_def Array.nth_def Array.length_def guard_def)
> 
> definition run_ST :: "'a Heap â 'a" where
>  [code del]: "run_ST h = fst (the (execute h (undefined ''heap'')))" (* or Heap.empty *)
> 
> (* run_ST admits to go outside the ST monad again and reason via the
>   functional result of the computation  *)
> lemma run_ST_effect: assumes "â h. â h'. effect c h h' r"
>  shows "run_ST c = r" 
> proof -
>  from assms obtain h' where "effect c (undefined ''heap'') h' r" by auto
>  thus ?thesis unfolding run_ST_def effect_def by simp
> qed
> 
> definition "head_functional xs = run_ST (head xs)" 
> 
> lemma head_sound_as_functional_program: "xs â [] â head_functional xs = hd xs" 
>  unfolding head_functional_def
>  using run_ST_effect head_sound_as_effect by metis
> 
> 
> (* this code belongs into the code-setup for Heap, cf. the code-printing in Heap_Monad *)
> code_printing constant run_ST â (Haskell) "RunST.runST"
> 
> code_printing code_module "RunST" â (Haskell)
> âimport qualified Control.Monad.ST; 
> runST = Control.Monad.ST.runST;â
> 
> 
> 
> definition "test = show (head_functional [17,90,2])"
> export_code test in Haskell module_name Head
> 
> (* the problem now is the type-signature in the generated code of
> 
> nth ::
>  forall a.
>    (Heapa a) => Heap.STArray Heap.RealWorld a ->
>                   Nat -> Heap.ST Heap.RealWorld a;
> nth a n = Heap.readArray a (integer_of_nat n);
> 
> and
> 
> head :: [Nat] -> Heap.ST Heap.RealWorld Nat;
> head xs = do { 
>            a <- Heap.newListArray xs;
>            nth a zero_nat
>           };
> 
> because of the code_printing setup in Heap_Monad
> 
> type RealWorld = Control.Monad.ST.RealWorld; 
> 
> type_constructor Heap â (Haskell) "Heap.ST/ Heap.RealWorld/ _"
> 
> 
> 
> The problem is that the type of the Haskell function runST is of
> type forall a. ((forall s. ST s a) -> a), so that in particular the
>  state in the ST monad must be arbitrary, but not a fixed type like RealWorld.
> 
> So, the proper code-printing would be 
> 
> type_constructor Heap â (Haskell) "Heap.ST/ s/ _" 
> 
> where "s" is some additional type variable. (ST in Haskell requires
> two type parameters, one for state, the other for the return type). 
> 
> 
> Now there is the problem, that I don't know how to tell the code-generator
> to observe the heap/ST type as binary, although it is unary in Isabelle.
> 
> In particular, the type of nth and head have to become
> 
> nth ::
>  forall a s.
>    (Heapa a) => Heap.STArray s a -> Nat -> Heap.ST s a;
> 
> head :: forall s. [Nat] -> Heap.ST s Nat;
> 
> where the s is quantified. Once one performs this change, compilation and
> execution works as expected.
> 
> *)
> end



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