src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 48072 ace701efe203
parent 46029 4a19e3d147c3
child 48073 1b609a7837ef
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -633,8 +633,12 @@
     1.4      (*assumption: dummy values are not relevant for serialization*)
     1.5      val (unitt, unitT) = case lookup_const naming @{const_name Unity}
     1.6       of SOME unit' =>
     1.7 -        let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
     1.8 -        in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
     1.9 +          let
    1.10 +            val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
    1.11 +          in
    1.12 +            (IConst { name = unit', typargs = [], dicts = [], dom = [],
    1.13 +              range = unitT, annotate = false }, unitT)
    1.14 +          end
    1.15        | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    1.16      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.17        | dest_abs (t, ty) =
    1.18 @@ -643,21 +647,21 @@
    1.19              val v = singleton (Name.variant_list vs) "x";
    1.20              val ty' = (hd o fst o unfold_fun) ty;
    1.21            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    1.22 -    fun force (t as IConst (c, _) `$ t') = if is_return c
    1.23 +    fun force (t as IConst { name = c, ... } `$ t') = if is_return c
    1.24            then t' else t `$ unitt
    1.25        | force t = t `$ unitt;
    1.26      fun tr_bind'' [(t1, _), (t2, ty2)] =
    1.27        let
    1.28          val ((v, ty), t) = dest_abs (t2, ty2);
    1.29 -      in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
    1.30 +      in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
    1.31      and tr_bind' t = case unfold_app t
    1.32 -     of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
    1.33 +     of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
    1.34            then tr_bind'' [(x1, ty1), (x2, ty2)]
    1.35            else force t
    1.36        | _ => force t;
    1.37 -    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
    1.38 -      [(unitt, tr_bind'' ts)]), dummy_case_term)
    1.39 -    fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
    1.40 +    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
    1.41 +      ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
    1.42 +    fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
    1.43         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    1.44          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.45          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    1.46 @@ -668,10 +672,9 @@
    1.47           of (IConst const, ts) => imp_monad_bind' const ts
    1.48            | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
    1.49        | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
    1.50 -      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
    1.51 -          (((imp_monad_bind t, ty),
    1.52 -            (map o pairself) imp_monad_bind pats),
    1.53 -              imp_monad_bind t0);
    1.54 +      | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
    1.55 +          ICase { term = imp_monad_bind t, typ = ty,
    1.56 +            clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
    1.57  
    1.58    in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
    1.59  
    1.60 @@ -688,3 +691,4 @@
    1.61  hide_const (open) Heap heap guard raise' fold_map
    1.62  
    1.63  end
    1.64 +