src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 31871 cc1486840914
parent 31724 9b5a128cdb5c
child 31893 7d8a89390cbf
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 14:53:56 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 14:53:57 2009 +0200
     1.3 @@ -306,67 +306,75 @@
     1.4  code_const "Heap_Monad.Fail" (OCaml "Failure")
     1.5  code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
     1.6  
     1.7 -setup {* let
     1.8 -  open Code_Thingol;
     1.9 +setup {*
    1.10 +
    1.11 +let
    1.12  
    1.13 -  fun lookup naming = the o Code_Thingol.lookup_const naming;
    1.14 +open Code_Thingol;
    1.15 +
    1.16 +fun imp_program naming =
    1.17  
    1.18 -  fun imp_monad_bind'' bind' return' unit' ts =
    1.19 -    let
    1.20 -      val dummy_name = "";
    1.21 -      val dummy_type = ITyVar dummy_name;
    1.22 -      val dummy_case_term = IVar dummy_name;
    1.23 -      (*assumption: dummy values are not relevant for serialization*)
    1.24 -      val unitt = IConst (unit', (([], []), []));
    1.25 -      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.26 -        | dest_abs (t, ty) =
    1.27 -            let
    1.28 -              val vs = Code_Thingol.fold_varnames cons t [];
    1.29 -              val v = Name.variant vs "x";
    1.30 -              val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
    1.31 -            in ((v, ty'), t `$ IVar v) end;
    1.32 -      fun force (t as IConst (c, _) `$ t') = if c = return'
    1.33 -            then t' else t `$ unitt
    1.34 -        | force t = t `$ unitt;
    1.35 -      fun tr_bind' [(t1, _), (t2, ty2)] =
    1.36 -        let
    1.37 -          val ((v, ty), t) = dest_abs (t2, ty2);
    1.38 -        in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    1.39 -      and tr_bind'' t = case Code_Thingol.unfold_app t
    1.40 -           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    1.41 -                then tr_bind' [(x1, ty1), (x2, ty2)]
    1.42 -                else force t
    1.43 -            | _ => force t;
    1.44 -    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
    1.45 -      [(unitt, tr_bind' ts)]), dummy_case_term) end
    1.46 -  and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    1.47 -     of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
    1.48 -      | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
    1.49 -      | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
    1.50 -    else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
    1.51 -  and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
    1.52 -    | imp_monad_bind bind' return' unit' (t as IVar _) = t
    1.53 -    | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
    1.54 -       of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
    1.55 -        | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
    1.56 -    | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
    1.57 -    | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
    1.58 -        (((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);
    1.59 +  let
    1.60 +    fun is_const c = case lookup_const naming c
    1.61 +     of SOME c' => (fn c'' => c' = c'')
    1.62 +      | NONE => K false;
    1.63 +    val is_bindM = is_const @{const_name bindM};
    1.64 +    val is_return = is_const @{const_name return};
    1.65 +    val dummy_name = "X";
    1.66 +    val dummy_type = ITyVar dummy_name;
    1.67 +    val dummy_case_term = IVar "";
    1.68 +    (*assumption: dummy values are not relevant for serialization*)
    1.69 +    val unitt = case lookup_const naming @{const_name Unity}
    1.70 +     of SOME unit' => IConst (unit', (([], []), []))
    1.71 +      | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    1.72 +    fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.73 +      | dest_abs (t, ty) =
    1.74 +          let
    1.75 +            val vs = fold_varnames cons t [];
    1.76 +            val v = Name.variant vs "x";
    1.77 +            val ty' = (hd o fst o unfold_fun) ty;
    1.78 +          in ((v, ty'), t `$ IVar v) end;
    1.79 +    fun force (t as IConst (c, _) `$ t') = if is_return c
    1.80 +          then t' else t `$ unitt
    1.81 +      | force t = t `$ unitt;
    1.82 +    fun tr_bind' [(t1, _), (t2, ty2)] =
    1.83 +      let
    1.84 +        val ((v, ty), t) = dest_abs (t2, ty2);
    1.85 +      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    1.86 +    and tr_bind'' t = case unfold_app t
    1.87 +         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c
    1.88 +              then tr_bind' [(x1, ty1), (x2, ty2)]
    1.89 +              else force t
    1.90 +          | _ => force t;
    1.91 +    fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
    1.92 +      [(unitt, tr_bind' ts)]), dummy_case_term)
    1.93 +    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
    1.94 +       of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    1.95 +        | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.96 +        | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    1.97 +      else IConst const `$$ map imp_monad_bind ts
    1.98 +    and imp_monad_bind (IConst const) = imp_monad_bind' const []
    1.99 +      | imp_monad_bind (t as IVar _) = t
   1.100 +      | imp_monad_bind (t as _ `$ _) = (case unfold_app t
   1.101 +         of (IConst const, ts) => imp_monad_bind' const ts
   1.102 +          | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
   1.103 +      | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
   1.104 +      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
   1.105 +          (((imp_monad_bind t, ty),
   1.106 +            (map o pairself) imp_monad_bind pats),
   1.107 +              imp_monad_bind t0);
   1.108  
   1.109 -  fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
   1.110 -    (imp_monad_bind (lookup naming @{const_name bindM})
   1.111 -      (lookup naming @{const_name return})
   1.112 -      (lookup naming @{const_name Unity}));
   1.113 +  in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
   1.114  
   1.115  in
   1.116  
   1.117 -  Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   1.118 -  #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
   1.119 +Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   1.120 +#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
   1.121  
   1.122  end
   1.123 +
   1.124  *}
   1.125  
   1.126 -
   1.127  code_reserved OCaml Failure raise
   1.128  
   1.129