Mercurial > urweb
annotate demo/more/meta.urs @ 1205:7cd11380cdf1
WHERE-dependent checking
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 04 Apr 2010 17:18:41 -0400 |
parents | 6bcc1020d5cd |
children |
rev | line source |
---|---|
adamc@1004 | 1 con meta = fn (db :: Type, widget :: Type) => |
adamc@1004 | 2 {Nam : string, |
adamc@1004 | 3 Show : db -> xbody, |
adamc@1004 | 4 Widget : nm :: Name -> xml form [] [nm = widget], |
adamc@1004 | 5 WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], |
adamc@1004 | 6 Parse : widget -> db, |
adamc@1004 | 7 Inject : sql_injectable db} |
adamc@1004 | 8 |
adamc@1004 | 9 val int : string -> meta (int, string) |
adamc@1004 | 10 val float : string -> meta (float, string) |
adamc@1004 | 11 val string : string -> meta (string, string) |
adamc@1004 | 12 val bool : string -> meta (bool, bool) |
adamc@1007 | 13 |
adamc@1007 | 14 val textarea : string -> meta (string, string) |
adamc@1007 | 15 |
adamc@1009 | 16 val allContent : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts -> xbody |
adamc@1009 | 17 |
adamc@1007 | 18 val allWidgets : ts ::: {(Type * Type)} -> $(map meta ts) -> folder ts |
adamc@1007 | 19 -> xml form [] (map snd ts) |
adamc@1008 | 20 |
adamc@1011 | 21 val allPopulated : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts |
adamc@1011 | 22 -> xml form [] (map snd ts) |
adamc@1011 | 23 |
adamc@1008 | 24 val allPopulatedTr : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts |
adamc@1008 | 25 -> xml ([Tr] ++ form) [] (map snd ts) |
adamc@1008 | 26 |
adamc@1008 | 27 val ensql : avail ::: {{Type}} -> ts ::: {(Type * Type)} -> $(map meta ts) -> $(map snd ts) -> folder ts |
adamc@1008 | 28 -> $(map (sql_exp avail [] []) (map fst ts)) |
adamc@1030 | 29 |
adamc@1030 | 30 con private = fn t :: Type => |
adamc@1030 | 31 {Nam : string, |
adamc@1030 | 32 Initialize : t, |
adamc@1030 | 33 Show : t -> xbody, |
adamc@1030 | 34 Inject : sql_injectable t} |
adamc@1030 | 35 |
adamc@1030 | 36 val initialize : ts ::: {Type} -> $(map private ts) -> folder ts -> $(map (sql_exp [] [] []) ts) |