Mercurial > urweb

annotate demo/more/meta.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
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 fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : meta (t, string) =
adamc@1004 10 {Nam = name,
adamc@1004 11 Show = txt,
adamc@1004 12 Widget = fn [nm :: Name] => <xml><textbox{nm}/></xml>,
adamc@1004 13 WidgetPopulated = fn [nm :: Name] n =>
adamc@1004 14 <xml><textbox{nm} value={show n}/></xml>,
adamc@1004 15 Parse = readError,
adamc@1004 16 Inject = _}
adamc@1004 17
adamc@1004 18 val int = default
adamc@1004 19 val float = default
adamc@1004 20 val string = default
adamc@1004 21 fun bool name = {Nam = name,
adamc@1004 22 Show = txt,
adamc@1004 23 Widget = fn [nm :: Name] => <xml><checkbox{nm}/></xml>,
adamc@1004 24 WidgetPopulated = fn [nm :: Name] b =>
adamc@1004 25 <xml><checkbox{nm} checked={b}/></xml>,
adamc@1004 26 Parse = fn x => x,
adamc@1004 27 Inject = _}
adamc@1007 28
adamc@1007 29 fun textarea name = {Nam = name,
adamc@1007 30 Show = cdata,
adamc@1007 31 Widget = fn [nm :: Name] => <xml><br/><textarea{nm} rows={10} cols={80}/></xml>,
adamc@1007 32 WidgetPopulated = fn [nm :: Name] s => <xml><br/>
adamc@1007 33 <textarea{nm} rows={10} cols={80}>{[s]}</textarea>
adamc@1007 34 </xml>,
adamc@1007 35 Parse = fn s => s,
adamc@1007 36 Inject = _}
adamc@1007 37
adamc@1009 38 fun allContent [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) =
adamc@1009 39 foldRX2 [meta] [fst] [_]
adamc@1009 40 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
adamc@1009 41 (m : meta p) v =>
adamc@1009 42 <xml><b>{[m.Nam]}</b>: {m.Show v}<br/></xml>)
adamc@1009 43 [_] fl r vs
adamc@1009 44
adamc@1007 45 fun allWidgets [ts ::: {(Type * Type)}] (r : $(map meta ts)) (fl : folder ts) =
adamc@1007 46 foldR [meta] [fn ts :: {(Type * Type)} => xml form [] (map snd ts)]
adamc@1007 47 (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
adamc@1007 48 [[nm] ~ rest] (col : meta t) (acc : xml form [] (map snd rest)) => <xml>
adamc@1007 49 <b>{[col.Nam]}</b>: {col.Widget [nm]}<br/>
adamc@1007 50 {useMore acc}
adamc@1007 51 </xml>)
adamc@1007 52 <xml/>
adamc@1007 53 [_] fl r
adamc@1008 54
adamc@1011 55 fun allPopulated [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) =
adamc@1011 56 foldR2 [meta] [fst] [fn cols :: {(Type * Type)} =>
adamc@1011 57 xml form [] (map snd cols)]
adamc@1011 58 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
adamc@1011 59 (m : meta p) v (acc : xml form [] (map snd rest)) =>
adamc@1011 60 <xml>
adamc@1011 61 {[m.Nam]}: {m.WidgetPopulated [nm] v}<br/>
adamc@1011 62 {useMore acc}
adamc@1011 63 </xml>)
adamc@1011 64 <xml/>
adamc@1011 65 [_] fl r vs
adamc@1011 66
adamc@1008 67 fun allPopulatedTr [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) =
adamc@1008 68 foldR2 [meta] [fst] [fn cols :: {(Type * Type)} =>
adamc@1008 69 xml [Body, Form, Tr] [] (map snd cols)]
adamc@1008 70 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
adamc@1008 71 (m : meta p) v (acc : xml [Body, Form, Tr] [] (map snd rest)) =>
adamc@1008 72 <xml>
adamc@1008 73 <td>{m.WidgetPopulated [nm] v}</td>
adamc@1008 74 {useMore acc}
adamc@1008 75 </xml>)
adamc@1008 76 <xml/>
adamc@1008 77 [_] fl r vs
adamc@1008 78
adamc@1008 79 fun ensql [avail] [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map snd ts)) (fl : folder ts) =
adamc@1008 80 map2 [meta] [snd] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
adamc@1008 81 (fn [ts] meta v => @sql_inject meta.Inject (meta.Parse v))
adamc@1008 82 [_] fl r vs
adamc@1030 83
adamc@1030 84 con private = fn t :: Type =>
adamc@1030 85 {Nam : string,
adamc@1030 86 Initialize : t,
adamc@1030 87 Show : t -> xbody,
adamc@1030 88 Inject : sql_injectable t}
adamc@1030 89
adamc@1030 90 fun initialize [ts] (r : $(map private ts)) (fl : folder ts) =
adamc@1030 91 mp [private] [sql_exp [] [] []] (fn [t] r => @sql_inject r.Inject r.Initialize) [_] fl r