Mercurial > urweb

annotate lib/top.urs @ 479:ffa18975e661

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Broaden set of possible especializations
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 14:42:52 -0500
parents 7cb418e9714f
children
rev   line source
adamc@422 1 val not : bool -> bool
adamc@422 2
adamc@329 3 con idT = fn t :: Type => t
adamc@329 4 con record = fn t :: {Type} => $t
adamc@339 5 con fstTT = fn t :: (Type * Type) => t.1
adamc@339 6 con sndTT = fn t :: (Type * Type) => t.2
adamc@445 7 con fstTTT = fn t :: (Type * Type * Type) => t.1
adamc@445 8 con sndTTT = fn t :: (Type * Type * Type) => t.2
adamc@445 9 con thdTTT = fn t :: (Type * Type * Type) => t.3
adamc@329 10
adamc@355 11 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
adamc@355 12 [nm = f t] ++ acc) []
adamc@325 13
adamc@411 14 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
adamc@411 15 [nm = f] ++ acc) []
adamc@411 16
adamc@355 17 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
adamc@355 18 [nm = f t] ++ acc) []
adamc@339 19
adamc@445 20 con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
adamc@445 21 [nm = f t] ++ acc) []
adamc@445 22
adamc@339 23 con ex = fn tf :: (Type -> Type) =>
adamc@355 24 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 25
adamc@339 26 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
adamc@339 27
adamc@325 28 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 29 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 30
adamc@325 31 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@355 32 -> xml ctx use []
adamc@329 33
adamc@411 34 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 35 -> (nm :: Name -> rest :: {Unit}
adamc@411 36 -> fn [[nm] ~ rest] =>
adamc@411 37 tf -> tr rest -> tr ([nm] ++ rest))
adamc@411 38 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
adamc@411 39
adamc@418 40 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 41 -> (nm :: Name -> rest :: {Unit}
adamc@418 42 -> fn [[nm] ~ rest] =>
adamc@418 43 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@418 44 -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
adamc@418 45
adamc@418 46 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@418 47 -> (nm :: Name -> rest :: {Unit}
adamc@418 48 -> fn [[nm] ~ rest] =>
adamc@418 49 tf1 -> tf2 -> xml ctx [] [])
adamc@418 50 -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
adamc@418 51
adamc@336 52 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
adamc@355 53 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 54 -> fn [[nm] ~ rest] =>
adamc@355 55 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 56 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
adamc@336 57
adamc@339 58 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
adamc@355 59 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 60 -> fn [[nm] ~ rest] =>
adamc@355 61 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 62 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
adamc@339 63
adamc@445 64 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
adamc@445 65 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 66 -> fn [[nm] ~ rest] =>
adamc@445 67 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@445 68 -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r
adamc@445 69
adamc@355 70 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
adamc@355 71 -> tr :: ({Type} -> Type)
adamc@355 72 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 73 -> fn [[nm] ~ rest] =>
adamc@355 74 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 75 -> tr []
adamc@355 76 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
adamc@355 77
adamc@339 78 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
adamc@355 79 -> tr :: ({(Type * Type)} -> Type)
adamc@355 80 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 81 -> fn [[nm] ~ rest] =>
adamc@355 82 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 83 -> tr [] -> r :: {(Type * Type)}
adamc@355 84 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
adamc@339 85
adamc@445 86 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
adamc@445 87 -> tr :: ({(Type * Type * Type)} -> Type)
adamc@445 88 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 89 -> fn [[nm] ~ rest] =>
adamc@445 90 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@445 91 -> tr [] -> r :: {(Type * Type * Type)}
adamc@445 92 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r
adamc@445 93
adamc@336 94 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
adamc@355 95 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 96 -> fn [[nm] ~ rest] =>
adamc@355 97 tf t -> xml ctx [] [])
adamc@355 98 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
adamc@336 99
adamc@339 100 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
adamc@355 101 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 102 -> fn [[nm] ~ rest] =>
adamc@355 103 tf t -> xml ctx [] [])
adamc@355 104 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
adamc@339 105
adamc@445 106 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
adamc@445 107 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 108 -> fn [[nm] ~ rest] =>
adamc@445 109 tf t -> xml ctx [] [])
adamc@445 110 -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] []
adamc@445 111
adamc@332 112 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
adamc@355 113 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 114 -> fn [[nm] ~ rest] =>
adamc@355 115 tf1 t -> tf2 t -> xml ctx [] [])
adamc@355 116 -> r :: {Type}
adamc@355 117 -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
adamc@334 118
adamc@355 119 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
adamc@355 120 -> ctx :: {Unit}
adamc@355 121 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 122 -> fn [[nm] ~ rest] =>
adamc@355 123 tf1 t -> tf2 t -> xml ctx [] [])
adamc@355 124 -> r :: {(Type * Type)}
adamc@355 125 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
adamc@339 126
adamc@445 127
adamc@445 128 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
adamc@445 129 -> ctx :: {Unit}
adamc@445 130 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 131 -> fn [[nm] ~ rest] =>
adamc@445 132 tf1 t -> tf2 t -> xml ctx [] [])
adamc@445 133 -> r :: {(Type * Type * Type)}
adamc@445 134 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] []
adamc@445 135
adamc@334 136 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@355 137 -> sql_query tables exps
adamc@355 138 -> fn [tables ~ exps] =>
adamc@355 139 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@355 140 [nm = $fields] ++ acc) [] tables)
adamc@355 141 -> xml ctx [] [])
adamc@355 142 -> transaction (xml ctx [] [])
adamc@341 143
adamc@469 144 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@469 145 -> sql_query tables exps
adamc@469 146 -> fn [tables ~ exps] =>
adamc@469 147 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@469 148 [nm = $fields] ++ acc) [] tables)
adamc@469 149 -> transaction (xml ctx [] []))
adamc@469 150 -> transaction (xml ctx [] [])
adamc@469 151
adamc@355 152 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@355 153 -> sql_query tables exps
adamc@355 154 -> fn [tables ~ exps] =>
adamc@355 155 transaction
adamc@355 156 (option
adamc@355 157 $(exps
adamc@355 158 ++ fold (fn nm (fields :: {Type}) acc
adamc@355 159 [[nm] ~ acc] =>
adamc@355 160 [nm = $fields] ++ acc)
adamc@355 161 [] tables))
adamc@440 162
adamc@440 163 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@440 164 -> sql_query tables exps
adamc@440 165 -> fn [tables ~ exps] =>
adamc@440 166 transaction
adamc@440 167 $(exps
adamc@440 168 ++ fold (fn nm (fields :: {Type}) acc
adamc@440 169 [[nm] ~ acc] =>
adamc@440 170 [nm = $fields] ++ acc)
adamc@440 171 [] tables)
adamc@470 172
adamc@470 173 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 174 -> t ::: Type -> sql_injectable (option t)
adamc@470 175 -> sql_exp tables agg exps (option t)
adamc@470 176 -> sql_exp tables agg exps (option t)
adamc@470 177 -> sql_exp tables agg exps bool
adamc@470 178
adamc@470 179 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 180 -> t ::: Type -> sql_injectable (option t)
adamc@470 181 -> sql_exp tables agg exps (option t)
adamc@470 182 -> option t
adamc@470 183 -> sql_exp tables agg exps bool