diff demo/more/versioned.urs @ 993:10114d7b7477

SELECT DISTINCT; eta expansion during Cjrization
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 15:39:27 -0400
parents
children 166ea3944b91
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/more/versioned.urs	Tue Oct 06 15:39:27 2009 -0400
@@ -0,0 +1,19 @@
+functor Make(M : sig
+                 con key :: {Type}
+                 con data :: {Type}
+                 constraint key ~ data
+                 constraint [When] ~ (key ++ data)
+
+                 val key : $(map sql_injectable key)
+                 val data : $(map (fn t => {Inj : sql_injectable_prim t,
+                                            Eq : eq t}) data)
+
+                 val keyFolder : folder key
+                 val dataFolder : folder data
+             end) : sig
+    val insert : $(M.key ++ M.data) -> transaction unit
+    val update : $(M.key ++ M.data) -> transaction unit
+
+    val keys : transaction (list $M.key)
+    val current : $M.key -> transaction (option $M.data)
+end