# HG changeset patch # User Adam Chlipala # Date 1313781781 14400 # Node ID a99b743a30873cd732e8520dc45c6281b94a6127 # Parent 6f046b4bad24049244941c96e4667ee37c718b05 Basis.mkMonad diff -r 6f046b4bad24 -r a99b743a3087 doc/manual.tex --- a/doc/manual.tex Fri Aug 19 14:20:24 2011 -0400 +++ b/doc/manual.tex Fri Aug 19 15:23:01 2011 -0400 @@ -1382,7 +1382,11 @@ \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 -r 6f046b4bad24 -r a99b743a3087 lib/ur/basis.urs --- a/lib/ur/basis.urs Fri Aug 19 14:20:24 2011 -0400 +++ b/lib/ur/basis.urs Fri Aug 19 15:23:01 2011 -0400 @@ -126,6 +126,11 @@ -> 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 -r 6f046b4bad24 -r a99b743a3087 lib/ur/option.ur --- a/lib/ur/option.ur Fri Aug 19 14:20:24 2011 -0400 +++ b/lib/ur/option.ur Fri Aug 19 15:23:01 2011 -0400 @@ -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 -r 6f046b4bad24 -r a99b743a3087 lib/ur/option.urs --- a/lib/ur/option.urs Fri Aug 19 14:20:24 2011 -0400 +++ b/lib/ur/option.urs Fri Aug 19 15:23:01 2011 -0400 @@ -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 -r 6f046b4bad24 -r a99b743a3087 src/core_print.sml --- a/src/core_print.sml Fri Aug 19 14:20:24 2011 -0400 +++ b/src/core_print.sml Fri Aug 19 15:23:01 2011 -0400 @@ -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 @@ | 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 @@ 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 -r 6f046b4bad24 -r a99b743a3087 src/monoize.sml --- a/src/monoize.sml Fri Aug 19 14:20:24 2011 -0400 +++ b/src/monoize.sml Fri Aug 19 15:23:01 2011 -0400 @@ -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 @@ 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 @@ 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 @@ ((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 @@ 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 -r 6f046b4bad24 -r a99b743a3087 src/reduce.sml --- a/src/reduce.sml Fri Aug 19 14:20:24 2011 -0400 +++ b/src/reduce.sml Fri Aug 19 15:23:01 2011 -0400 @@ -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 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 @@ 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 @@ (*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 @@ | 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 -r 6f046b4bad24 -r a99b743a3087 tests/optionM.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/optionM.ur Fri Aug 19 15:23:01 2011 -0400 @@ -0,0 +1,3 @@ +fun main () : transaction page = return {[x <- Some 1; + y <- Some 2; + return (x + y)]} diff -r 6f046b4bad24 -r a99b743a3087 tests/optionM.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/optionM.urp Fri Aug 19 15:23:01 2011 -0400 @@ -0,0 +1,2 @@ +$/option +optionM