Basis.mkMonad

9 files changed, 126 insertions, 36 deletions

diff --git a/doc/manual.tex b/doc/manual.tex
index a1fe4a1d..052249ce 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1382,7 +1382,11 @@ $$\begin{array}{l}
   \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\
   \hspace{.1in} \to \mt{monad} \; \mt{m} \\
   \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\
-  \hspace{.1in} \to \mt{m} \; \mt{t2}
+  \hspace{.1in} \to \mt{m} \; \mt{t2} \\
+  \mt{val} \; \mt{mkMonad} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \\
+  \hspace{.1in} \to \{\mt{Return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{m} \; \mt{t}, \\
+  \hspace{.3in} \mt{Bind} : \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \to \mt{m} \; \mt{t2}\} \\
+  \hspace{.1in} \to \mt{monad} \; \mt{m}
 \end{array}$$
 
 \subsection{Transactions}
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index ece4bfef..494eaa4b 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -126,6 +126,11 @@ val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
            -> m t1 -> (t1 -> m t2)
            -> m t2
 
+val mkMonad : m ::: (Type -> Type)
+              -> {Return : t ::: Type -> t -> m t,
+                  Bind : t1 ::: Type -> t2 ::: Type -> m t1 -> (t1 -> m t2) -> m t2}
+              -> monad m
+
 con transaction :: Type -> Type
 val transaction_monad : monad transaction
 
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index 0aa07a2d..5c89fc9d 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -1,5 +1,11 @@
 datatype t = datatype Basis.option
 
+val monad = mkMonad {Return = @@Some,
+                     Bind = fn [a] [b] (m1 : t a) (m2 : a -> t b) =>
+                               case m1 of
+                                   None => None
+                                 | Some v => m2 v}
+
 fun eq [a] (_ : eq a) =
     mkEq (fn x y =>
              case (x, y) of
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index 62687963..ba43613f 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,5 +1,7 @@
 datatype t = datatype Basis.option
 
+val monad : monad t
+
 val eq : a ::: Type -> eq a -> eq (t a)
 val ord : a ::: Type -> ord a -> ord (t a)
 
diff --git a/src/core_print.sml b/src/core_print.sml
index ca8066b3..8e46db04 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -281,7 +281,7 @@ fun p_exp' par env (e, _) =
       | EApp (e1, e2) => parenIf par (box [p_exp' true env e1,
                                            space,
                                            p_exp' true env e2])
-      | EAbs (x, t, _, e) => parenIf par (box [string "fn",
+      | EAbs (x, t, _, e) => parenIf par (box [string "(fn",
                                                space,
                                                string x,
                                                space,
@@ -291,7 +291,8 @@ fun p_exp' par env (e, _) =
                                                space,
                                                string "=>",
                                                space,
-                                               p_exp (E.pushERel env x t) e])
+                                               p_exp (E.pushERel env x t) e,
+                                               string ")"])
       | ECApp (e, c) => parenIf par (box [p_exp env e,
                                           space,
                                           string "[",
diff --git a/src/monoize.sml b/src/monoize.sml
index 337e198c..7849e1cd 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -1315,20 +1315,17 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                  fm)
             end
 
-          | L.EFfi ("Basis", "transaction_monad") => ((L'.ERecord [], loc), fm)
-          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "return"), _), (L.CFfi ("Basis", "transaction"), _)), _), t) =>
+          | L.ECApp ((L.EFfi ("Basis", "transaction_return"), _), t) =>
             let
                 val t = monoType env t
             in
-                ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (t, (L'.TFun ((L'.TRecord [], loc), t), loc)), loc),
-                           (L'.EAbs ("x", t,
+                ((L'.EAbs ("x", t,
                                      (L'.TFun ((L'.TRecord [], loc), t), loc),
                                      (L'.EAbs ("_", (L'.TRecord [], loc), t,
-                                               (L'.ERel 1, loc)), loc)), loc)), loc),
+                                               (L'.ERel 1, loc)), loc)), loc),
                  fm)
             end
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), (L.CFfi ("Basis", "transaction"), _)), _),
-                               t1), _), t2) =>
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "transaction_bind"), _), t1), _), t2) =>
             let
                 val t1 = monoType env t1
                 val t2 = monoType env t2
