From 0e84370511179878aa0ebae8bf43810efac194a5 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 6 Oct 2009 10:15:26 -0400
Subject: Fix a de Bruijn index bug in map fusion

---
 demo/more/orm.urs | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

(limited to 'demo/more/orm.urs')

diff --git a/demo/more/orm.urs b/demo/more/orm.urs
index f284d3ec..429d2380 100644
--- a/demo/more/orm.urs
+++ b/demo/more/orm.urs
@@ -1,23 +1,25 @@
-con link :: Type -> Type
+con link :: (Type * Type) -> Type
+val noParent : t ::: Type -> link (t, unit)
 
-con meta = fn col :: Type => {
-	      Link : link col,
-	      Inj : sql_injectable col
+con meta = fn col_parent :: (Type * Type) => {
+	      Link : link col_parent,
+	      Inj : sql_injectable col_parent.1
 	      }
 
 functor Table(M : sig
-		  con cols :: {Type}
+		  con cols :: {(Type * Type)}
 		  val cols : $(map meta cols)
 		  constraint [Id] ~ cols
 		  val folder : folder cols
 	      end) : sig
     type id
-    val inj : sql_injectable id
-    val id : meta id
+    type row' = $(map fst M.cols)
+    type row = $([Id = id] ++ map fst M.cols)
 
-    type row = $([Id = id] ++ M.cols)
+    val inj : sql_injectable id
+    val id : meta (id, row)
 
-    val create : $M.cols -> transaction row
+    val create : row' -> transaction row
     val delete : row -> transaction unit
     val save : row -> transaction unit
     val lookup : id -> transaction (option row)
@@ -25,9 +27,12 @@ functor Table(M : sig
 
     con col :: Type -> Type
     val idCol : col id
-    val cols : $(map col M.cols)
+    val cols : $(map (fn col_parent :: (Type * Type) =>
+                         {Col : col col_parent.1,
+                          Parent : row -> transaction (option col_parent.2)}) M.cols)
 
     type filter
+    val find : filter -> transaction (option row)
     val search : filter -> transaction (list row)
 
     val eq : t ::: Type -> col t -> t -> filter
-- 
cgit v1.2.3