comparison demo/more/orm.urs @ 990:46803e668a89

Fix a de Bruijn index bug in map fusion
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 10:15:26 -0400
parents 0bdc4d538f1c
children b132f8620a66
comparison
equal deleted inserted replaced
989:0bdc4d538f1c 990:46803e668a89
1 con link :: Type -> Type 1 con link :: (Type * Type) -> Type
2 val noParent : t ::: Type -> link (t, unit)
2 3
3 con meta = fn col :: Type => { 4 con meta = fn col_parent :: (Type * Type) => {
4 Link : link col, 5 Link : link col_parent,
5 Inj : sql_injectable col 6 Inj : sql_injectable col_parent.1
6 } 7 }
7 8
8 functor Table(M : sig 9 functor Table(M : sig
9 con cols :: {Type} 10 con cols :: {(Type * Type)}
10 val cols : $(map meta cols) 11 val cols : $(map meta cols)
11 constraint [Id] ~ cols 12 constraint [Id] ~ cols
12 val folder : folder cols 13 val folder : folder cols
13 end) : sig 14 end) : sig
14 type id 15 type id
16 type row' = $(map fst M.cols)
17 type row = $([Id = id] ++ map fst M.cols)
18
15 val inj : sql_injectable id 19 val inj : sql_injectable id
16 val id : meta id 20 val id : meta (id, row)
17 21
18 type row = $([Id = id] ++ M.cols) 22 val create : row' -> transaction row
19
20 val create : $M.cols -> transaction row
21 val delete : row -> transaction unit 23 val delete : row -> transaction unit
22 val save : row -> transaction unit 24 val save : row -> transaction unit
23 val lookup : id -> transaction (option row) 25 val lookup : id -> transaction (option row)
24 val list : transaction (list row) 26 val list : transaction (list row)
25 27
26 con col :: Type -> Type 28 con col :: Type -> Type
27 val idCol : col id 29 val idCol : col id
28 val cols : $(map col M.cols) 30 val cols : $(map (fn col_parent :: (Type * Type) =>
31 {Col : col col_parent.1,
32 Parent : row -> transaction (option col_parent.2)}) M.cols)
29 33
30 type filter 34 type filter
35 val find : filter -> transaction (option row)
31 val search : filter -> transaction (list row) 36 val search : filter -> transaction (list row)
32 37
33 val eq : t ::: Type -> col t -> t -> filter 38 val eq : t ::: Type -> col t -> t -> filter
34 val ne : t ::: Type -> col t -> t -> filter 39 val ne : t ::: Type -> col t -> t -> filter
35 val lt : t ::: Type -> col t -> t -> filter 40 val lt : t ::: Type -> col t -> t -> filter