From 3aac0d79c1ad2da6358cf6619c62a56ddd2ed195 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 19 Dec 2008 10:27:58 -0500 Subject: Monad type class seems to be working --- lib/basis.urs | 19 +++++++++++++------ lib/top.ur | 8 ++++---- src/corify.sml | 2 ++ src/elaborate.sml | 10 +++++++++- src/monoize.sml | 6 ++++-- 5 files changed, 32 insertions(+), 13 deletions(-) diff --git a/lib/basis.urs b/lib/basis.urs index eb2a6d29..25923870 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -69,15 +69,22 @@ val read_bool : read bool 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 --git a/lib/top.ur b/lib/top.ur index fd7676a3..35e8519b 100644 --- a/lib/top.ur +++ b/lib/top.ur @@ -30,8 +30,8 @@ fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf = 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 @@ fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) (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 --git a/src/corify.sml b/src/corify.sml index 8bb1a925..2383ee03 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -926,8 +926,10 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) = 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 --git a/src/elaborate.sml b/src/elaborate.sml index 05e08c81..c18cfb49 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3548,7 +3548,15 @@ fun elabFile basis topStr topSgn env file = ("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 --git a/src/monoize.sml b/src/monoize.sml index 1880c57d..1c4aa81b 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -934,7 +934,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (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 -- cgit v1.2.3