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

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 (2009-11-17)
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