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



Hi Rene,

Am 21.10.2016 um 08:16 schrieb Thiemann, Rene:
> 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.

this indeed is the core of the problem: there is a safe runST in
Haskell, but I have found no way to express this adequately in the HOL
type system.  Early code generation setups for Imperative HOL attempted
this but that never worked out.

Hope this helps,
	Florian

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

-- 

PGP available:
http://isabelle.in.tum.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.