Mercurial > urweb

comparison src/termination.sml @ 410:c5a3d223f157

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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