adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
authorbulwahn
Wed Sep 07 13:51:37 2011 +0200 (2011-09-07)
changeset 44794d3fdd0a24e15
parent 44793 fddb09e6f84d
child 44795 238c6c7da908
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 07 13:51:36 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 07 13:51:37 2011 +0200
     1.3 @@ -628,7 +628,9 @@
     1.4      val dummy_case_term = IVar NONE;
     1.5      (*assumption: dummy values are not relevant for serialization*)
     1.6      val (unitt, unitT) = case lookup_const naming @{const_name Unity}
     1.7 -     of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
     1.8 +     of SOME unit' =>
     1.9 +        let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
    1.10 +        in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
    1.11        | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    1.12      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.13        | dest_abs (t, ty) =
    1.14 @@ -645,13 +647,13 @@
    1.15          val ((v, ty), t) = dest_abs (t2, ty2);
    1.16        in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
    1.17      and tr_bind' t = case unfold_app t
    1.18 -     of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
    1.19 +     of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
    1.20            then tr_bind'' [(x1, ty1), (x2, ty2)]
    1.21            else force t
    1.22        | _ => force t;
    1.23      fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
    1.24        [(unitt, tr_bind'' ts)]), dummy_case_term)
    1.25 -    fun imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
    1.26 +    fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
    1.27         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    1.28          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.29          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))