Mercurial > urweb

annotate lib/ur/top.urs @ 1260:25ebd8c4fafb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thunking recursive JavaScripted function ASTs, to reduce page load time dramatically
author Adam Chlipala <adamc@hcoop.net>
date Sat, 22 May 2010 14:09:06 -0400
parents 61c3139eab12
children 4172863d049d
rev   line source
adamc@623 1 (** Row folding *)
adamc@623 2
adamc@631 3 con folder :: K --> {K} -> Type
adamc@623 4
adamc@653 5 val fold : K --> tf :: ({K} -> Type)
adamc@653 6 -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
adamc@653 7 tf r -> tf ([nm = v] ++ r))
adamc@653 8 -> tf []
adamc@1093 9 -> r ::: {K} -> folder r -> tf r
adamc@653 10
adamc@627 11 structure Folder : sig
adamc@627 12 val nil : K --> folder (([]) :: {K})
adamc@627 13 val cons : K --> r ::: {K} -> nm :: Name -> v :: K
adamc@629 14 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
adamc@628 15 val concat : K --> r1 ::: {K} -> r2 ::: {K}
adamc@629 16 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
adamc@630 17 val mp : K1 --> K2 --> f ::: (K1 -> K2) -> r ::: {K1}
adamc@630 18 -> folder r -> folder (map f r)
adamc@627 19 end
adamc@627 20
adamc@623 21
adamc@422 22 val not : bool -> bool
adamc@422 23
adamc@898 24 con id = K ==> fn t :: K => t
adamc@329 25 con record = fn t :: {Type} => $t
adamc@637 26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
adamc@637 27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
adamc@637 28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
adamc@637 29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
adamc@637 30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
adamc@329 31
adamc@643 32 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
adamc@445 33
adamc@339 34 con ex = fn tf :: (Type -> Type) =>
adamc@355 35 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 36
adamc@339 37 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
adamc@339 38
adamc@325 39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 41
adamc@777 42 val show_option : t ::: Type -> show t -> show (option t)
adamc@777 43 val read_option : t ::: Type -> read t -> read (option t)
adamc@777 44
adamc@720 45 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@720 46 -> xml ctx use []
adamc@329 47
adamc@993 48 val map0 : K --> tf :: (K -> Type)
adamc@993 49 -> (t :: K -> tf t)
adamc@1093 50 -> r ::: {K} -> folder r -> $(map tf r)
adamc@898 51 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@898 52 -> (t ::: K -> tf1 t -> tf2 t)
adamc@1093 53 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
adamc@937 54 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 55 -> (t ::: K -> tf1 t -> tf2 t -> tf t)
adamc@1093 56 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
adamc@937 57 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 58 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
adamc@1093 59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
adamc@898 60
adamc@411 61 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 62 -> (nm :: Name -> rest :: {Unit}
adamc@629 63 -> [[nm] ~ rest] =>
adamc@411 64 tf -> tr rest -> tr ([nm] ++ rest))
adamc@1093 65 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
adamc@411 66
adamc@418 67 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 68 -> (nm :: Name -> rest :: {Unit}
adamc@629 69 -> [[nm] ~ rest] =>
adamc@418 70 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@1093 71 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
adamc@418 72
adamc@623 73 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
adamc@623 74 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 75 -> [[nm] ~ rest] =>
adamc@355 76 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 77 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
adamc@336 78
adamc@623 79 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@623 80 -> tr :: ({K} -> Type)
adamc@623 81 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 82 -> [[nm] ~ rest] =>
adamc@623 83 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@623 84 -> tr []
adamc@1093 85 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@623 86
adamc@910 87 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
adamc@910 88 -> tr :: ({K} -> Type)
adamc@910 89 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@910 90 -> [[nm] ~ rest] =>
adamc@910 91 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@910 92 -> tr []
adamc@1093 93 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
adamc@910 94
adamc@1172 95 val mapUX : tf :: Type -> ctx :: {Unit}
adamc@1172 96 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
adamc@1172 97 tf -> xml ctx [] [])
adamc@1172 98 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
adamc@623 99
adamc@1172 100 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit}
adamc@1172 101 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 102 -> [[nm] ~ rest] =>
adamc@1172 103 tf t -> xml ctx [] [])
adamc@1172 104 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
adamc@445 105
adamc@1173 106 val mapUX2 : tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@1173 107 -> (nm :: Name -> rest :: {Unit}
adamc@1173 108 -> [[nm] ~ rest] =>
adamc@1173 109 tf1 -> tf2 -> xml ctx [] [])
adamc@1173 110 -> r ::: {Unit} -> folder r
adamc@1173 111 -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
adamc@1173 112
adamc@1172 113 val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 114 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 115 -> [[nm] ~ rest] =>
adamc@1172 116 tf1 t -> tf2 t -> xml ctx [] [])
adamc@1172 117 -> r ::: {K} -> folder r
adamc@1172 118 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@1172 119
adamc@1172 120 val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 121 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 122 -> [[nm] ~ rest] =>
adamc@1172 123 tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
adamc@1172 124 -> r ::: {K} -> folder r
adamc@1172 125 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
adamc@910 126
adamc@1081 127 val queryL : tables ::: {{Type}} -> exps ::: {Type}
adamc@1081 128 -> [tables ~ exps] =>
adamc@1191 129 sql_query [] tables exps
adamc@1081 130 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
adamc@1081 131
adamc@1177 132 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
adamc@1191 133 -> sql_query [] [t = fs] []
adamc@1177 134 -> ($fs -> state -> transaction state)
adamc@1177 135 -> state
adamc@1177 136 -> transaction state
adamc@1177 137
adamc@1177 138 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
adamc@1191 139 -> sql_query [] [t = fs] []
adamc@1177 140 -> ($fs -> state -> state)
adamc@1177 141 -> state
adamc@1177 142 -> transaction state
adamc@1177 143
adamc@682 144 val queryI : tables ::: {{Type}} -> exps ::: {Type}
adamc@682 145 -> [tables ~ exps] =>
adamc@1191 146 sql_query [] tables exps
adamc@682 147 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 148 -> transaction unit)
adamc@682 149 -> transaction unit
adamc@682 150
adamc@1004 151 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 152 -> [tables ~ exps] =>
adamc@1191 153 sql_query [] tables exps
adamc@632 154 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 155 -> xml ctx inp [])
adamc@1004 156 -> transaction (xml ctx inp [])
adamc@341 157
adamc@1076 158 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@1191 159 -> sql_query [] [nm = fs] []
adamc@1076 160 -> ($fs -> xml ctx inp [])
adamc@1076 161 -> transaction (xml ctx inp [])
adamc@1076 162
adamc@1032 163 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 164 -> [tables ~ exps] =>
adamc@1191 165 sql_query [] tables exps
adamc@632 166 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 167 -> transaction (xml ctx inp []))
adamc@1032 168 -> transaction (xml ctx inp [])
adamc@1110 169 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@1191 170 -> sql_query [] [nm = fs] []
adamc@1110 171 -> ($fs -> transaction (xml ctx inp []))
adamc@1110 172 -> transaction (xml ctx inp [])
adamc@1110 173 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@1191 174 -> sql_query [] [] exps
adamc@1110 175 -> ($exps -> transaction (xml ctx inp []))
adamc@1110 176 -> transaction (xml ctx inp [])
adamc@1110 177
adamc@1072 178 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@1072 179 -> [tables ~ exps] =>
adamc@1191 180 sql_query [] tables exps
adamc@1072 181 -> transaction bool
adamc@1072 182
adamc@355 183 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 184 -> [tables ~ exps] =>
adamc@1191 185 sql_query [] tables exps
adamc@629 186 -> transaction
adamc@629 187 (option
adamc@629 188 $(exps
adamc@629 189 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 190
adamc@1003 191 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
adamc@1191 192 -> sql_query [] [nm = fs] []
adamc@1003 193 -> transaction (option $fs)
adamc@1003 194
adamc@1076 195 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1076 196 -> [tabs ~ [nm]] =>
adamc@1191 197 sql_query [] (mapU [] tabs) [nm = t]
adamc@1006 198 -> transaction (option t)
adamc@1006 199
adamc@440 200 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 201 -> [tables ~ exps] =>
adamc@1191 202 sql_query [] tables exps
adamc@629 203 -> transaction
adamc@629 204 $(exps
adamc@629 205 ++ map (fn fields :: {Type} => $fields) tables)
adamc@1003 206
adamc@1076 207 val oneRow1 : nm ::: Name -> fs ::: {Type}
adamc@1191 208 -> sql_query [] [nm = fs] []
adamc@1076 209 -> transaction $fs
adamc@1076 210
adamc@1064 211 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1064 212 -> [tabs ~ [nm]] =>
adamc@1191 213 sql_query [] (mapU [] tabs) [nm = t]
adamc@1003 214 -> transaction t
adamc@1003 215
adamc@1074 216 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
adamc@1074 217 -> transaction bool
adamc@1074 218
adamc@470 219 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 220 -> t ::: Type -> sql_injectable (option t)
adamc@470 221 -> sql_exp tables agg exps (option t)
adamc@470 222 -> sql_exp tables agg exps (option t)
adamc@470 223 -> sql_exp tables agg exps bool
adamc@470 224
adamc@470 225 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 226 -> t ::: Type -> sql_injectable (option t)
adamc@470 227 -> sql_exp tables agg exps (option t)
adamc@470 228 -> option t
adamc@470 229 -> sql_exp tables agg exps bool