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
|
adam@1321
|
132 val queryL1 : t ::: Name -> fs ::: {Type}
|
adam@1321
|
133 -> sql_query [] [t = fs] []
|
adam@1321
|
134 -> transaction (list $fs)
|
adam@1321
|
135
|
adamc@1177
|
136 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
|
adamc@1191
|
137 -> sql_query [] [t = fs] []
|
adamc@1177
|
138 -> ($fs -> state -> transaction state)
|
adamc@1177
|
139 -> state
|
adamc@1177
|
140 -> transaction state
|
adamc@1177
|
141
|
adamc@1177
|
142 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
|
adamc@1191
|
143 -> sql_query [] [t = fs] []
|
adamc@1177
|
144 -> ($fs -> state -> state)
|
adamc@1177
|
145 -> state
|
adamc@1177
|
146 -> transaction state
|
adamc@1177
|
147
|
adamc@682
|
148 val queryI : tables ::: {{Type}} -> exps ::: {Type}
|
adamc@682
|
149 -> [tables ~ exps] =>
|
adamc@1191
|
150 sql_query [] tables exps
|
adamc@682
|
151 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@682
|
152 -> transaction unit)
|
adamc@682
|
153 -> transaction unit
|
adamc@682
|
154
|
adam@1363
|
155 val queryI1 : nm ::: Name -> fs ::: {Type}
|
adam@1363
|
156 -> sql_query [] [nm = fs] []
|
adam@1363
|
157 -> ($fs -> transaction unit)
|
adam@1363
|
158 -> transaction unit
|
adam@1363
|
159
|
adamc@1004
|
160 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
|
adamc@629
|
161 -> [tables ~ exps] =>
|
adamc@1191
|
162 sql_query [] tables exps
|
adamc@632
|
163 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@1004
|
164 -> xml ctx inp [])
|
adamc@1004
|
165 -> transaction (xml ctx inp [])
|
adamc@341
|
166
|
adamc@1076
|
167 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
|
adamc@1191
|
168 -> sql_query [] [nm = fs] []
|
adamc@1076
|
169 -> ($fs -> xml ctx inp [])
|
adamc@1076
|
170 -> transaction (xml ctx inp [])
|
adamc@1076
|
171
|
adamc@1032
|
172 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
|
adamc@629
|
173 -> [tables ~ exps] =>
|
adamc@1191
|
174 sql_query [] tables exps
|
adamc@632
|
175 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@1032
|
176 -> transaction (xml ctx inp []))
|
adamc@1032
|
177 -> transaction (xml ctx inp [])
|
adamc@1110
|
178 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
|
adamc@1191
|
179 -> sql_query [] [nm = fs] []
|
adamc@1110
|
180 -> ($fs -> transaction (xml ctx inp []))
|
adamc@1110
|
181 -> transaction (xml ctx inp [])
|
adamc@1110
|
182 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
|
adamc@1191
|
183 -> sql_query [] [] exps
|
adamc@1110
|
184 -> ($exps -> transaction (xml ctx inp []))
|
adamc@1110
|
185 -> transaction (xml ctx inp [])
|
adamc@1110
|
186
|
adamc@1072
|
187 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
|
adamc@1072
|
188 -> [tables ~ exps] =>
|
adamc@1191
|
189 sql_query [] tables exps
|
adamc@1072
|
190 -> transaction bool
|
adamc@1072
|
191
|
adamc@355
|
192 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
|
adamc@629
|
193 -> [tables ~ exps] =>
|
adamc@1191
|
194 sql_query [] tables exps
|
adamc@629
|
195 -> transaction
|
adamc@629
|
196 (option
|
adamc@629
|
197 $(exps
|
adamc@629
|
198 ++ map (fn fields :: {Type} => $fields) tables))
|
adamc@440
|
199
|
adamc@1003
|
200 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
|
adamc@1191
|
201 -> sql_query [] [nm = fs] []
|
adamc@1003
|
202 -> transaction (option $fs)
|
adamc@1003
|
203
|
adamc@1076
|
204 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
|
adamc@1076
|
205 -> [tabs ~ [nm]] =>
|
adamc@1191
|
206 sql_query [] (mapU [] tabs) [nm = t]
|
adamc@1006
|
207 -> transaction (option t)
|
adamc@1006
|
208
|
adamc@440
|
209 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
|
adamc@629
|
210 -> [tables ~ exps] =>
|
adamc@1191
|
211 sql_query [] tables exps
|
adamc@629
|
212 -> transaction
|
adamc@629
|
213 $(exps
|
adamc@629
|
214 ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@1003
|
215
|
adamc@1076
|
216 val oneRow1 : nm ::: Name -> fs ::: {Type}
|
adamc@1191
|
217 -> sql_query [] [nm = fs] []
|
adamc@1076
|
218 -> transaction $fs
|
adamc@1076
|
219
|
adamc@1064
|
220 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
|
adamc@1064
|
221 -> [tabs ~ [nm]] =>
|
adamc@1191
|
222 sql_query [] (mapU [] tabs) [nm = t]
|
adamc@1003
|
223 -> transaction t
|
adamc@1003
|
224
|
adamc@1074
|
225 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
|
adamc@1074
|
226 -> transaction bool
|
adamc@1074
|
227
|
adamc@470
|
228 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@470
|
229 -> t ::: Type -> sql_injectable (option t)
|
adamc@470
|
230 -> sql_exp tables agg exps (option t)
|
adamc@470
|
231 -> sql_exp tables agg exps (option t)
|
adamc@470
|
232 -> sql_exp tables agg exps bool
|
adamc@470
|
233
|
adamc@470
|
234 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@470
|
235 -> t ::: Type -> sql_injectable (option t)
|
adamc@470
|
236 -> sql_exp tables agg exps (option t)
|
adamc@470
|
237 -> option t
|
adamc@470
|
238 -> sql_exp tables agg exps bool
|
adam@1360
|
239
|
adam@1360
|
240 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t
|