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