added eta expansion to imperative monad bind
authorhaftmann
Tue, 06 Feb 2007 11:40:53 +0100
changeset 22248 74ea64617c89
parent 22247 5bad0d429694
child 22249 5460a5e4caa2
added eta expansion to imperative monad bind
src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Feb 06 00:53:15 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Feb 06 11:40:53 2007 +0100
@@ -249,7 +249,15 @@
   let
     fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] =
           pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty _ _ _ _ = error "Bad arguments for imperative monad bind";
+      | pretty pr vars fxy [t1, t2] =
+          let
+            (*this code suffers from the lack of a proper concept for bindings*)
+            val vs = CodegenThingol.fold_varnames cons t2 [];
+            val v = Name.variant vs "x";
+            val vars' = CodegenNames.intro_vars [v] vars;
+            val var = IVar v;
+            val ty = "" `%% []; (*an approximation*)
+          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
   in (2, pretty) end;