Mercurial > urweb
comparison src/termination.sml @ 410:c5a3d223f157
Sql demo
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 21 Oct 2008 18:44:52 -0400 |
parents | 075b36dbb1a4 |
children | dfc8c991abd0 |
comparison
equal
deleted
inserted
replaced
409:81d9f42bb641 | 410:c5a3d223f157 |
---|---|
29 | 29 |
30 open Elab | 30 open Elab |
31 | 31 |
32 structure E = ElabEnv | 32 structure E = ElabEnv |
33 structure IM = IntBinaryMap | 33 structure IM = IntBinaryMap |
34 structure IS = IntBinarySet | |
34 | 35 |
35 datatype pedigree = | 36 datatype pedigree = |
36 Func of int | 37 Func of int |
37 | Arg of int * int * con | 38 | Arg of int * int * con |
38 | Subarg of int * int * con | 39 | Subarg of int * int * con |
116 | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps) | 117 | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps) |
117 | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps) | 118 | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps) |
118 | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps | 119 | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps |
119 end | 120 end |
120 | 121 |
121 fun exp (penv, calls) e = | 122 fun exp parent (penv, calls) e = |
122 let | 123 let |
123 val default = (Rabble, calls) | 124 val default = (Rabble, calls) |
124 | 125 |
125 fun apps () = | 126 fun apps () = |
126 let | 127 let |
155 | 156 |
156 val calls = foldl (fn ((x, e, _), calls) => | 157 val calls = foldl (fn ((x, e, _), calls) => |
157 if checkName x then | 158 if checkName x then |
158 calls | 159 calls |
159 else | 160 else |
160 #2 (exp (penv, calls) e)) calls xets | 161 #2 (exp parent (penv, calls) e)) calls xets |
161 in | 162 in |
162 (Rabble, [Rabble], calls) | 163 (Rabble, [Rabble], calls) |
163 end | 164 end |
164 | 165 |
165 | EApp (e1, e2) => | 166 | EApp (e1, e2) => |
166 let | 167 let |
167 val (p1, ps, calls) = combiner calls e1 | 168 val (p1, ps, calls) = combiner calls e1 |
168 val (p2, calls) = exp (penv, calls) e2 | 169 val (p2, calls) = exp parent (penv, calls) e2 |
169 | 170 |
170 val p = case p1 of | 171 val p = case p1 of |
171 Rabble => Rabble | 172 Rabble => Rabble |
172 | Arg _ => Rabble | 173 | Arg _ => Rabble |
173 | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran) | 174 | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran) |
189 in | 190 in |
190 (p, ps, calls) | 191 (p, ps, calls) |
191 end | 192 end |
192 | _ => | 193 | _ => |
193 let | 194 let |
194 val (p, calls) = exp (penv, calls) e | 195 val (p, calls) = exp parent (penv, calls) e |
195 in | 196 in |
196 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; | 197 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; |
197 print (p2s p ^ "\n");*) | 198 print (p2s p ^ "\n");*) |
198 (p, [p], calls) | 199 (p, [p], calls) |
199 end | 200 end |
203 val calls = | 204 val calls = |
204 case ps of | 205 case ps of |
205 [] => raise Fail "Termination: Empty ps" | 206 [] => raise Fail "Termination: Empty ps" |
206 | f :: ps => | 207 | f :: ps => |
207 case f of | 208 case f of |
208 Func i => (i, ps) :: calls | 209 Func i => (parent, i, ps) :: calls |
209 | _ => calls | 210 | _ => calls |
210 in | 211 in |
211 (p, calls) | 212 (p, calls) |
212 end | 213 end |
213 in | 214 in |
225 | EModProj _ => default | 226 | EModProj _ => default |
226 | 227 |
227 | EApp _ => apps () | 228 | EApp _ => apps () |
228 | EAbs (_, _, _, e) => | 229 | EAbs (_, _, _, e) => |
229 let | 230 let |
230 val (_, calls) = exp (Rabble :: penv, calls) e | 231 val (_, calls) = exp parent (Rabble :: penv, calls) e |
231 in | 232 in |
232 (Rabble, calls) | 233 (Rabble, calls) |
233 end | 234 end |
234 | ECApp _ => apps () | 235 | ECApp _ => apps () |
235 | ECAbs (_, _, _, e) => | 236 | ECAbs (_, _, _, e) => |
236 let | 237 let |
237 val (_, calls) = exp (penv, calls) e | 238 val (_, calls) = exp parent (penv, calls) e |
238 in | 239 in |
239 (Rabble, calls) | 240 (Rabble, calls) |
240 end | 241 end |
241 | 242 |
242 | ERecord xets => | 243 | ERecord xets => |
243 let | 244 let |
244 val calls = foldl (fn ((_, e, _), calls) => #2 (exp (penv, calls) e)) calls xets | 245 val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets |
245 in | 246 in |
246 (Rabble, calls) | 247 (Rabble, calls) |
247 end | 248 end |
248 | EField (e, x, _) => | 249 | EField (e, x, _) => |
249 let | 250 let |
250 val (p, calls) = exp (penv, calls) e | 251 val (p, calls) = exp parent (penv, calls) e |
251 val p = | 252 val p = |
252 case p of | 253 case p of |
253 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) => | 254 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) => |
254 (case List.find (fn (x', _) => namesEq (x, x')) xts of | 255 (case List.find (fn (x', _) => namesEq (x, x')) xts of |
255 NONE => Rabble | 256 NONE => Rabble |
258 in | 259 in |
259 (p, calls) | 260 (p, calls) |
260 end | 261 end |
261 | ECut (e, _, _) => | 262 | ECut (e, _, _) => |
262 let | 263 let |
263 val (_, calls) = exp (penv, calls) e | 264 val (_, calls) = exp parent (penv, calls) e |
264 in | 265 in |
265 (Rabble, calls) | 266 (Rabble, calls) |
266 end | 267 end |
267 | EWith (e1, _, e2, _) => | 268 | EWith (e1, _, e2, _) => |
268 let | 269 let |
269 val (_, calls) = exp (penv, calls) e1 | 270 val (_, calls) = exp parent (penv, calls) e1 |
270 val (_, calls) = exp (penv, calls) e2 | 271 val (_, calls) = exp parent (penv, calls) e2 |
271 in | 272 in |
272 (Rabble, calls) | 273 (Rabble, calls) |
273 end | 274 end |
274 | EFold _ => (Rabble, calls) | 275 | EFold _ => (Rabble, calls) |
275 | 276 |
276 | ECase (e, pes, _) => | 277 | ECase (e, pes, _) => |
277 let | 278 let |
278 val (p, calls) = exp (penv, calls) e | 279 val (p, calls) = exp parent (penv, calls) e |
279 | 280 |
280 val calls = foldl (fn ((pt, e), calls) => | 281 val calls = foldl (fn ((pt, e), calls) => |
281 let | 282 let |
282 val penv = pat penv (p, pt) | 283 val penv = pat penv (p, pt) |
283 val (_, calls) = exp (penv, calls) e | 284 val (_, calls) = exp parent (penv, calls) e |
284 in | 285 in |
285 calls | 286 calls |
286 end) calls pes | 287 end) calls pes |
287 in | 288 in |
288 (Rabble, calls) | 289 (Rabble, calls) |
289 end | 290 end |
290 | 291 |
291 | EError => (Rabble, calls) | 292 | EError => (Rabble, calls) |
292 | EUnif (ref (SOME e)) => exp (penv, calls) e | 293 | EUnif (ref (SOME e)) => exp parent (penv, calls) e |
293 | EUnif (ref NONE) => (Rabble, calls) | 294 | EUnif (ref NONE) => (Rabble, calls) |
294 end | 295 end |
295 | 296 |
296 fun doVali (i, (_, f, _, e), calls) = | 297 fun doVali (i, (_, f, _, e), calls) = |
297 let | 298 let |
299 case #1 e of | 300 case #1 e of |
300 EAbs (_, t, _, e) => | 301 EAbs (_, t, _, e) => |
301 unravel (e, j + 1, Arg (i, j, t) :: penv) | 302 unravel (e, j + 1, Arg (i, j, t) :: penv) |
302 | ECAbs (_, _, _, e) => | 303 | ECAbs (_, _, _, e) => |
303 unravel (e, j, penv) | 304 unravel (e, j, penv) |
304 | _ => (j, #2 (exp (penv, calls) e)) | 305 | _ => (j, #2 (exp f (penv, calls) e)) |
305 in | 306 in |
306 unravel (e, 0, []) | 307 unravel (e, 0, []) |
307 end | 308 end |
308 | 309 |
309 val (ns, calls) = ListUtil.foldliMap doVali [] vis | 310 val (ns, calls) = ListUtil.foldliMap doVali [] vis |
311 | |
312 fun isRecursive (from, to, _) = | |
313 let | |
314 fun search (at, soFar) = | |
315 at = from | |
316 orelse List.exists (fn (from', to', _) => | |
317 from' = at | |
318 andalso not (IS.member (soFar, to')) | |
319 andalso search (to', IS.add (soFar, to'))) | |
320 calls | |
321 in | |
322 search (to, IS.empty) | |
323 end | |
324 | |
325 val calls = List.filter isRecursive calls | |
310 | 326 |
311 fun search (ns, choices) = | 327 fun search (ns, choices) = |
312 case ns of | 328 case ns of |
313 [] => | 329 [] => |
314 let | 330 let |
315 val choices = rev choices | 331 val choices = rev choices |
316 in | 332 in |
317 List.all (fn (f, args) => | 333 List.all (fn (_, f, args) => |
318 let | 334 let |
319 val recArg = List.nth (choices, f) | 335 val recArg = List.nth (choices, f) |
320 | 336 |
321 fun isDatatype (t, _) = | 337 fun isDatatype (t, _) = |
322 case t of | 338 case t of |