@@ -1336,17 +1333,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 val mt1 = (L'.TFun (un, t1), loc)
                 val mt2 = (L'.TFun (un, t2), loc)
             in
-                ((L'.EAbs ("_", un,
-                           (L'.TFun (mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc)), loc),
-                           (L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc),
-                                     (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc),
-                                               (L'.EAbs ("_", un, un,
-                                                         (L'.ELet ("r", t1, (L'.EApp ((L'.ERel 2, loc),
-                                                                                      (L'.ERecord [], loc)), loc),
-                                                                   (L'.EApp (
-                                                                    (L'.EApp ((L'.ERel 2, loc), (L'.ERel 0, loc)), loc),
-                                                                    (L'.ERecord [], loc)),
-                                                                    loc)), loc)), loc)), loc)), loc)), loc),
+                ((L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc),
+                           (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc),
+                                     (L'.EAbs ("_", un, un,
+                                               (L'.ELet ("r", t1, (L'.EApp ((L'.ERel 2, loc),
+                                                                            (L'.ERecord [], loc)), loc),
+                                                         (L'.EApp (
+                                                          (L'.EApp ((L'.ERel 2, loc), (L'.ERel 0, loc)), loc),
+                                                          (L'.ERecord [], loc)),
+                                                          loc)), loc)), loc)), loc)), loc),
                  fm)
             end
 
@@ -1427,18 +1422,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 ((L'.ESpawn e, loc), fm)
             end
 
-          | L.EFfi ("Basis", "signal_monad") => ((L'.ERecord [], loc), fm)
-          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "return"), _), (L.CFfi ("Basis", "signal"), _)), _), t) =>
+          | L.ECApp ((L.EFfi ("Basis", "signal_return"), _), t) =>
             let
                 val t = monoType env t
             in
-                ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (t, (L'.TSignal t, loc)), loc),
-                           (L'.EAbs ("x", t, (L'.TSignal t, loc),
-                                     (L'.ESignalReturn (L'.ERel 0, loc), loc)), loc)), loc),
+                ((L'.EAbs ("x", t, (L'.TSignal t, loc),
+                           (L'.ESignalReturn (L'.ERel 0, loc), loc)), loc),
                  fm)
             end
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), (L.CFfi ("Basis", "signal"), _)), _),
-                               t1), _), t2) =>
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "signal_bind"), _), t1), _), t2) =>
             let
                 val t1 = monoType env t1
                 val t2 = monoType env t2
@@ -1446,11 +1438,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 val mt1 = (L'.TSignal t1, loc)
                 val mt2 = (L'.TSignal t2, loc)
             in
-                ((L'.EAbs ("_", un, (L'.TFun (mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc)), loc),
-                           (L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc),
-                                     (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), mt2,
-                                               (L'.ESignalBind ((L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)),
-                  loc),
+                ((L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc),
+                           (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), mt2,
+                                     (L'.ESignalBind ((L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
                  fm)
             end
           | L.ECApp ((L.EFfi ("Basis", "signal"), _), t) =>
diff --git a/src/reduce.sml b/src/reduce.sml
index b2462695..9371e9bd 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -36,6 +36,12 @@ structure IM = IntBinaryMap
 
 structure E = CoreEnv
 
+fun multiLiftConInCon n c =
+    if n = 0 then
+        c
+    else
+        multiLiftConInCon (n - 1) (E.liftConInCon 0 c)
+
 fun multiLiftExpInExp n e =
     if n = 0 then
         e
@@ -204,6 +210,28 @@ fun match (env, p : pat, e : exp) =
         match (env, p, e)
     end
 
+fun returnType m loc =
+    (TCFun ("a", (KType, loc),
+            (TFun ((CRel 0, loc),
+                   (CApp (multiLiftConInCon 1 m, (CRel 0, loc)), loc)), loc)), loc)
+
+fun bindType m loc =
+    (TCFun ("a", (KType, loc),
+            (TCFun ("b", (KType, loc),
+                    (TFun ((CApp (multiLiftConInCon 2 m, (CRel 1, loc)), loc),
+                           (TFun ((TFun ((CRel 1, loc),
+                                         (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)),
+                                   loc),
+                                  (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)), loc)),
+                     loc)), loc)), loc)
+
+fun monadRecord m loc =
+    (TRecord (CRecord ((KType, loc),
+                       [((CName "Return", loc),
+                         returnType m loc),
+                        ((CName "Bind", loc),
+                         bindType m loc)]), loc), loc)
+
 fun kindConAndExp (namedC, namedE) =
     let
         fun kind env (all as (k, loc)) =
@@ -273,10 +301,14 @@ fun kindConAndExp (namedC, namedE) =
                     (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
                     find (n, env, 0, 0, 0)
                 end
+
               | CNamed n =>
                 (case IM.find (namedC, n) of
                      NONE => all
                    | SOME c => c)
+
+              | CFfi ("Basis", "monad") => (CAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), monadRecord (CRel 0, loc) loc), loc)
+
               | CFfi _ => all
               | CApp (c1, c2) =>
                 let
@@ -415,6 +447,51 @@ fun kindConAndExp (namedC, namedE) =
                                | SOME e => e)
                           | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
                                                             map (con env) cs, Option.map (exp env) eo), loc)
