annotate demo/more/orm.urs @ 2297:6d56080f495c

Fix a read-after-free bug using a timestamp check
author Adam Chlipala <adam@chlipala.net>
date Thu, 19 Nov 2015 13:18:58 -0500
parents bb3fc575cfe7
children
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@1002 4 con meta = fn (col :: Type, parent :: Type) => {
adamc@1002 5 Link : link (col, parent),
adamc@1002 6 Inj : sql_injectable col
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@1002 32 val cols : $(map (fn (colm :: Type, parent :: Type) =>
adamc@1002 33 {Col : col colm,
adamc@1002 34 Parent : row -> transaction (option parent)}) 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