Ur/Web: demo/crud.urs annotate

Implemented proper congruence closure, to the point where tests/policy works

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 08 Apr 2010 12:46:21 -0400
parents	bb3fc575cfe7
children

rev	line source
adamc@1002	1 con colMeta = fn (db :: Type, widget :: Type) =>
adamc@421	2 {Nam : string,
adamc@1002	3 Show : db -> xbody,
adamc@1002	4 Widget : nm :: Name -> xml form [] [nm = widget],
adamc@1002	5 WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
adamc@1002	6 Parse : widget -> db,
adamc@1002	7 Inject : sql_injectable db}
adamc@622	8 con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
adamc@421	9
adamc@421	10 val int : string -> colMeta (int, string)
adamc@421	11 val float : string -> colMeta (float, string)
adamc@421	12 val string : string -> colMeta (string, string)
adamc@421	13 val bool : string -> colMeta (bool, bool)
adamc@421	14
adamc@421	15 functor Make(M : sig
adamc@421	16 con cols :: {(Type * Type)}
adamc@421	17 constraint [Id] ~ cols
adamc@632	18 val fl : folder cols
adamc@632	19
adamc@706	20 table tab : ([Id = int] ++ map fst cols)
adamc@421	21
adamc@421	22 val title : string
adamc@421	23
adamc@421	24 val cols : colsMeta cols
adamc@421	25 end) : sig
adamc@421	26 val main : unit -> transaction page
adamc@421	27 end

Mercurial > urweb