Mercurial > urweb

comparison lib/top.ur @ 360:c1e96b387115

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Syntax highlighting for embedded XML
author Adam Chlipala <adamc@hcoop.net>
date Tue, 14 Oct 2008 16:37:43 -0400
parents 383c72d11db8
children 28d3d7210687
comparison
equal deleted inserted replaced
359:465593c024ca 360:c1e96b387115
72 -> fn [[nm] ~ rest] => 72 -> fn [[nm] ~ rest] =>
73 tf t -> xml ctx [] []) = 73 tf t -> xml ctx [] []) =
74 foldTR [tf] [fn _ => xml ctx [] []] 74 foldTR [tf] [fn _ => xml ctx [] []]
75 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => 75 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc =>
76 <xml>{f [nm] [t] [rest] r}{acc}</xml>) 76 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
77 <xml></xml> 77 <xml/>
78 78
79 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) 79 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
80 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 80 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
81 -> fn [[nm] ~ rest] => 81 -> fn [[nm] ~ rest] =>
82 tf t -> xml ctx [] []) = 82 tf t -> xml ctx [] []) =
83 foldT2R [tf] [fn _ => xml ctx [] []] 83 foldT2R [tf] [fn _ => xml ctx [] []]
84 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) 84 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
85 [[nm] ~ rest] r acc => 85 [[nm] ~ rest] r acc =>
86 <xml>{f [nm] [t] [rest] r}{acc}</xml>) 86 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
87 <xml></xml> 87 <xml/>
88 88
89 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) 89 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
90 (f : nm :: Name -> t :: Type -> rest :: {Type} 90 (f : nm :: Name -> t :: Type -> rest :: {Type}
91 -> fn [[nm] ~ rest] => 91 -> fn [[nm] ~ rest] =>
92 tf1 t -> tf2 t -> xml ctx [] []) = 92 tf1 t -> tf2 t -> xml ctx [] []) =
93 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] 93 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
94 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] 94 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest]
95 r1 r2 acc => 95 r1 r2 acc =>
96 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 96 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
97 <xml></xml> 97 <xml/>
98 98
99 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) 99 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
100 (ctx :: {Unit}) 100 (ctx :: {Unit})
101 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 101 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
102 -> fn [[nm] ~ rest] => 102 -> fn [[nm] ~ rest] =>
103 tf1 t -> tf2 t -> xml ctx [] []) = 103 tf1 t -> tf2 t -> xml ctx [] []) =
104 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] 104 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
105 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) 105 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
106 [[nm] ~ rest] r1 r2 acc => 106 [[nm] ~ rest] r1 r2 acc =>
107 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 107 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
108 <xml></xml> 108 <xml/>
109 109
110 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) 110 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
111 (q : sql_query tables exps) [tables ~ exps] 111 (q : sql_query tables exps) [tables ~ exps]
112 (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 112 (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
113 [nm = $fields] ++ acc) [] tables) 113 [nm = $fields] ++ acc) [] tables)
114 -> xml ctx [] []) = 114 -> xml ctx [] []) =
115 query q 115 query q
116 (fn fs acc => return <xml>{acc}{f fs}</xml>) 116 (fn fs acc => return <xml>{acc}{f fs}</xml>)
117 <xml></xml> 117 <xml/>
118 118
119 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) 119 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type})
120 (q : sql_query tables exps) [tables ~ exps] = 120 (q : sql_query tables exps) [tables ~ exps] =
121 query q 121 query q
122 (fn fs _ => return (Some fs)) 122 (fn fs _ => return (Some fs))