[isabelle] Haskell code generation for Imperative/HOL



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.