src/HOL/Imperative_HOL/Heap_Monad.thy
author haftmann
Fri Jul 09 16:58:44 2010 +0200 (2010-07-09)
changeset 37758 bf86a65403a8
parent 37756 59caa6180fff
child 37771 1bec64044b5e
permissions -rw-r--r--
pervasive success combinator
     1 (*  Title:      HOL/Library/Heap_Monad.thy
     2     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* A monad with a polymorphic heap *}
     6 
     7 theory Heap_Monad
     8 imports Heap
     9 begin
    10 
    11 subsection {* The monad *}
    12 
    13 subsubsection {* Monad construction *}
    14 
    15 text {* Monadic heap actions either produce values
    16   and transform the heap, or fail *}
    17 datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    18 
    19 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
    20   [code del]: "execute (Heap f) = f"
    21 
    22 lemma Heap_cases [case_names succeed fail]:
    23   fixes f and h
    24   assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    25   assumes fail: "execute f h = None \<Longrightarrow> P"
    26   shows P
    27   using assms by (cases "execute f h") auto
    28 
    29 lemma Heap_execute [simp]:
    30   "Heap (execute f) = f" by (cases f) simp_all
    31 
    32 lemma Heap_eqI:
    33   "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
    34     by (cases f, cases g) (auto simp: expand_fun_eq)
    35 
    36 ML {* structure Execute_Simps = Named_Thms(
    37   val name = "execute_simps"
    38   val description = "simplification rules for execute"
    39 ) *}
    40 
    41 setup Execute_Simps.setup
    42 
    43 lemma execute_Let [simp, execute_simps]:
    44   "execute (let x = t in f x) = (let x = t in execute (f x))"
    45   by (simp add: Let_def)
    46 
    47 
    48 subsubsection {* Specialised lifters *}
    49 
    50 definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
    51   [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
    52 
    53 lemma execute_tap [simp, execute_simps]:
    54   "execute (tap f) h = Some (f h, h)"
    55   by (simp add: tap_def)
    56 
    57 definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    58   [code del]: "heap f = Heap (Some \<circ> f)"
    59 
    60 lemma execute_heap [simp, execute_simps]:
    61   "execute (heap f) = Some \<circ> f"
    62   by (simp add: heap_def)
    63 
    64 definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    65   [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
    66 
    67 lemma execute_guard [execute_simps]:
    68   "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
    69   "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
    70   by (simp_all add: guard_def)
    71 
    72 
    73 subsubsection {* Predicate classifying successful computations *}
    74 
    75 definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
    76   "success f h \<longleftrightarrow> execute f h \<noteq> None"
    77 
    78 lemma successI:
    79   "execute f h \<noteq> None \<Longrightarrow> success f h"
    80   by (simp add: success_def)
    81 
    82 lemma successE:
    83   assumes "success f h"
    84   obtains r h' where "execute f h = Some (r, h')"
    85   using assms by (auto simp add: success_def)
    86 
    87 ML {* structure Success_Intros = Named_Thms(
    88   val name = "success_intros"
    89   val description = "introduction rules for success"
    90 ) *}
    91 
    92 setup Success_Intros.setup
    93 
    94 lemma success_tapI [iff, success_intros]:
    95   "success (tap f) h"
    96   by (rule successI) simp
    97 
    98 lemma success_heapI [iff, success_intros]:
    99   "success (heap f) h"
   100   by (rule successI) simp
   101 
   102 lemma success_guardI [success_intros]:
   103   "P h \<Longrightarrow> success (guard P f) h"
   104   by (rule successI) (simp add: execute_guard)
   105 
   106 lemma success_LetI [success_intros]:
   107   "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
   108   by (simp add: Let_def)
   109 
   110 
   111 subsubsection {* Monad combinators *}
   112 
   113 definition return :: "'a \<Rightarrow> 'a Heap" where
   114   [code del]: "return x = heap (Pair x)"
   115 
   116 lemma execute_return [simp, execute_simps]:
   117   "execute (return x) = Some \<circ> Pair x"
   118   by (simp add: return_def)
   119 
   120 lemma success_returnI [iff, success_intros]:
   121   "success (return x) h"
   122   by (rule successI) simp
   123 
   124 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   125   [code del]: "raise s = Heap (\<lambda>_. None)"
   126 
   127 lemma execute_raise [simp, execute_simps]:
   128   "execute (raise s) = (\<lambda>_. None)"
   129   by (simp add: raise_def)
   130 
   131 definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   132   [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
   133                   Some (x, h') \<Rightarrow> execute (g x) h'
   134                 | None \<Rightarrow> None)"
   135 
   136 notation bind (infixl "\<guillemotright>=" 54)
   137 
   138 lemma execute_bind [execute_simps]:
   139   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   140   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   141   by (simp_all add: bind_def)
   142 
   143 lemma success_bindI [success_intros]:
   144   "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
   145   by (auto intro!: successI elim!: successE simp add: bind_def)
   146 
   147 lemma execute_bind_successI [execute_simps]:
   148   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   149   by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   150   
   151 lemma execute_eq_SomeI:
   152   assumes "Heap_Monad.execute f h = Some (x, h')"
   153     and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   154   shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
   155   using assms by (simp add: bind_def)
   156 
   157 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   158   by (rule Heap_eqI) (simp add: execute_bind)
   159 
   160 lemma bind_return [simp]: "f \<guillemotright>= return = f"
   161   by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   162 
   163 lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   164   by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   165 
   166 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   167   by (rule Heap_eqI) (simp add: execute_bind)
   168 
   169 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   170   "f >> g \<equiv> f >>= (\<lambda>_. g)"
   171 
   172 notation chain (infixl "\<guillemotright>" 54)
   173 
   174 
   175 subsubsection {* do-syntax *}
   176 
   177 text {*
   178   We provide a convenient do-notation for monadic expressions
   179   well-known from Haskell.  @{const Let} is printed
   180   specially in do-expressions.
   181 *}
   182 
   183 nonterminals do_expr
   184 
   185 syntax
   186   "_do" :: "do_expr \<Rightarrow> 'a"
   187     ("(do (_)//done)" [12] 100)
   188   "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   189     ("_ <- _;//_" [1000, 13, 12] 12)
   190   "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   191     ("_;//_" [13, 12] 12)
   192   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   193     ("let _ = _;//_" [1000, 13, 12] 12)
   194   "_nil" :: "'a \<Rightarrow> do_expr"
   195     ("_" [12] 12)
   196 
   197 syntax (xsymbols)
   198   "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   199     ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
   200 
   201 translations
   202   "_do f" => "f"
   203   "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   204   "_chain f g" => "f \<guillemotright> g"
   205   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   206   "_nil f" => "f"
   207 
   208 print_translation {*
   209 let
   210   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   211         let
   212           val (v, t) = Syntax.variant_abs abs;
   213         in (Free (v, ty), t) end
   214     | dest_abs_eta t =
   215         let
   216           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   217         in (Free (v, dummyT), t) end;
   218   fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
   219         let
   220           val (v, g') = dest_abs_eta g;
   221           val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
   222           val v_used = fold_aterms
   223             (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
   224         in if v_used then
   225           Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
   226         else
   227           Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
   228         end
   229     | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
   230         Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
   231     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   232         let
   233           val (v, g') = dest_abs_eta g;
   234         in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
   235     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   236         Const (@{const_syntax return}, dummyT) $ f
   237     | unfold_monad f = f;
   238   fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
   239     | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   240         contains_bind t;
   241   fun bind_monad_tr' (f::g::ts) = list_comb
   242     (Const (@{syntax_const "_do"}, dummyT) $
   243       unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
   244   fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   245     if contains_bind g' then list_comb
   246       (Const (@{syntax_const "_do"}, dummyT) $
   247         unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   248     else raise Match;
   249 in
   250  [(@{const_syntax bind}, bind_monad_tr'),
   251   (@{const_syntax Let}, Let_monad_tr')]
   252 end;
   253 *}
   254 
   255 
   256 subsection {* Generic combinators *}
   257 
   258 subsubsection {* Assertions *}
   259 
   260 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   261   "assert P x = (if P x then return x else raise ''assert'')"
   262 
   263 lemma execute_assert [execute_simps]:
   264   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   265   "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   266   by (simp_all add: assert_def)
   267 
   268 lemma success_assertI [success_intros]:
   269   "P x \<Longrightarrow> success (assert P x) h"
   270   by (rule successI) (simp add: execute_assert)
   271 
   272 lemma assert_cong [fundef_cong]:
   273   assumes "P = P'"
   274   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   275   shows "(assert P x >>= f) = (assert P' x >>= f')"
   276   by (rule Heap_eqI) (insert assms, simp add: assert_def)
   277 
   278 
   279 subsubsection {* Plain lifting *}
   280 
   281 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   282   "lift f = return o f"
   283 
   284 lemma lift_collapse [simp]:
   285   "lift f x = return (f x)"
   286   by (simp add: lift_def)
   287 
   288 lemma bind_lift:
   289   "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   290   by (simp add: lift_def comp_def)
   291 
   292 
   293 subsubsection {* Iteration -- warning: this is rarely useful! *}
   294 
   295 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   296   "fold_map f [] = return []"
   297 | "fold_map f (x # xs) = do
   298      y \<leftarrow> f x;
   299      ys \<leftarrow> fold_map f xs;
   300      return (y # ys)
   301    done"
   302 
   303 lemma fold_map_append:
   304   "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   305   by (induct xs) simp_all
   306 
   307 lemma execute_fold_map_unchanged_heap [execute_simps]:
   308   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   309   shows "execute (fold_map f xs) h =
   310     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   311 using assms proof (induct xs)
   312   case Nil show ?case by simp
   313 next
   314   case (Cons x xs)
   315   from Cons.prems obtain y
   316     where y: "execute (f x) h = Some (y, h)" by auto
   317   moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   318     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   319   ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   320 qed
   321 
   322 
   323 subsubsection {* A monadic combinator for simple recursive functions *}
   324 
   325 text {* Using a locale to fix arguments f and g of MREC *}
   326 
   327 locale mrec =
   328   fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
   329   and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
   330 begin
   331 
   332 function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
   333   "mrec x h = (case execute (f x) h of
   334      Some (Inl r, h') \<Rightarrow> Some (r, h')
   335    | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
   336              Some (z, h'') \<Rightarrow> execute (g x s z) h''
   337            | None \<Rightarrow> None)
   338    | None \<Rightarrow> None)"
   339 by auto
   340 
   341 lemma graph_implies_dom:
   342   "mrec_graph x y \<Longrightarrow> mrec_dom x"
   343 apply (induct rule:mrec_graph.induct) 
   344 apply (rule accpI)
   345 apply (erule mrec_rel.cases)
   346 by simp
   347 
   348 lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
   349   unfolding mrec_def 
   350   by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
   351 
   352 lemma mrec_di_reverse: 
   353   assumes "\<not> mrec_dom (x, h)"
   354   shows "
   355    (case execute (f x) h of
   356      Some (Inl r, h') \<Rightarrow> False
   357    | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
   358    | None \<Rightarrow> False
   359    )" 
   360 using assms apply (auto split: option.split sum.split)
   361 apply (rule ccontr)
   362 apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
   363 done
   364 
   365 lemma mrec_rule:
   366   "mrec x h = 
   367    (case execute (f x) h of
   368      Some (Inl r, h') \<Rightarrow> Some (r, h')
   369    | Some (Inr s, h') \<Rightarrow> 
   370           (case mrec s h' of
   371              Some (z, h'') \<Rightarrow> execute (g x s z) h''
   372            | None \<Rightarrow> None)
   373    | None \<Rightarrow> None
   374    )"
   375 apply (cases "mrec_dom (x,h)", simp)
   376 apply (frule mrec_default)
   377 apply (frule mrec_di_reverse, simp)
   378 by (auto split: sum.split option.split simp: mrec_default)
   379 
   380 definition
   381   "MREC x = Heap (mrec x)"
   382 
   383 lemma MREC_rule:
   384   "MREC x = 
   385   (do y \<leftarrow> f x;
   386                 (case y of 
   387                 Inl r \<Rightarrow> return r
   388               | Inr s \<Rightarrow> 
   389                 do z \<leftarrow> MREC s ;
   390                    g x s z
   391                 done) done)"
   392   unfolding MREC_def
   393   unfolding bind_def return_def
   394   apply simp
   395   apply (rule ext)
   396   apply (unfold mrec_rule[of x])
   397   by (auto split: option.splits prod.splits sum.splits)
   398 
   399 lemma MREC_pinduct:
   400   assumes "execute (MREC x) h = Some (r, h')"
   401   assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
   402   assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
   403     \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
   404   shows "P x h h' r"
   405 proof -
   406   from assms(1) have mrec: "mrec x h = Some (r, h')"
   407     unfolding MREC_def execute.simps .
   408   from mrec have dom: "mrec_dom (x, h)"
   409     apply -
   410     apply (rule ccontr)
   411     apply (drule mrec_default) by auto
   412   from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
   413     by auto
   414   from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
   415   proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
   416     case (1 x h)
   417     obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
   418     show ?case
   419     proof (cases "execute (f x) h")
   420       case (Some result)
   421       then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
   422       note Inl' = this
   423       show ?thesis
   424       proof (cases a)
   425         case (Inl aa)
   426         from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
   427           by auto
   428       next
   429         case (Inr b)
   430         note Inr' = this
   431         show ?thesis
   432         proof (cases "mrec b h1")
   433           case (Some result)
   434           then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
   435           moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
   436             apply (intro 1(2))
   437             apply (auto simp add: Inr Inl')
   438             done
   439           moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
   440           ultimately show ?thesis
   441             apply auto
   442             apply (rule rec_case)
   443             apply auto
   444             unfolding MREC_def by auto
   445         next
   446           case None
   447           from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
   448         qed
   449       qed
   450     next
   451       case None
   452       from this 1(1) mrec 1(3) show ?thesis by simp
   453     qed
   454   qed
   455   from this h'_r show ?thesis by simp
   456 qed
   457 
   458 end
   459 
   460 text {* Providing global versions of the constant and the theorems *}
   461 
   462 abbreviation "MREC == mrec.MREC"
   463 lemmas MREC_rule = mrec.MREC_rule
   464 lemmas MREC_pinduct = mrec.MREC_pinduct
   465 
   466 
   467 subsection {* Code generator setup *}
   468 
   469 subsubsection {* Logical intermediate layer *}
   470 
   471 primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
   472   [code del, code_post]: "raise' (STR s) = raise s"
   473 
   474 lemma raise_raise' [code_inline]:
   475   "raise s = raise' (STR s)"
   476   by simp
   477 
   478 code_datatype raise' -- {* avoid @{const "Heap"} formally *}
   479 
   480 
   481 subsubsection {* SML and OCaml *}
   482 
   483 code_type Heap (SML "unit/ ->/ _")
   484 code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
   485 code_const return (SML "!(fn/ ()/ =>/ _)")
   486 code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
   487 
   488 code_type Heap (OCaml "unit/ ->/ _")
   489 code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   490 code_const return (OCaml "!(fun/ ()/ ->/ _)")
   491 code_const Heap_Monad.raise' (OCaml "failwith/ _")
   492 
   493 setup {*
   494 
   495 let
   496 
   497 open Code_Thingol;
   498 
   499 fun imp_program naming =
   500 
   501   let
   502     fun is_const c = case lookup_const naming c
   503      of SOME c' => (fn c'' => c' = c'')
   504       | NONE => K false;
   505     val is_bind = is_const @{const_name bind};
   506     val is_return = is_const @{const_name return};
   507     val dummy_name = "";
   508     val dummy_type = ITyVar dummy_name;
   509     val dummy_case_term = IVar NONE;
   510     (*assumption: dummy values are not relevant for serialization*)
   511     val unitt = case lookup_const naming @{const_name Unity}
   512      of SOME unit' => IConst (unit', (([], []), []))
   513       | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
   514     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
   515       | dest_abs (t, ty) =
   516           let
   517             val vs = fold_varnames cons t [];
   518             val v = Name.variant vs "x";
   519             val ty' = (hd o fst o unfold_fun) ty;
   520           in ((SOME v, ty'), t `$ IVar (SOME v)) end;
   521     fun force (t as IConst (c, _) `$ t') = if is_return c
   522           then t' else t `$ unitt
   523       | force t = t `$ unitt;
   524     fun tr_bind' [(t1, _), (t2, ty2)] =
   525       let
   526         val ((v, ty), t) = dest_abs (t2, ty2);
   527       in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
   528     and tr_bind'' t = case unfold_app t
   529          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
   530               then tr_bind' [(x1, ty1), (x2, ty2)]
   531               else force t
   532           | _ => force t;
   533     fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
   534       [(unitt, tr_bind' ts)]), dummy_case_term)
   535     and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
   536        of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
   537         | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
   538         | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
   539       else IConst const `$$ map imp_monad_bind ts
   540     and imp_monad_bind (IConst const) = imp_monad_bind' const []
   541       | imp_monad_bind (t as IVar _) = t
   542       | imp_monad_bind (t as _ `$ _) = (case unfold_app t
   543          of (IConst const, ts) => imp_monad_bind' const ts
   544           | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
   545       | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
   546       | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
   547           (((imp_monad_bind t, ty),
   548             (map o pairself) imp_monad_bind pats),
   549               imp_monad_bind t0);
   550 
   551   in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
   552 
   553 in
   554 
   555 Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   556 #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
   557 
   558 end
   559 
   560 *}
   561 
   562 
   563 subsubsection {* Haskell *}
   564 
   565 text {* Adaption layer *}
   566 
   567 code_include Haskell "Heap"
   568 {*import qualified Control.Monad;
   569 import qualified Control.Monad.ST;
   570 import qualified Data.STRef;
   571 import qualified Data.Array.ST;
   572 
   573 type RealWorld = Control.Monad.ST.RealWorld;
   574 type ST s a = Control.Monad.ST.ST s a;
   575 type STRef s a = Data.STRef.STRef s a;
   576 type STArray s a = Data.Array.ST.STArray s Int a;
   577 
   578 newSTRef = Data.STRef.newSTRef;
   579 readSTRef = Data.STRef.readSTRef;
   580 writeSTRef = Data.STRef.writeSTRef;
   581 
   582 newArray :: (Int, Int) -> a -> ST s (STArray s a);
   583 newArray = Data.Array.ST.newArray;
   584 
   585 newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
   586 newListArray = Data.Array.ST.newListArray;
   587 
   588 lengthArray :: STArray s a -> ST s Int;
   589 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
   590 
   591 readArray :: STArray s a -> Int -> ST s a;
   592 readArray = Data.Array.ST.readArray;
   593 
   594 writeArray :: STArray s a -> Int -> a -> ST s ();
   595 writeArray = Data.Array.ST.writeArray;*}
   596 
   597 code_reserved Haskell Heap
   598 
   599 text {* Monad *}
   600 
   601 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   602 code_monad "op \<guillemotright>=" Haskell
   603 code_const return (Haskell "return")
   604 code_const Heap_Monad.raise' (Haskell "error/ _")
   605 
   606 hide_const (open) Heap heap guard raise' fold_map
   607 
   608 end