src/HOL/Imperative_HOL/Heap_Monad.thy
author haftmann
Tue Jul 13 11:38:03 2010 +0200 (2010-07-13)
changeset 37787 30dc3abf4a58
parent 37772 026ed2fc15d4
child 37792 ba0bc31b90d7
permissions -rw-r--r--
theorem collections do not contain default rules any longer
     1 (*  Title:      HOL/Imperative_HOL/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 and primitive reasoning infrastructure *}
     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 [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 [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 [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 "r = fst (the (execute c h))"
    85     and "h' = snd (the (execute c h))"
    86     and "execute f h \<noteq> None"
    87   using assms by (simp add: success_def)
    88 
    89 ML {* structure Success_Intros = Named_Thms(
    90   val name = "success_intros"
    91   val description = "introduction rules for success"
    92 ) *}
    93 
    94 setup Success_Intros.setup
    95 
    96 lemma success_tapI [success_intros]:
    97   "success (tap f) h"
    98   by (rule successI) (simp add: execute_simps)
    99 
   100 lemma success_heapI [success_intros]:
   101   "success (heap f) h"
   102   by (rule successI) (simp add: execute_simps)
   103 
   104 lemma success_guardI [success_intros]:
   105   "P h \<Longrightarrow> success (guard P f) h"
   106   by (rule successI) (simp add: execute_guard)
   107 
   108 lemma success_LetI [success_intros]:
   109   "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
   110   by (simp add: Let_def)
   111 
   112 lemma success_ifI:
   113   "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
   114     success (if c then t else e) h"
   115   by (simp add: success_def)
   116 
   117 
   118 subsubsection {* Predicate for a simple relational calculus *}
   119 
   120 text {*
   121   The @{text crel} predicate states that when a computation @{text c}
   122   runs with the heap @{text h} will result in return value @{text r}
   123   and a heap @{text "h'"}, i.e.~no exception occurs.
   124 *}  
   125 
   126 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
   127   crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
   128 
   129 lemma crelI:
   130   "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
   131   by (simp add: crel_def)
   132 
   133 lemma crelE:
   134   assumes "crel c h h' r"
   135   obtains "r = fst (the (execute c h))"
   136     and "h' = snd (the (execute c h))"
   137     and "success c h"
   138 proof (rule that)
   139   from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
   140   then show "success c h" by (simp add: success_def)
   141   from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
   142     by simp_all
   143   then show "r = fst (the (execute c h))"
   144     and "h' = snd (the (execute c h))" by simp_all
   145 qed
   146 
   147 lemma crel_success:
   148   "crel c h h' r \<Longrightarrow> success c h"
   149   by (simp add: crel_def success_def)
   150 
   151 lemma success_crelE:
   152   assumes "success c h"
   153   obtains r h' where "crel c h h' r"
   154   using assms by (auto simp add: crel_def success_def)
   155 
   156 lemma crel_deterministic:
   157   assumes "crel f h h' a"
   158     and "crel f h h'' b"
   159   shows "a = b" and "h' = h''"
   160   using assms unfolding crel_def by auto
   161 
   162 ML {* structure Crel_Intros = Named_Thms(
   163   val name = "crel_intros"
   164   val description = "introduction rules for crel"
   165 ) *}
   166 
   167 ML {* structure Crel_Elims = Named_Thms(
   168   val name = "crel_elims"
   169   val description = "elimination rules for crel"
   170 ) *}
   171 
   172 setup "Crel_Intros.setup #> Crel_Elims.setup"
   173 
   174 lemma crel_LetI [crel_intros]:
   175   assumes "x = t" "crel (f x) h h' r"
   176   shows "crel (let x = t in f x) h h' r"
   177   using assms by simp
   178 
   179 lemma crel_LetE [crel_elims]:
   180   assumes "crel (let x = t in f x) h h' r"
   181   obtains "crel (f t) h h' r"
   182   using assms by simp
   183 
   184 lemma crel_ifI:
   185   assumes "c \<Longrightarrow> crel t h h' r"
   186     and "\<not> c \<Longrightarrow> crel e h h' r"
   187   shows "crel (if c then t else e) h h' r"
   188   by (cases c) (simp_all add: assms)
   189 
   190 lemma crel_ifE:
   191   assumes "crel (if c then t else e) h h' r"
   192   obtains "c" "crel t h h' r"
   193     | "\<not> c" "crel e h h' r"
   194   using assms by (cases c) simp_all
   195 
   196 lemma crel_tapI [crel_intros]:
   197   assumes "h' = h" "r = f h"
   198   shows "crel (tap f) h h' r"
   199   by (rule crelI) (simp add: assms execute_simps)
   200 
   201 lemma crel_tapE [crel_elims]:
   202   assumes "crel (tap f) h h' r"
   203   obtains "h' = h" and "r = f h"
   204   using assms by (rule crelE) (auto simp add: execute_simps)
   205 
   206 lemma crel_heapI [crel_intros]:
   207   assumes "h' = snd (f h)" "r = fst (f h)"
   208   shows "crel (heap f) h h' r"
   209   by (rule crelI) (simp add: assms execute_simps)
   210 
   211 lemma crel_heapE [crel_elims]:
   212   assumes "crel (heap f) h h' r"
   213   obtains "h' = snd (f h)" and "r = fst (f h)"
   214   using assms by (rule crelE) (simp add: execute_simps)
   215 
   216 lemma crel_guardI [crel_intros]:
   217   assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   218   shows "crel (guard P f) h h' r"
   219   by (rule crelI) (simp add: assms execute_simps)
   220 
   221 lemma crel_guardE [crel_elims]:
   222   assumes "crel (guard P f) h h' r"
   223   obtains "h' = snd (f h)" "r = fst (f h)" "P h"
   224   using assms by (rule crelE)
   225     (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
   226 
   227 
   228 subsubsection {* Monad combinators *}
   229 
   230 definition return :: "'a \<Rightarrow> 'a Heap" where
   231   [code del]: "return x = heap (Pair x)"
   232 
   233 lemma execute_return [execute_simps]:
   234   "execute (return x) = Some \<circ> Pair x"
   235   by (simp add: return_def execute_simps)
   236 
   237 lemma success_returnI [success_intros]:
   238   "success (return x) h"
   239   by (rule successI) (simp add: execute_simps)
   240 
   241 lemma crel_returnI [crel_intros]:
   242   "h = h' \<Longrightarrow> crel (return x) h h' x"
   243   by (rule crelI) (simp add: execute_simps)
   244 
   245 lemma crel_returnE [crel_elims]:
   246   assumes "crel (return x) h h' r"
   247   obtains "r = x" "h' = h"
   248   using assms by (rule crelE) (simp add: execute_simps)
   249 
   250 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   251   [code del]: "raise s = Heap (\<lambda>_. None)"
   252 
   253 lemma execute_raise [execute_simps]:
   254   "execute (raise s) = (\<lambda>_. None)"
   255   by (simp add: raise_def)
   256 
   257 lemma crel_raiseE [crel_elims]:
   258   assumes "crel (raise x) h h' r"
   259   obtains "False"
   260   using assms by (rule crelE) (simp add: success_def execute_simps)
   261 
   262 definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   263   [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
   264                   Some (x, h') \<Rightarrow> execute (g x) h'
   265                 | None \<Rightarrow> None)"
   266 
   267 notation bind (infixl "\<guillemotright>=" 54)
   268 
   269 lemma execute_bind [execute_simps]:
   270   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   271   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   272   by (simp_all add: bind_def)
   273 
   274 lemma execute_bind_success:
   275   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   276   by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   277 
   278 lemma success_bind_executeI:
   279   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   280   by (auto intro!: successI elim!: successE simp add: bind_def)
   281 
   282 lemma success_bind_crelI [success_intros]:
   283   "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   284   by (auto simp add: crel_def success_def bind_def)
   285 
   286 lemma crel_bindI [crel_intros]:
   287   assumes "crel f h h' r" "crel (g r) h' h'' r'"
   288   shows "crel (f \<guillemotright>= g) h h'' r'"
   289   using assms
   290   apply (auto intro!: crelI elim!: crelE successE)
   291   apply (subst execute_bind, simp_all)
   292   done
   293 
   294 lemma crel_bindE [crel_elims]:
   295   assumes "crel (f \<guillemotright>= g) h h'' r'"
   296   obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   297   using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   298 
   299 lemma execute_bind_eq_SomeI:
   300   assumes "Heap_Monad.execute f h = Some (x, h')"
   301     and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   302   shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
   303   using assms by (simp add: bind_def)
   304 
   305 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   306   by (rule Heap_eqI) (simp add: execute_bind execute_simps)
   307 
   308 lemma bind_return [simp]: "f \<guillemotright>= return = f"
   309   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   310 
   311 lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   312   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   313 
   314 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   315   by (rule Heap_eqI) (simp add: execute_simps)
   316 
   317 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   318   "f >> g \<equiv> f >>= (\<lambda>_. g)"
   319 
   320 notation chain (infixl "\<guillemotright>" 54)
   321 
   322 
   323 subsubsection {* do-syntax *}
   324 
   325 text {*
   326   We provide a convenient do-notation for monadic expressions
   327   well-known from Haskell.  @{const Let} is printed
   328   specially in do-expressions.
   329 *}
   330 
   331 nonterminals do_expr
   332 
   333 syntax
   334   "_do" :: "do_expr \<Rightarrow> 'a"
   335     ("(do (_)//done)" [12] 100)
   336   "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   337     ("_ <- _;//_" [1000, 13, 12] 12)
   338   "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   339     ("_;//_" [13, 12] 12)
   340   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   341     ("let _ = _;//_" [1000, 13, 12] 12)
   342   "_nil" :: "'a \<Rightarrow> do_expr"
   343     ("_" [12] 12)
   344 
   345 syntax (xsymbols)
   346   "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   347     ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
   348 
   349 translations
   350   "_do f" => "f"
   351   "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   352   "_chain f g" => "f \<guillemotright> g"
   353   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   354   "_nil f" => "f"
   355 
   356 print_translation {*
   357 let
   358   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   359         let
   360           val (v, t) = Syntax.variant_abs abs;
   361         in (Free (v, ty), t) end
   362     | dest_abs_eta t =
   363         let
   364           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   365         in (Free (v, dummyT), t) end;
   366   fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
   367         let
   368           val (v, g') = dest_abs_eta g;
   369           val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
   370           val v_used = fold_aterms
   371             (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
   372         in if v_used then
   373           Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
   374         else
   375           Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
   376         end
   377     | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
   378         Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
   379     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   380         let
   381           val (v, g') = dest_abs_eta g;
   382         in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
   383     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   384         Const (@{const_syntax return}, dummyT) $ f
   385     | unfold_monad f = f;
   386   fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
   387     | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   388         contains_bind t;
   389   fun bind_monad_tr' (f::g::ts) = list_comb
   390     (Const (@{syntax_const "_do"}, dummyT) $
   391       unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
   392   fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   393     if contains_bind g' then list_comb
   394       (Const (@{syntax_const "_do"}, dummyT) $
   395         unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   396     else raise Match;
   397 in
   398  [(@{const_syntax bind}, bind_monad_tr'),
   399   (@{const_syntax Let}, Let_monad_tr')]
   400 end;
   401 *}
   402 
   403 
   404 subsection {* Generic combinators *}
   405 
   406 subsubsection {* Assertions *}
   407 
   408 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   409   "assert P x = (if P x then return x else raise ''assert'')"
   410 
   411 lemma execute_assert [execute_simps]:
   412   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   413   "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   414   by (simp_all add: assert_def execute_simps)
   415 
   416 lemma success_assertI [success_intros]:
   417   "P x \<Longrightarrow> success (assert P x) h"
   418   by (rule successI) (simp add: execute_assert)
   419 
   420 lemma crel_assertI [crel_intros]:
   421   "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
   422   by (rule crelI) (simp add: execute_assert)
   423  
   424 lemma crel_assertE [crel_elims]:
   425   assumes "crel (assert P x) h h' r"
   426   obtains "P x" "r = x" "h' = h"
   427   using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
   428 
   429 lemma assert_cong [fundef_cong]:
   430   assumes "P = P'"
   431   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   432   shows "(assert P x >>= f) = (assert P' x >>= f')"
   433   by (rule Heap_eqI) (insert assms, simp add: assert_def)
   434 
   435 
   436 subsubsection {* Plain lifting *}
   437 
   438 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   439   "lift f = return o f"
   440 
   441 lemma lift_collapse [simp]:
   442   "lift f x = return (f x)"
   443   by (simp add: lift_def)
   444 
   445 lemma bind_lift:
   446   "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   447   by (simp add: lift_def comp_def)
   448 
   449 
   450 subsubsection {* Iteration -- warning: this is rarely useful! *}
   451 
   452 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   453   "fold_map f [] = return []"
   454 | "fold_map f (x # xs) = do
   455      y \<leftarrow> f x;
   456      ys \<leftarrow> fold_map f xs;
   457      return (y # ys)
   458    done"
   459 
   460 lemma fold_map_append:
   461   "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   462   by (induct xs) simp_all
   463 
   464 lemma execute_fold_map_unchanged_heap [execute_simps]:
   465   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   466   shows "execute (fold_map f xs) h =
   467     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   468 using assms proof (induct xs)
   469   case Nil show ?case by (simp add: execute_simps)
   470 next
   471   case (Cons x xs)
   472   from Cons.prems obtain y
   473     where y: "execute (f x) h = Some (y, h)" by auto
   474   moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   475     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   476   ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
   477 qed
   478 
   479 subsection {* Code generator setup *}
   480 
   481 subsubsection {* Logical intermediate layer *}
   482 
   483 primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
   484   [code del, code_post]: "raise' (STR s) = raise s"
   485 
   486 lemma raise_raise' [code_inline]:
   487   "raise s = raise' (STR s)"
   488   by simp
   489 
   490 code_datatype raise' -- {* avoid @{const "Heap"} formally *}
   491 
   492 
   493 subsubsection {* SML and OCaml *}
   494 
   495 code_type Heap (SML "unit/ ->/ _")
   496 code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
   497 code_const return (SML "!(fn/ ()/ =>/ _)")
   498 code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
   499 
   500 code_type Heap (OCaml "unit/ ->/ _")
   501 code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   502 code_const return (OCaml "!(fun/ ()/ ->/ _)")
   503 code_const Heap_Monad.raise' (OCaml "failwith/ _")
   504 
   505 setup {*
   506 
   507 let
   508 
   509 open Code_Thingol;
   510 
   511 fun imp_program naming =
   512 
   513   let
   514     fun is_const c = case lookup_const naming c
   515      of SOME c' => (fn c'' => c' = c'')
   516       | NONE => K false;
   517     val is_bind = is_const @{const_name bind};
   518     val is_return = is_const @{const_name return};
   519     val dummy_name = "";
   520     val dummy_type = ITyVar dummy_name;
   521     val dummy_case_term = IVar NONE;
   522     (*assumption: dummy values are not relevant for serialization*)
   523     val unitt = case lookup_const naming @{const_name Unity}
   524      of SOME unit' => IConst (unit', (([], []), []))
   525       | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
   526     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
   527       | dest_abs (t, ty) =
   528           let
   529             val vs = fold_varnames cons t [];
   530             val v = Name.variant vs "x";
   531             val ty' = (hd o fst o unfold_fun) ty;
   532           in ((SOME v, ty'), t `$ IVar (SOME v)) end;
   533     fun force (t as IConst (c, _) `$ t') = if is_return c
   534           then t' else t `$ unitt
   535       | force t = t `$ unitt;
   536     fun tr_bind' [(t1, _), (t2, ty2)] =
   537       let
   538         val ((v, ty), t) = dest_abs (t2, ty2);
   539       in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
   540     and tr_bind'' t = case unfold_app t
   541          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
   542               then tr_bind' [(x1, ty1), (x2, ty2)]
   543               else force t
   544           | _ => force t;
   545     fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
   546       [(unitt, tr_bind' ts)]), dummy_case_term)
   547     and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
   548        of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
   549         | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
   550         | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
   551       else IConst const `$$ map imp_monad_bind ts
   552     and imp_monad_bind (IConst const) = imp_monad_bind' const []
   553       | imp_monad_bind (t as IVar _) = t
   554       | imp_monad_bind (t as _ `$ _) = (case unfold_app t
   555          of (IConst const, ts) => imp_monad_bind' const ts
   556           | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
   557       | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
   558       | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
   559           (((imp_monad_bind t, ty),
   560             (map o pairself) imp_monad_bind pats),
   561               imp_monad_bind t0);
   562 
   563   in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
   564 
   565 in
   566 
   567 Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   568 #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
   569 
   570 end
   571 
   572 *}
   573 
   574 
   575 subsubsection {* Haskell *}
   576 
   577 text {* Adaption layer *}
   578 
   579 code_include Haskell "Heap"
   580 {*import qualified Control.Monad;
   581 import qualified Control.Monad.ST;
   582 import qualified Data.STRef;
   583 import qualified Data.Array.ST;
   584 
   585 type RealWorld = Control.Monad.ST.RealWorld;
   586 type ST s a = Control.Monad.ST.ST s a;
   587 type STRef s a = Data.STRef.STRef s a;
   588 type STArray s a = Data.Array.ST.STArray s Int a;
   589 
   590 newSTRef = Data.STRef.newSTRef;
   591 readSTRef = Data.STRef.readSTRef;
   592 writeSTRef = Data.STRef.writeSTRef;
   593 
   594 newArray :: (Int, Int) -> a -> ST s (STArray s a);
   595 newArray = Data.Array.ST.newArray;
   596 
   597 newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
   598 newListArray = Data.Array.ST.newListArray;
   599 
   600 lengthArray :: STArray s a -> ST s Int;
   601 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
   602 
   603 readArray :: STArray s a -> Int -> ST s a;
   604 readArray = Data.Array.ST.readArray;
   605 
   606 writeArray :: STArray s a -> Int -> a -> ST s ();
   607 writeArray = Data.Array.ST.writeArray;*}
   608 
   609 code_reserved Haskell Heap
   610 
   611 text {* Monad *}
   612 
   613 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   614 code_monad "op \<guillemotright>=" Haskell
   615 code_const return (Haskell "return")
   616 code_const Heap_Monad.raise' (Haskell "error/ _")
   617 
   618 hide_const (open) Heap heap guard raise' fold_map
   619 
   620 end