1.1 --- a/src/HOL/Library/Heap_Monad.thy	Wed Jul 30 07:33:56 2008 +0200
     1.2 +++ b/src/HOL/Library/Heap_Monad.thy	Wed Jul 30 07:33:57 2008 +0200
     1.3 @@ -288,26 +288,84 @@
     1.4  hide (open) const Fail raise_exc
     1.5  
     1.6  
     1.7 -subsubsection {* SML *}
     1.8 +subsubsection {* SML and OCaml *}
     1.9  
    1.10  code_type Heap (SML "unit/ ->/ _")
    1.11  code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
    1.12 -code_monad run "op \<guillemotright>=" return "()" SML
    1.13 +code_const "op \<guillemotright>=" (SML "!(fn/ f/ =>/ fn/ g/ =>/ fn/ ()/ =>/ g/ (f/ ())/ ())")
    1.14  code_const run (SML "_")
    1.15 -code_const return (SML "(fn/ ()/ =>/ _)")
    1.16 +code_const return (SML "!(fn/ ()/ =>/ _)")
    1.17  code_const "Heap_Monad.Fail" (SML "Fail")
    1.18 -code_const "Heap_Monad.raise_exc" (SML "(fn/ ()/ =>/ raise/ _)")
    1.19 -
    1.20 -
    1.21 -subsubsection {* OCaml *}
    1.22 +code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
    1.23  
    1.24  code_type Heap (OCaml "_")
    1.25  code_const Heap (OCaml "failwith/ \"bare Heap\"")
    1.26 -code_monad run "op \<guillemotright>=" return "()" OCaml
    1.27 +code_const "op \<guillemotright>=" (OCaml "!(fun/ f/ g/ ()/ ->/ g/ (f/ ())/ ())")
    1.28  code_const run (OCaml "_")
    1.29 -code_const return (OCaml "(fun/ ()/ ->/ _)")
    1.30 +code_const return (OCaml "!(fun/ ()/ ->/ _)")
    1.31  code_const "Heap_Monad.Fail" (OCaml "Failure")
    1.32 -code_const "Heap_Monad.raise_exc" (OCaml "(fun/ ()/ ->/ raise/ _)")
    1.33 +code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
    1.34 +
    1.35 +ML {*
    1.36 +local
    1.37 +
    1.38 +open CodeThingol;
    1.39 +
    1.40 +val bind' = CodeName.const @{theory} @{const_name bindM};
    1.41 +val return' = CodeName.const @{theory} @{const_name return};
    1.42 +val unit' = CodeName.const @{theory} @{const_name Unity};
    1.43 +
    1.44 +fun imp_monad_bind'' ts =
    1.45 +  let
    1.46 +    val dummy_name = "";
    1.47 +    val dummy_type = ITyVar dummy_name;
    1.48 +    val dummy_case_term = IVar dummy_name;
    1.49 +    (*assumption: dummy values are not relevant for serialization*)
    1.50 +    val unitt = IConst (unit', ([], []));
    1.51 +    fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    1.52 +      | dest_abs (t, ty) =
    1.53 +          let
    1.54 +            val vs = CodeThingol.fold_varnames cons t [];
    1.55 +            val v = Name.variant vs "x";
    1.56 +            val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
    1.57 +          in ((v, ty'), t `$ IVar v) end;
    1.58 +    fun force (t as IConst (c, _) `$ t') = if c = return'
    1.59 +          then t' else t `$ unitt
    1.60 +      | force t = t `$ unitt;
    1.61 +    fun tr_bind' [(t1, _), (t2, ty2)] =
    1.62 +      let
    1.63 +        val ((v, ty), t) = dest_abs (t2, ty2);
    1.64 +      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    1.65 +    and tr_bind'' t = case CodeThingol.unfold_app t
    1.66 +         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    1.67 +              then tr_bind' [(x1, ty1), (x2, ty2)]
    1.68 +              else force t
    1.69 +          | _ => force t;
    1.70 +  in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
    1.71 +    [(unitt, tr_bind' ts)]), dummy_case_term) end
    1.72 +and imp_monad_bind' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    1.73 +   of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    1.74 +    | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.75 +    | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    1.76 +  else IConst const `$$ map imp_monad_bind ts
    1.77 +and imp_monad_bind (IConst const) = imp_monad_bind' const []
    1.78 +  | imp_monad_bind (t as IVar _) = t
    1.79 +  | imp_monad_bind (t as _ `$ _) = (case unfold_app t
    1.80 +     of (IConst const, ts) => imp_monad_bind' const ts
    1.81 +      | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
    1.82 +  | imp_monad_bind (v_ty `|-> t) = v_ty `|-> imp_monad_bind t
    1.83 +  | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
    1.84 +      (((imp_monad_bind t, ty), (map o pairself) imp_monad_bind pats), imp_monad_bind t0);
    1.85 +
    1.86 +in
    1.87 +
    1.88 +val imp_program = (Graph.map_nodes o map_terms_stmt) imp_monad_bind;
    1.89 +
    1.90 +end
    1.91 +*}
    1.92 +
    1.93 +setup {* CodeTarget.extend_target ("SML_imp", ("SML", imp_program)) *}
    1.94 +setup {* CodeTarget.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
    1.95  
    1.96  code_reserved OCaml Failure raise
    1.97  

     2.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Wed Jul 30 07:33:56 2008 +0200
     2.2 +++ b/src/HOL/ex/ImperativeQuicksort.thy	Wed Jul 30 07:33:57 2008 +0200
     2.3 @@ -630,7 +630,9 @@
     2.4  
     2.5  ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
     2.6  
     2.7 +export_code qsort in SML_imp module_name Arr
     2.8  export_code qsort in OCaml module_name Arr file -
     2.9 +export_code qsort in OCaml_imp module_name Arr file -
    2.10  export_code qsort in Haskell module_name Arr file -
    2.11  
    2.12  end
    2.13 \ No newline at end of file