annotate demo/more/orm.urs @ 991:b132f8620a66

Initial Orm1 demo
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 10:34:27 -0400
parents 46803e668a89
children bb3fc575cfe7
rev   line source
adamc@990 1 con link :: (Type * Type) -> Type
adamc@990 2 val noParent : t ::: Type -> link (t, unit)
adamc@987 3
adamc@990 4 con meta = fn col_parent :: (Type * Type) => {
adamc@990 5 Link : link col_parent,
adamc@990 6 Inj : sql_injectable col_parent.1
adamc@987 7 }
adamc@987 8
adamc@991 9 val local : t :: Type -> sql_injectable t -> meta (t, unit)
adamc@991 10
adamc@987 11 functor Table(M : sig
adamc@990 12 con cols :: {(Type * Type)}
adamc@987 13 val cols : $(map meta cols)
adamc@987 14 constraint [Id] ~ cols
adamc@987 15 val folder : folder cols
adamc@987 16 end) : sig
adamc@987 17 type id
adamc@990 18 type row' = $(map fst M.cols)
adamc@990 19 type row = $([Id = id] ++ map fst M.cols)
adamc@990 20
adamc@987 21 val inj : sql_injectable id
adamc@990 22 val id : meta (id, row)
adamc@987 23
adamc@990 24 val create : row' -> transaction row
adamc@988 25 val delete : row -> transaction unit
adamc@988 26 val save : row -> transaction unit
adamc@988 27 val lookup : id -> transaction (option row)
adamc@988 28 val list : transaction (list row)
adamc@989 29
adamc@989 30 con col :: Type -> Type
adamc@989 31 val idCol : col id
adamc@990 32 val cols : $(map (fn col_parent :: (Type * Type) =>
adamc@990 33 {Col : col col_parent.1,
adamc@990 34 Parent : row -> transaction (option col_parent.2)}) M.cols)
adamc@989 35
adamc@989 36 type filter
adamc@990 37 val find : filter -> transaction (option row)
adamc@989 38 val search : filter -> transaction (list row)
adamc@989 39
adamc@989 40 val eq : t ::: Type -> col t -> t -> filter
adamc@989 41 val ne : t ::: Type -> col t -> t -> filter
adamc@989 42 val lt : t ::: Type -> col t -> t -> filter
adamc@989 43 val le : t ::: Type -> col t -> t -> filter
adamc@989 44 val gt : t ::: Type -> col t -> t -> filter
adamc@989 45 val ge : t ::: Type -> col t -> t -> filter
adamc@989 46
adamc@989 47 val _and : filter -> filter -> filter
adamc@989 48 val or : filter -> filter -> filter
adamc@987 49 end