+
+                          | EFfi ("Basis", "return") =>
+                            (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+                                    (ECAbs ("a", (KType, loc),
+                                            (EAbs ("m", monadRecord (CRel 1, loc) loc, returnType (CRel 1, loc) loc,
+                                                   (ECApp ((EField ((ERel 0, loc), (CName "Return", loc),
+                                                                    {field = returnType (CRel 1, loc) loc,
+                                                                     rest = (CRecord ((KType, loc),
+                                                                                      [((CName "Bind", loc), bindType (CRel 1, loc) loc)]),
+                                                                             loc)}), loc), (CRel 0, loc)), loc)), loc)), loc)), loc)
+
+                          | EFfi ("Basis", "bind") =>
+                            (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+                                    (ECAbs ("a", (KType, loc),
+                                            (ECAbs ("b", (KType, loc),
+                                                    (EAbs ("m", monadRecord (CRel 2, loc) loc, bindType (CRel 2, loc) loc,
+                                                           (ECApp ((ECApp ((EField ((ERel 0, loc), (CName "Bind", loc),
+                                                                                    {field = bindType (CRel 2, loc) loc,
+                                                                                     rest = (CRecord ((KType, loc),
+                                                                                                      [((CName "Return", loc),
+                                                                                                        returnType (CRel 2, loc) loc)]),
+                                                                                             loc)}), loc), (CRel 1, loc)), loc),
+                                                                  (CRel 0, loc)), loc)), loc)), loc)), loc)), loc)
+
+                          | EFfi ("Basis", "mkMonad") =>
+                            (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+                                    (EAbs ("m", monadRecord (CRel 0, loc) loc, monadRecord (CRel 0, loc) loc,
+                                           (ERel 0, loc)), loc)), loc)
+
+                          | EFfi ("Basis", "transaction_monad") =>
+                            (ERecord [((CName "Return", loc),
+                                       (EFfi ("Basis", "transaction_return"), loc),
+                                       returnType (CFfi ("Basis", "transaction"), loc) loc),
+                                      ((CName "Bind", loc),
+                                       (EFfi ("Basis", "transaction_bind"), loc),
+                                       bindType (CFfi ("Basis", "transaction"), loc) loc)], loc)
+
+                          | EFfi ("Basis", "signal_monad") =>
+                            (ERecord [((CName "Return", loc),
+                                       (EFfi ("Basis", "signal_return"), loc),
+                                       returnType (CFfi ("Basis", "signal"), loc) loc),
+                                      ((CName "Bind", loc),
+                                       (EFfi ("Basis", "signal_bind"), loc),
+                                       bindType (CFfi ("Basis", "signal"), loc) loc)], loc)
+
                           | EFfi _ => all
                           | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
 
diff --git a/tests/optionM.ur b/tests/optionM.ur
new file mode 100644
index 00000000..4af6a46c
--- /dev/null
+++ b/tests/optionM.ur
@@ -0,0 +1,3 @@
+fun main () : transaction page = return <xml>{[x <- Some 1;
+                                               y <- Some 2;
+                                               return (x + y)]}</xml>
diff --git a/tests/optionM.urp b/tests/optionM.urp
new file mode 100644
index 00000000..b043dfe0
--- /dev/null
+++ b/tests/optionM.urp
@@ -0,0 +1,2 @@
+$/option
+optionM