annotate demo/more/grid.urs @ 944:da3ec6014d2f

Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents e2194a6793ae
children 8c37699de273
rev   line source
adamc@944 1 con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
adamc@915 2 {Header : string,
adamc@944 3 Project : row -> transaction input,
adamc@944 4 Update : row -> input -> transaction row,
adamc@944 5 Display : input -> xbody,
adamc@944 6 Edit : input -> xbody,
adamc@944 7 Validate : input -> signal bool,
adamc@944 8 CreateFilter : transaction filter,
adamc@944 9 DisplayFilter : filter -> xbody,
adamc@944 10 Filter : filter -> row -> signal bool}
adamc@915 11
adamc@944 12 con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) =>
adamc@944 13 {Initialize : transaction global_input_filter.1,
adamc@944 14 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
adamc@915 15
adamc@935 16 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
adamc@935 17 {Initial : acc,
adamc@935 18 Step : row -> acc -> acc,
adamc@935 19 Display : acc -> xbody}
adamc@935 20
adamc@915 21 functor Make(M : sig
adamc@915 22 type row
adamc@936 23 type key
adamc@936 24 val keyOf : row -> key
adamc@936 25
adamc@915 26 val list : transaction (list row)
adamc@915 27 val new : transaction row
adamc@936 28 val save : key -> row -> transaction unit
adamc@936 29 val delete : key -> transaction unit
adamc@915 30
adamc@944 31 con cols :: {(Type * Type * Type)}
adamc@915 32 val cols : $(map (colMeta row) cols)
adamc@915 33
adamc@915 34 val folder : folder cols
adamc@935 35
adamc@935 36 con aggregates :: {Type}
adamc@935 37 val aggregates : $(map (aggregateMeta row) aggregates)
adamc@937 38 val aggFolder : folder aggregates
adamc@915 39 end) : sig
adamc@915 40 type grid
adamc@915 41
adamc@915 42 val grid : transaction grid
adamc@915 43 val sync : grid -> transaction unit
adamc@915 44 val render : grid -> xbody
adamc@940 45
adamc@940 46 val showSelection : grid -> source bool
adamc@940 47 val selection : grid -> signal (list M.row)
adamc@940 48
adamc@915 49 style tabl
adamc@915 50 style tr
adamc@915 51 style th
adamc@915 52 style td
adamc@943 53 style agg
adamc@915 54 end