*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Haskell code generation for Imperative/HOL*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Thu, 20 Oct 2016 21:50:01 +0000*Accept-language*: de-DE, de-AT, en-US*Thread-index*: AQHSKxvoDPPA29fTV0OS7yT5oTlZPQ==*Thread-topic*: 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

**Follow-Ups**:**Re: [isabelle] Haskell code generation for Imperative/HOL***From:*Thiemann, Rene

- Previous by Date: [isabelle] HOL-Algebra breaks "algebra" method
- Next by Date: Re: [isabelle] Haskell code generation for Imperative/HOL
- Previous by Thread: Re: [isabelle] HOL-Algebra breaks "algebra" method
- Next by Thread: Re: [isabelle] Haskell code generation for Imperative/HOL
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list