# HG changeset patch # User haftmann # Date 1246366437 -7200 # Node ID cc14868409143178dd49347614224120654069e6 # Parent 5274d3d0a6f2b59a351a9898424b0276668f13be streamlined code diff -r 5274d3d0a6f2 -r cc1486840914 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 14:53:56 2009 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 14:53:57 2009 +0200 @@ -306,67 +306,75 @@ code_const "Heap_Monad.Fail" (OCaml "Failure") code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)") -setup {* let - open Code_Thingol; +setup {* + +let - fun lookup naming = the o Code_Thingol.lookup_const naming; +open Code_Thingol; + +fun imp_program naming = - fun imp_monad_bind'' bind' return' unit' ts = - let - val dummy_name = ""; - val dummy_type = ITyVar dummy_name; - val dummy_case_term = IVar dummy_name; - (*assumption: dummy values are not relevant for serialization*) - val unitt = IConst (unit', (([], []), [])); - fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t) - | dest_abs (t, ty) = - let - val vs = Code_Thingol.fold_varnames cons t []; - val v = Name.variant vs "x"; - val ty' = (hd o fst o Code_Thingol.unfold_fun) ty; - in ((v, ty'), t `$ IVar v) end; - fun force (t as IConst (c, _) `$ t') = if c = return' - then t' else t `$ unitt - | force t = t `$ unitt; - fun tr_bind' [(t1, _), (t2, ty2)] = - let - val ((v, ty), t) = dest_abs (t2, ty2); - in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end - and tr_bind'' t = case Code_Thingol.unfold_app t - of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind' - then tr_bind' [(x1, ty1), (x2, ty2)] - else force t - | _ => force t; - in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type), - [(unitt, tr_bind' ts)]), dummy_case_term) end - and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys) - of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] - | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3 - | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts)) - else IConst const `$$ map (imp_monad_bind bind' return' unit') ts - and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const [] - | imp_monad_bind bind' return' unit' (t as IVar _) = t - | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t - of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts - | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts) - | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t - | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase - (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0); + let + fun is_const c = case lookup_const naming c + of SOME c' => (fn c'' => c' = c'') + | NONE => K false; + val is_bindM = is_const @{const_name bindM}; + val is_return = is_const @{const_name return}; + val dummy_name = "X"; + val dummy_type = ITyVar dummy_name; + val dummy_case_term = IVar ""; + (*assumption: dummy values are not relevant for serialization*) + val unitt = case lookup_const naming @{const_name Unity} + of SOME unit' => IConst (unit', (([], []), [])) + | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants."); + fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t) + | dest_abs (t, ty) = + let + val vs = fold_varnames cons t []; + val v = Name.variant vs "x"; + val ty' = (hd o fst o unfold_fun) ty; + in ((v, ty'), t `$ IVar v) end; + fun force (t as IConst (c, _) `$ t') = if is_return c + then t' else t `$ unitt + | force t = t `$ unitt; + fun tr_bind' [(t1, _), (t2, ty2)] = + let + val ((v, ty), t) = dest_abs (t2, ty2); + in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end + and tr_bind'' t = case unfold_app t + of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c + then tr_bind' [(x1, ty1), (x2, ty2)] + else force t + | _ => force t; + fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type), + [(unitt, tr_bind' ts)]), dummy_case_term) + and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys) + of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] + | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 + | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) + else IConst const `$$ map imp_monad_bind ts + and imp_monad_bind (IConst const) = imp_monad_bind' const [] + | imp_monad_bind (t as IVar _) = t + | imp_monad_bind (t as _ `$ _) = (case unfold_app t + of (IConst const, ts) => imp_monad_bind' const ts + | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) + | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t + | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase + (((imp_monad_bind t, ty), + (map o pairself) imp_monad_bind pats), + imp_monad_bind t0); - fun imp_program naming = (Graph.map_nodes o map_terms_stmt) - (imp_monad_bind (lookup naming @{const_name bindM}) - (lookup naming @{const_name return}) - (lookup naming @{const_name Unity})); + in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; in - Code_Target.extend_target ("SML_imp", ("SML", imp_program)) - #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) +Code_Target.extend_target ("SML_imp", ("SML", imp_program)) +#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) end + *} - code_reserved OCaml Failure raise