Mercurial > urweb

comparison lib/ur/top.ur @ 719:5c099b1308ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hello compiles with CSS
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 11:08:00 -0400
parents 4e260887d8f2
children acb8537f58f0
comparison
equal deleted inserted replaced
718:f152f215a02c 719:5c099b1308ae
69 f [choice] body 69 f [choice] body
70 70
71 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) 71 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) 72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
73 73
74 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = 74 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (css ::: {Unit}) (_ : show t) (v : t) =
75 cdata (show v) 75 cdata (show v)
76 76
77 fun foldUR (tf :: Type) (tr :: {Unit} -> Type) 77 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
78 (f : nm :: Name -> rest :: {Unit} 78 (f : nm :: Name -> rest :: {Unit}
79 -> [[nm] ~ rest] => 79 -> [[nm] ~ rest] =>
92 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r] 92 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
93 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) [[nm] ~ rest] acc r1 r2 => 93 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) [[nm] ~ rest] acc r1 r2 =>
94 f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 94 f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
95 (fn _ _ => i) 95 (fn _ _ => i)
96 96
97 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) 97 fun foldURX2 (css ::: {Unit}) (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
98 (f : nm :: Name -> rest :: {Unit} 98 (f : nm :: Name -> rest :: {Unit}
99 -> [[nm] ~ rest] => 99 -> [[nm] ~ rest] =>
100 tf1 -> tf2 -> xml ctx [] []) = 100 tf1 -> tf2 -> xml ctx [] [] css) =
101 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] 101 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] [] css]
102 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => 102 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
103 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>) 103 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
104 <xml/> 104 <xml/>
105 105
106 fun foldR K (tf :: K -> Type) (tr :: {K} -> Type) 106 fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
122 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] 122 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
123 (acc : _ -> _ -> tr rest) r1 r2 => 123 (acc : _ -> _ -> tr rest) r1 r2 =>
124 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 124 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
125 (fn _ _ => i) 125 (fn _ _ => i)
126 126
127 fun foldRX K (tf :: K -> Type) (ctx :: {Unit}) 127 fun foldRX K (css ::: {Unit}) (tf :: K -> Type) (ctx :: {Unit})
128 (f : nm :: Name -> t :: K -> rest :: {K} 128 (f : nm :: Name -> t :: K -> rest :: {K}
129 -> [[nm] ~ rest] => 129 -> [[nm] ~ rest] =>
130 tf t -> xml ctx [] []) = 130 tf t -> xml ctx [] [] css) =
131 foldR [tf] [fn _ => xml ctx [] []] 131 foldR [tf] [fn _ => xml ctx [] [] css]
132 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc => 132 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc =>
133 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>) 133 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
134 <xml/> 134 <xml/>
135 135
136 fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit}) 136 fun foldRX2 K (css ::: {Unit}) (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
137 (f : nm :: Name -> t :: K -> rest :: {K} 137 (f : nm :: Name -> t :: K -> rest :: {K}
138 -> [[nm] ~ rest] => 138 -> [[nm] ~ rest] =>
139 tf1 t -> tf2 t -> xml ctx [] []) = 139 tf1 t -> tf2 t -> xml ctx [] [] css) =
140 foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] 140 foldR2 [tf1] [tf2] [fn _ => xml ctx [] [] css]
141 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] 141 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
142 r1 r2 acc => 142 r1 r2 acc =>
143 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) 143 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
144 <xml/> 144 <xml/>
145 145
149 -> transaction unit) = 149 -> transaction unit) =
150 query q 150 query q
151 (fn fs _ => f fs) 151 (fn fs _ => f fs)
152 () 152 ()
153 153
154 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) 154 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (css ::: {Unit})
155 [tables ~ exps] (q : sql_query tables exps) 155 [tables ~ exps] (q : sql_query tables exps)
156 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 156 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
157 -> xml ctx [] []) = 157 -> xml ctx [] [] css) =
158 query q 158 query q
159 (fn fs acc => return <xml>{acc}{f fs}</xml>) 159 (fn fs acc => return <xml>{acc}{f fs}</xml>)
160 <xml/> 160 <xml/>
161 161
162 fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) 162 fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (css ::: {Unit})
163 [tables ~ exps] (q : sql_query tables exps) 163 [tables ~ exps] (q : sql_query tables exps)
164 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 164 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
165 -> transaction (xml ctx [] [])) = 165 -> transaction (xml ctx [] [] css)) =
166 query q 166 query q
167 (fn fs acc => 167 (fn fs acc =>
168 r <- f fs; 168 r <- f fs;
169 return <xml>{acc}{r}</xml>) 169 return <xml>{acc}{r}</xml>)
170 <xml/> 170 <xml/>