# HG changeset patch # User Adam Chlipala # Date 1229700478 18000 # Node ID 803b2f3bb86b15a8c133fe7a5c2953a705064ff9 # Parent 44958d74c43f2d66e08651cc1abe2c14a08d3676 Monad type class seems to be working diff -r 44958d74c43f -r 803b2f3bb86b lib/basis.urs --- a/lib/basis.urs Fri Dec 19 10:03:31 2008 -0500 +++ b/lib/basis.urs Fri Dec 19 10:27:58 2008 -0500 @@ -69,15 +69,22 @@ val read_time : read time -(** * Transactions *) +(** * Monads *) + +class monad :: Type -> Type +val return : m ::: (Type -> Type) -> t ::: Type + -> monad m + -> t -> m t +val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type + -> monad m + -> m t1 -> (t1 -> m t2) + -> m t2 + +(** ** Transactions *) con transaction :: Type -> Type +val transaction_monad : monad transaction -val return : t ::: Type - -> t -> transaction t -val bind : t1 ::: Type -> t2 ::: Type - -> transaction t1 -> (t1 -> transaction t2) - -> transaction t2 (** HTTP operations *) diff -r 44958d74c43f -r 803b2f3bb86b lib/top.ur --- a/lib/top.ur Fri Dec 19 10:03:31 2008 -0500 +++ b/lib/top.ur Fri Dec 19 10:27:58 2008 -0500 @@ -30,8 +30,8 @@ fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) -fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = - cdata (@show sh v) +fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = + cdata (show v) fun foldUR (tf :: Type) (tr :: {Unit} -> Type) (f : nm :: Name -> rest :: {Unit} @@ -233,9 +233,9 @@ (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) - (t ::: Type) (inj : sql_injectable (option t)) + (t ::: Type) (_ : sql_injectable (option t)) (e1 : sql_exp tables agg exps (option t)) (e2 : option t) = case e2 of None => (SQL {e1} IS NULL) - | Some _ => sql_binary sql_eq e1 (@sql_inject inj e2) + | Some _ => sql_binary sql_eq e1 (sql_inject e2) diff -r 44958d74c43f -r 803b2f3bb86b src/corify.sml --- a/src/corify.sml Fri Dec 19 10:03:31 2008 -0500 +++ b/src/corify.sml Fri Dec 19 10:27:58 2008 -0500 @@ -926,8 +926,10 @@ val e = (L.EModProj (m, ms, s), loc) val ef = (L.EModProj (basis, [], "bind"), loc) + val ef = (L.ECApp (ef, (L.CModProj (basis, [], "transaction"), loc)), loc) val ef = (L.ECApp (ef, ran'), loc) val ef = (L.ECApp (ef, ran), loc) + val ef = (L.EApp (ef, (L.EModProj (basis, [], "transaction_monad"), loc)), loc) val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc) val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc), diff -r 44958d74c43f -r 803b2f3bb86b src/elaborate.sml --- a/src/elaborate.sml Fri Dec 19 10:03:31 2008 -0500 +++ b/src/elaborate.sml Fri Dec 19 10:27:58 2008 -0500 @@ -3548,7 +3548,15 @@ ("c1", p_con env c1), ("c2", p_con env c2)]; raise Fail "Unresolved constraint in top.ur")) - | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs + | TypeClass (env, c, r, loc) => + let + val c = normClassKey env c + in + case E.resolveClass env c of + SOME e => r := SOME e + | NONE => expError env (Unresolvable (loc, c)) + end) gs + val () = subSgn (env', D.empty) topSgn' topSgn val (env', top_n) = E.pushStrNamed env' "Top" topSgn diff -r 44958d74c43f -r 803b2f3bb86b src/monoize.sml --- a/src/monoize.sml Fri Dec 19 10:03:31 2008 -0500 +++ b/src/monoize.sml Fri Dec 19 10:27:58 2008 -0500 @@ -934,7 +934,8 @@ fm) end - | L.ECApp ((L.EFfi ("Basis", "return"), _), t) => + | L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "return"), _), _), _), t), _), + (L.EFfi ("Basis", "transaction_monad"), _)) => let val t = monoType env t in @@ -943,7 +944,8 @@ (L'.EAbs ("_", (L'.TRecord [], loc), t, (L'.ERel 1, loc)), loc)), loc), fm) end - | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), t1), _), t2) => + | L.EApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _), + (L.EFfi ("Basis", "transaction_monad"), _)) => let val t1 = monoType env t1 val t2 = monoType env t2