summaryrefslogtreecommitdiff
path: root/demo/more/orm.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-06 10:15:26 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-06 10:15:26 -0400
commit80d6d2caaf8994d49c7a411f22993a4bb8eef973 (patch)
treebbb81bd1c2dfd38b74df44ae8c236f5353a7a043 /demo/more/orm.urs
parent51ab6fecd3f6bd527d9cc044bdd33a9f4ad87c4d (diff)
Fix a de Bruijn index bug in map fusion
Diffstat (limited to 'demo/more/orm.urs')
-rw-r--r--demo/more/orm.urs25
1 files changed, 15 insertions, 10 deletions
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