haftmann@37787: (* Title: HOL/Imperative_HOL/Heap_Monad.thy haftmann@26170: Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen haftmann@26170: *) haftmann@26170: haftmann@37771: header {* A monad with a polymorphic heap and primitive reasoning infrastructure *} haftmann@26170: haftmann@26170: theory Heap_Monad krauss@37792: imports Heap Monad_Syntax haftmann@26170: begin haftmann@26170: haftmann@26170: subsection {* The monad *} haftmann@26170: haftmann@37758: subsubsection {* Monad construction *} haftmann@26170: haftmann@26170: text {* Monadic heap actions either produce values haftmann@26170: and transform the heap, or fail *} haftmann@37709: datatype 'a Heap = Heap "heap \ ('a \ heap) option" haftmann@26170: haftmann@37709: primrec execute :: "'a Heap \ heap \ ('a \ heap) option" where haftmann@37709: [code del]: "execute (Heap f) = f" haftmann@26170: haftmann@37758: lemma Heap_cases [case_names succeed fail]: haftmann@37758: fixes f and h haftmann@37758: assumes succeed: "\x h'. execute f h = Some (x, h') \ P" haftmann@37758: assumes fail: "execute f h = None \ P" haftmann@37758: shows P haftmann@37758: using assms by (cases "execute f h") auto haftmann@37758: haftmann@26170: lemma Heap_execute [simp]: haftmann@26170: "Heap (execute f) = f" by (cases f) simp_all haftmann@26170: haftmann@26170: lemma Heap_eqI: haftmann@26170: "(\h. execute f h = execute g h) \ f = g" haftmann@26170: by (cases f, cases g) (auto simp: expand_fun_eq) haftmann@26170: haftmann@37758: ML {* structure Execute_Simps = Named_Thms( haftmann@37758: val name = "execute_simps" haftmann@37758: val description = "simplification rules for execute" haftmann@37758: ) *} haftmann@37758: haftmann@37758: setup Execute_Simps.setup haftmann@37758: haftmann@37787: lemma execute_Let [execute_simps]: haftmann@37758: "execute (let x = t in f x) = (let x = t in execute (f x))" haftmann@37758: by (simp add: Let_def) haftmann@37758: haftmann@37758: haftmann@37758: subsubsection {* Specialised lifters *} haftmann@37758: haftmann@37758: definition tap :: "(heap \ 'a) \ 'a Heap" where haftmann@37758: [code del]: "tap f = Heap (\h. Some (f h, h))" haftmann@37758: haftmann@37787: lemma execute_tap [execute_simps]: haftmann@37758: "execute (tap f) h = Some (f h, h)" haftmann@37758: by (simp add: tap_def) haftmann@26170: haftmann@37709: definition heap :: "(heap \ 'a \ heap) \ 'a Heap" where haftmann@37709: [code del]: "heap f = Heap (Some \ f)" haftmann@26170: haftmann@37787: lemma execute_heap [execute_simps]: haftmann@37709: "execute (heap f) = Some \ f" haftmann@26170: by (simp add: heap_def) haftmann@26170: haftmann@37754: definition guard :: "(heap \ bool) \ (heap \ 'a \ heap) \ 'a Heap" where haftmann@37754: [code del]: "guard P f = Heap (\h. if P h then Some (f h) else None)" haftmann@37754: haftmann@37758: lemma execute_guard [execute_simps]: haftmann@37754: "\ P h \ execute (guard P f) h = None" haftmann@37754: "P h \ execute (guard P f) h = Some (f h)" haftmann@37754: by (simp_all add: guard_def) haftmann@37754: haftmann@37758: haftmann@37758: subsubsection {* Predicate classifying successful computations *} haftmann@37758: haftmann@37758: definition success :: "'a Heap \ heap \ bool" where haftmann@37758: "success f h \ execute f h \ None" haftmann@37758: haftmann@37758: lemma successI: haftmann@37758: "execute f h \ None \ success f h" haftmann@37758: by (simp add: success_def) haftmann@37758: haftmann@37758: lemma successE: haftmann@37758: assumes "success f h" haftmann@37771: obtains r h' where "r = fst (the (execute c h))" haftmann@37771: and "h' = snd (the (execute c h))" haftmann@37771: and "execute f h \ None" haftmann@37771: using assms by (simp add: success_def) haftmann@37758: haftmann@37758: ML {* structure Success_Intros = Named_Thms( haftmann@37758: val name = "success_intros" haftmann@37758: val description = "introduction rules for success" haftmann@37758: ) *} haftmann@37758: haftmann@37758: setup Success_Intros.setup haftmann@37758: haftmann@37787: lemma success_tapI [success_intros]: haftmann@37758: "success (tap f) h" haftmann@37787: by (rule successI) (simp add: execute_simps) haftmann@37758: haftmann@37787: lemma success_heapI [success_intros]: haftmann@37758: "success (heap f) h" haftmann@37787: by (rule successI) (simp add: execute_simps) haftmann@37758: haftmann@37758: lemma success_guardI [success_intros]: haftmann@37758: "P h \ success (guard P f) h" haftmann@37758: by (rule successI) (simp add: execute_guard) haftmann@37758: haftmann@37758: lemma success_LetI [success_intros]: haftmann@37758: "x = t \ success (f x) h \ success (let x = t in f x) h" haftmann@37758: by (simp add: Let_def) haftmann@37758: haftmann@37771: lemma success_ifI: haftmann@37771: "(c \ success t h) \ (\ c \ success e h) \ haftmann@37771: success (if c then t else e) h" haftmann@37771: by (simp add: success_def) haftmann@37771: haftmann@37771: haftmann@37771: subsubsection {* Predicate for a simple relational calculus *} haftmann@37771: haftmann@37771: text {* haftmann@37771: The @{text crel} predicate states that when a computation @{text c} haftmann@37771: runs with the heap @{text h} will result in return value @{text r} haftmann@37771: and a heap @{text "h'"}, i.e.~no exception occurs. haftmann@37771: *} haftmann@37771: haftmann@37771: definition crel :: "'a Heap \ heap \ heap \ 'a \ bool" where haftmann@37771: crel_def: "crel c h h' r \ Heap_Monad.execute c h = Some (r, h')" haftmann@37771: haftmann@37771: lemma crelI: haftmann@37771: "Heap_Monad.execute c h = Some (r, h') \ crel c h h' r" haftmann@37771: by (simp add: crel_def) haftmann@37771: haftmann@37771: lemma crelE: haftmann@37771: assumes "crel c h h' r" haftmann@37771: obtains "r = fst (the (execute c h))" haftmann@37771: and "h' = snd (the (execute c h))" haftmann@37771: and "success c h" haftmann@37771: proof (rule that) haftmann@37771: from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def) haftmann@37771: then show "success c h" by (simp add: success_def) haftmann@37771: from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'" haftmann@37771: by simp_all haftmann@37771: then show "r = fst (the (execute c h))" haftmann@37771: and "h' = snd (the (execute c h))" by simp_all haftmann@37771: qed haftmann@37771: haftmann@37771: lemma crel_success: haftmann@37771: "crel c h h' r \ success c h" haftmann@37771: by (simp add: crel_def success_def) haftmann@37771: haftmann@37771: lemma success_crelE: haftmann@37771: assumes "success c h" haftmann@37771: obtains r h' where "crel c h h' r" haftmann@37771: using assms by (auto simp add: crel_def success_def) haftmann@37771: haftmann@37771: lemma crel_deterministic: haftmann@37771: assumes "crel f h h' a" haftmann@37771: and "crel f h h'' b" haftmann@37771: shows "a = b" and "h' = h''" haftmann@37771: using assms unfolding crel_def by auto haftmann@37771: haftmann@37771: ML {* structure Crel_Intros = Named_Thms( haftmann@37771: val name = "crel_intros" haftmann@37771: val description = "introduction rules for crel" haftmann@37771: ) *} haftmann@37771: haftmann@37771: ML {* structure Crel_Elims = Named_Thms( haftmann@37771: val name = "crel_elims" haftmann@37771: val description = "elimination rules for crel" haftmann@37771: ) *} haftmann@37771: haftmann@37771: setup "Crel_Intros.setup #> Crel_Elims.setup" haftmann@37771: haftmann@37771: lemma crel_LetI [crel_intros]: haftmann@37771: assumes "x = t" "crel (f x) h h' r" haftmann@37771: shows "crel (let x = t in f x) h h' r" haftmann@37771: using assms by simp haftmann@37771: haftmann@37771: lemma crel_LetE [crel_elims]: haftmann@37771: assumes "crel (let x = t in f x) h h' r" haftmann@37771: obtains "crel (f t) h h' r" haftmann@37771: using assms by simp haftmann@37771: haftmann@37771: lemma crel_ifI: haftmann@37771: assumes "c \ crel t h h' r" haftmann@37771: and "\ c \ crel e h h' r" haftmann@37771: shows "crel (if c then t else e) h h' r" haftmann@37771: by (cases c) (simp_all add: assms) haftmann@37771: haftmann@37771: lemma crel_ifE: haftmann@37771: assumes "crel (if c then t else e) h h' r" haftmann@37771: obtains "c" "crel t h h' r" haftmann@37771: | "\ c" "crel e h h' r" haftmann@37771: using assms by (cases c) simp_all haftmann@37771: haftmann@37771: lemma crel_tapI [crel_intros]: haftmann@37771: assumes "h' = h" "r = f h" haftmann@37771: shows "crel (tap f) h h' r" haftmann@37787: by (rule crelI) (simp add: assms execute_simps) haftmann@37771: haftmann@37771: lemma crel_tapE [crel_elims]: haftmann@37771: assumes "crel (tap f) h h' r" haftmann@37771: obtains "h' = h" and "r = f h" haftmann@37787: using assms by (rule crelE) (auto simp add: execute_simps) haftmann@37771: haftmann@37771: lemma crel_heapI [crel_intros]: haftmann@37771: assumes "h' = snd (f h)" "r = fst (f h)" haftmann@37771: shows "crel (heap f) h h' r" haftmann@37787: by (rule crelI) (simp add: assms execute_simps) haftmann@37771: haftmann@37771: lemma crel_heapE [crel_elims]: haftmann@37771: assumes "crel (heap f) h h' r" haftmann@37771: obtains "h' = snd (f h)" and "r = fst (f h)" haftmann@37787: using assms by (rule crelE) (simp add: execute_simps) haftmann@37771: haftmann@37771: lemma crel_guardI [crel_intros]: haftmann@37771: assumes "P h" "h' = snd (f h)" "r = fst (f h)" haftmann@37771: shows "crel (guard P f) h h' r" haftmann@37771: by (rule crelI) (simp add: assms execute_simps) haftmann@37771: haftmann@37771: lemma crel_guardE [crel_elims]: haftmann@37771: assumes "crel (guard P f) h h' r" haftmann@37771: obtains "h' = snd (f h)" "r = fst (f h)" "P h" haftmann@37771: using assms by (rule crelE) haftmann@37771: (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps) haftmann@37771: haftmann@37758: haftmann@37758: subsubsection {* Monad combinators *} haftmann@26170: haftmann@37709: definition return :: "'a \ 'a Heap" where haftmann@26170: [code del]: "return x = heap (Pair x)" haftmann@26170: haftmann@37787: lemma execute_return [execute_simps]: haftmann@37709: "execute (return x) = Some \ Pair x" haftmann@37787: by (simp add: return_def execute_simps) haftmann@26170: haftmann@37787: lemma success_returnI [success_intros]: haftmann@37758: "success (return x) h" haftmann@37787: by (rule successI) (simp add: execute_simps) haftmann@37758: haftmann@37771: lemma crel_returnI [crel_intros]: haftmann@37771: "h = h' \ crel (return x) h h' x" haftmann@37787: by (rule crelI) (simp add: execute_simps) haftmann@37771: haftmann@37771: lemma crel_returnE [crel_elims]: haftmann@37771: assumes "crel (return x) h h' r" haftmann@37771: obtains "r = x" "h' = h" haftmann@37787: using assms by (rule crelE) (simp add: execute_simps) haftmann@37771: haftmann@37709: definition raise :: "string \ 'a Heap" where -- {* the string is just decoration *} haftmann@37709: [code del]: "raise s = Heap (\_. None)" haftmann@26170: haftmann@37787: lemma execute_raise [execute_simps]: haftmann@37709: "execute (raise s) = (\_. None)" haftmann@26170: by (simp add: raise_def) haftmann@26170: haftmann@37771: lemma crel_raiseE [crel_elims]: haftmann@37771: assumes "crel (raise x) h h' r" haftmann@37771: obtains "False" haftmann@37787: using assms by (rule crelE) (simp add: success_def execute_simps) haftmann@37771: krauss@37792: definition bind :: "'a Heap \ ('a \ 'b Heap) \ 'b Heap" where krauss@37792: [code del]: "bind f g = Heap (\h. case execute f h of haftmann@37709: Some (x, h') \ execute (g x) h' haftmann@37709: | None \ None)" haftmann@37709: krauss@37792: setup {* krauss@37792: Adhoc_Overloading.add_variant haftmann@37816: @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind} krauss@37792: *} krauss@37792: haftmann@37758: lemma execute_bind [execute_simps]: haftmann@37709: "execute f h = Some (x, h') \ execute (f \= g) h = execute (g x) h'" haftmann@37709: "execute f h = None \ execute (f \= g) h = None" haftmann@37756: by (simp_all add: bind_def) haftmann@37709: haftmann@37771: lemma execute_bind_success: haftmann@37771: "success f h \ execute (f \= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))" haftmann@37771: by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def) haftmann@37771: haftmann@37771: lemma success_bind_executeI: haftmann@37771: "execute f h = Some (x, h') \ success (g x) h' \ success (f \= g) h" haftmann@37758: by (auto intro!: successI elim!: successE simp add: bind_def) haftmann@37758: haftmann@37771: lemma success_bind_crelI [success_intros]: haftmann@37771: "crel f h h' x \ success (g x) h' \ success (f \= g) h" haftmann@37771: by (auto simp add: crel_def success_def bind_def) haftmann@37771: haftmann@37771: lemma crel_bindI [crel_intros]: haftmann@37771: assumes "crel f h h' r" "crel (g r) h' h'' r'" haftmann@37771: shows "crel (f \= g) h h'' r'" haftmann@37771: using assms haftmann@37771: apply (auto intro!: crelI elim!: crelE successE) haftmann@37771: apply (subst execute_bind, simp_all) haftmann@37771: done haftmann@37771: haftmann@37771: lemma crel_bindE [crel_elims]: haftmann@37771: assumes "crel (f \= g) h h'' r'" haftmann@37771: obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'" haftmann@37771: using assms by (auto simp add: crel_def bind_def split: option.split_asm) haftmann@37771: haftmann@37771: lemma execute_bind_eq_SomeI: haftmann@37754: assumes "Heap_Monad.execute f h = Some (x, h')" haftmann@37754: and "Heap_Monad.execute (g x) h' = Some (y, h'')" haftmann@37754: shows "Heap_Monad.execute (f \= g) h = Some (y, h'')" haftmann@37756: using assms by (simp add: bind_def) haftmann@37754: haftmann@37709: lemma return_bind [simp]: "return x \= f = f x" haftmann@37787: by (rule Heap_eqI) (simp add: execute_bind execute_simps) haftmann@37709: haftmann@37709: lemma bind_return [simp]: "f \= return = f" haftmann@37787: by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits) haftmann@37709: haftmann@37828: lemma bind_bind [simp]: "(f \= g) \= k = (f :: 'a Heap) \= (\x. g x \= k)" haftmann@37787: by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits) haftmann@37709: haftmann@37709: lemma raise_bind [simp]: "raise e \= f = raise e" haftmann@37787: by (rule Heap_eqI) (simp add: execute_simps) haftmann@37709: haftmann@26170: haftmann@37758: subsection {* Generic combinators *} haftmann@26170: haftmann@37758: subsubsection {* Assertions *} haftmann@26170: haftmann@37709: definition assert :: "('a \ bool) \ 'a \ 'a Heap" where haftmann@37709: "assert P x = (if P x then return x else raise ''assert'')" haftmann@28742: haftmann@37758: lemma execute_assert [execute_simps]: haftmann@37754: "P x \ execute (assert P x) h = Some (x, h)" haftmann@37754: "\ P x \ execute (assert P x) h = None" haftmann@37787: by (simp_all add: assert_def execute_simps) haftmann@37754: haftmann@37758: lemma success_assertI [success_intros]: haftmann@37758: "P x \ success (assert P x) h" haftmann@37758: by (rule successI) (simp add: execute_assert) haftmann@37758: haftmann@37771: lemma crel_assertI [crel_intros]: haftmann@37771: "P x \ h' = h \ r = x \ crel (assert P x) h h' r" haftmann@37771: by (rule crelI) (simp add: execute_assert) haftmann@37771: haftmann@37771: lemma crel_assertE [crel_elims]: haftmann@37771: assumes "crel (assert P x) h h' r" haftmann@37771: obtains "P x" "r = x" "h' = h" haftmann@37771: using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def) haftmann@37771: haftmann@28742: lemma assert_cong [fundef_cong]: haftmann@28742: assumes "P = P'" haftmann@28742: assumes "\x. P' x \ f x = f' x" haftmann@28742: shows "(assert P x >>= f) = (assert P' x >>= f')" haftmann@37754: by (rule Heap_eqI) (insert assms, simp add: assert_def) haftmann@28742: haftmann@37758: haftmann@37758: subsubsection {* Plain lifting *} haftmann@37758: haftmann@37754: definition lift :: "('a \ 'b) \ 'a \ 'b Heap" where haftmann@37754: "lift f = return o f" haftmann@37709: haftmann@37754: lemma lift_collapse [simp]: haftmann@37754: "lift f x = return (f x)" haftmann@37754: by (simp add: lift_def) haftmann@37709: haftmann@37754: lemma bind_lift: haftmann@37754: "(f \= lift g) = (f \= (\x. return (g x)))" haftmann@37754: by (simp add: lift_def comp_def) haftmann@37709: haftmann@37758: haftmann@37758: subsubsection {* Iteration -- warning: this is rarely useful! *} haftmann@37758: haftmann@37756: primrec fold_map :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" where haftmann@37756: "fold_map f [] = return []" krauss@37792: | "fold_map f (x # xs) = do { haftmann@37709: y \ f x; haftmann@37756: ys \ fold_map f xs; haftmann@37709: return (y # ys) krauss@37792: }" haftmann@37709: haftmann@37756: lemma fold_map_append: haftmann@37756: "fold_map f (xs @ ys) = fold_map f xs \= (\xs. fold_map f ys \= (\ys. return (xs @ ys)))" haftmann@37754: by (induct xs) simp_all haftmann@37754: haftmann@37758: lemma execute_fold_map_unchanged_heap [execute_simps]: haftmann@37754: assumes "\x. x \ set xs \ \y. execute (f x) h = Some (y, h)" haftmann@37756: shows "execute (fold_map f xs) h = haftmann@37754: Some (List.map (\x. fst (the (execute (f x) h))) xs, h)" haftmann@37754: using assms proof (induct xs) haftmann@37787: case Nil show ?case by (simp add: execute_simps) haftmann@37754: next haftmann@37754: case (Cons x xs) haftmann@37754: from Cons.prems obtain y haftmann@37754: where y: "execute (f x) h = Some (y, h)" by auto haftmann@37756: moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h = haftmann@37754: Some (map (\x. fst (the (execute (f x) h))) xs, h)" by auto haftmann@37787: ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps) haftmann@37754: qed haftmann@37754: haftmann@26182: subsection {* Code generator setup *} haftmann@26182: haftmann@26182: subsubsection {* Logical intermediate layer *} haftmann@26182: haftmann@37709: primrec raise' :: "String.literal \ 'a Heap" where haftmann@37709: [code del, code_post]: "raise' (STR s) = raise s" haftmann@26182: haftmann@37709: lemma raise_raise' [code_inline]: haftmann@37709: "raise s = raise' (STR s)" haftmann@37709: by simp haftmann@26182: haftmann@37709: code_datatype raise' -- {* avoid @{const "Heap"} formally *} haftmann@26182: haftmann@26182: haftmann@27707: subsubsection {* SML and OCaml *} haftmann@26182: haftmann@26752: code_type Heap (SML "unit/ ->/ _") haftmann@37828: code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") haftmann@27707: code_const return (SML "!(fn/ ()/ =>/ _)") haftmann@37709: code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)") haftmann@26182: haftmann@37754: code_type Heap (OCaml "unit/ ->/ _") haftmann@37828: code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())") haftmann@27707: code_const return (OCaml "!(fun/ ()/ ->/ _)") haftmann@37828: code_const Heap_Monad.raise' (OCaml "failwith") haftmann@27707: haftmann@37838: haftmann@37838: subsubsection {* Haskell *} haftmann@37838: haftmann@37838: text {* Adaption layer *} haftmann@37838: haftmann@37838: code_include Haskell "Heap" haftmann@37838: {*import qualified Control.Monad; haftmann@37838: import qualified Control.Monad.ST; haftmann@37838: import qualified Data.STRef; haftmann@37838: import qualified Data.Array.ST; haftmann@37838: haftmann@37838: type RealWorld = Control.Monad.ST.RealWorld; haftmann@37838: type ST s a = Control.Monad.ST.ST s a; haftmann@37838: type STRef s a = Data.STRef.STRef s a; haftmann@37838: type STArray s a = Data.Array.ST.STArray s Int a; haftmann@37838: haftmann@37838: newSTRef = Data.STRef.newSTRef; haftmann@37838: readSTRef = Data.STRef.readSTRef; haftmann@37838: writeSTRef = Data.STRef.writeSTRef; haftmann@37838: haftmann@37838: newArray :: Int -> a -> ST s (STArray s a); haftmann@37838: newArray k = Data.Array.ST.newArray (0, k); haftmann@37838: haftmann@37838: newListArray :: [a] -> ST s (STArray s a); haftmann@37838: newListArray xs = Data.Array.ST.newListArray (0, length xs) xs; haftmann@37838: haftmann@37838: newFunArray :: Int -> (Int -> a) -> ST s (STArray s a); haftmann@37838: newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]); haftmann@37838: haftmann@37838: lengthArray :: STArray s a -> ST s Int; haftmann@37838: lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a); haftmann@37838: haftmann@37838: readArray :: STArray s a -> Int -> ST s a; haftmann@37838: readArray = Data.Array.ST.readArray; haftmann@37838: haftmann@37838: writeArray :: STArray s a -> Int -> a -> ST s (); haftmann@37838: writeArray = Data.Array.ST.writeArray;*} haftmann@37838: haftmann@37838: code_reserved Haskell Heap haftmann@37838: haftmann@37838: text {* Monad *} haftmann@37838: haftmann@37838: code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") haftmann@37838: code_monad bind Haskell haftmann@37838: code_const return (Haskell "return") haftmann@37838: code_const Heap_Monad.raise' (Haskell "error") haftmann@37838: haftmann@37838: haftmann@37838: subsubsection {* Scala *} haftmann@37838: haftmann@37842: code_include Scala "Heap" haftmann@37842: {*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) () haftmann@37842: haftmann@37842: class Ref[A](x: A) { haftmann@37842: var value = x haftmann@37842: } haftmann@37842: haftmann@37842: object Ref { haftmann@37842: def apply[A](x: A): Ref[A] = new Ref[A](x) haftmann@37842: } haftmann@37842: haftmann@37842: def lookup[A](r: Ref[A]): A = r.value haftmann@37842: haftmann@37842: def update[A](r: Ref[A], x: A): Unit = { r.value = x }*} haftmann@37838: haftmann@37838: code_reserved Scala Heap haftmann@37838: haftmann@37838: code_type Heap (Scala "Unit/ =>/ _") haftmann@37842: code_const bind (Scala "!Heap.bind((_), (_))") haftmann@37842: code_const return (Scala "('_: Unit)/ =>/ _") haftmann@37845: code_const Heap_Monad.raise' (Scala "!error((_))") haftmann@37838: haftmann@37838: haftmann@37838: subsubsection {* Target variants with less units *} haftmann@37838: haftmann@31871: setup {* haftmann@31871: haftmann@31871: let haftmann@27707: haftmann@31871: open Code_Thingol; haftmann@31871: haftmann@31871: fun imp_program naming = haftmann@27707: haftmann@31871: let haftmann@31871: fun is_const c = case lookup_const naming c haftmann@31871: of SOME c' => (fn c'' => c' = c'') haftmann@31871: | NONE => K false; haftmann@37756: val is_bind = is_const @{const_name bind}; haftmann@31871: val is_return = is_const @{const_name return}; haftmann@31893: val dummy_name = ""; haftmann@31871: val dummy_type = ITyVar dummy_name; haftmann@31893: val dummy_case_term = IVar NONE; haftmann@31871: (*assumption: dummy values are not relevant for serialization*) haftmann@31871: val unitt = case lookup_const naming @{const_name Unity} haftmann@31871: of SOME unit' => IConst (unit', (([], []), [])) haftmann@31871: | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants."); haftmann@31871: fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t) haftmann@31871: | dest_abs (t, ty) = haftmann@31871: let haftmann@31871: val vs = fold_varnames cons t []; haftmann@31871: val v = Name.variant vs "x"; haftmann@31871: val ty' = (hd o fst o unfold_fun) ty; haftmann@31893: in ((SOME v, ty'), t `$ IVar (SOME v)) end; haftmann@31871: fun force (t as IConst (c, _) `$ t') = if is_return c haftmann@31871: then t' else t `$ unitt haftmann@31871: | force t = t `$ unitt; haftmann@31871: fun tr_bind' [(t1, _), (t2, ty2)] = haftmann@31871: let haftmann@31871: val ((v, ty), t) = dest_abs (t2, ty2); haftmann@31871: in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end haftmann@31871: and tr_bind'' t = case unfold_app t haftmann@37754: of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c haftmann@31871: then tr_bind' [(x1, ty1), (x2, ty2)] haftmann@31871: else force t haftmann@31871: | _ => force t; haftmann@31893: fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type), haftmann@31871: [(unitt, tr_bind' ts)]), dummy_case_term) haftmann@37754: and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) haftmann@31871: of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] haftmann@31871: | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 haftmann@31871: | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) haftmann@31871: else IConst const `$$ map imp_monad_bind ts haftmann@31871: and imp_monad_bind (IConst const) = imp_monad_bind' const [] haftmann@31871: | imp_monad_bind (t as IVar _) = t haftmann@31871: | imp_monad_bind (t as _ `$ _) = (case unfold_app t haftmann@31871: of (IConst const, ts) => imp_monad_bind' const ts haftmann@31871: | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) haftmann@31871: | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t haftmann@31871: | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase haftmann@31871: (((imp_monad_bind t, ty), haftmann@31871: (map o pairself) imp_monad_bind pats), haftmann@31871: imp_monad_bind t0); haftmann@28663: haftmann@31871: in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; haftmann@27707: haftmann@27707: in haftmann@27707: haftmann@31871: Code_Target.extend_target ("SML_imp", ("SML", imp_program)) haftmann@31871: #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) haftmann@37838: #> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program)) haftmann@27707: haftmann@27707: end haftmann@31871: haftmann@27707: *} haftmann@27707: haftmann@26182: haftmann@37758: hide_const (open) Heap heap guard raise' fold_map haftmann@37724: haftmann@26170: end