diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/basis.urs | 19 | ||||
| -rw-r--r-- | lib/top.ur | 8 |
2 files changed, 17 insertions, 10 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 *) @@ -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) |