diff lib/basis.lig @ 243:2b9dfaffb008

Transactions and queries, at source level
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 14:48:33 -0400
parents f5732dc1316c
children
line wrap: on
line diff
--- a/lib/basis.lig	Thu Aug 28 14:05:47 2008 -0400
+++ b/lib/basis.lig	Thu Aug 28 14:48:33 2008 -0400
@@ -146,6 +146,26 @@
 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
 
 
+(*** Executing queries *)
+
+con transaction :: Type -> Type
+val return : t ::: Type
+        -> t -> transaction t
+val bind : t1 ::: Type -> t2 ::: Type
+        -> transaction t1 -> (t1 -> transaction t2)
+        -> transaction t2
+
+val query : tables ::: {{Type}} -> exps ::: {Type}
+        -> sql_query tables exps
+        -> state ::: Type
+        -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+                -> $exps
+                -> state
+                -> transaction state)
+        -> state
+        -> transaction state
+
+
 (** XML *)
 
 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type