adamc@313
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@313
|
2 * All rights reserved.
|
adamc@313
|
3 *
|
adamc@313
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@313
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@313
|
6 *
|
adamc@313
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@313
|
8 * this list of conditions and the following disclaimer.
|
adamc@313
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@313
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@313
|
11 * and/or other materials provided with the distribution.
|
adamc@313
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@313
|
13 * derived from this software without specific prior written permission.
|
adamc@313
|
14 *
|
adamc@313
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@313
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@313
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@313
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@313
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@313
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@313
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@313
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@313
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@313
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@313
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@313
|
26 *)
|
adamc@313
|
27
|
adamc@313
|
28 structure Termination :> TERMINATION = struct
|
adamc@313
|
29
|
adamc@313
|
30 open Elab
|
adamc@313
|
31
|
adamc@313
|
32 structure E = ElabEnv
|
adamc@313
|
33 structure IM = IntBinaryMap
|
adamc@410
|
34 structure IS = IntBinarySet
|
adamc@313
|
35
|
adamc@313
|
36 datatype pedigree =
|
adamc@313
|
37 Func of int
|
adamc@313
|
38 | Arg of int * int * con
|
adamc@313
|
39 | Subarg of int * int * con
|
adamc@313
|
40 | Rabble
|
adamc@313
|
41
|
adamc@313
|
42 fun p2s p =
|
adamc@313
|
43 case p of
|
adamc@313
|
44 Func i => "Func" ^ Int.toString i
|
adamc@313
|
45 | Arg (i, j, _) => "Arg" ^ Int.toString i ^ "," ^ Int.toString j
|
adamc@313
|
46 | Subarg (i, j, _) => "Subarg" ^ Int.toString i ^ "," ^ Int.toString j
|
adamc@313
|
47 | Rabble => "Rabble"
|
adamc@313
|
48
|
adamc@313
|
49 fun declOk' env (d, loc) =
|
adamc@313
|
50 case d of
|
adamc@313
|
51 DValRec vis =>
|
adamc@313
|
52 let
|
adamc@313
|
53 val nfns = length vis
|
adamc@313
|
54
|
adamc@313
|
55 val fenv = ListUtil.foldli (fn (i, (_, j, _, _), fenv) => IM.insert (fenv, j, i)) IM.empty vis
|
adamc@313
|
56
|
adamc@313
|
57 fun namesEq ((c1, _), (c2, _)) =
|
adamc@313
|
58 case (c1, c2) of
|
adamc@313
|
59 (CName s1, CName s2) => s1 = s2
|
adamc@313
|
60 | (CRel n1, CRel n2) => n1 = n2
|
adamc@313
|
61 | (CNamed n1, CNamed n2) => n1 = n2
|
adamc@313
|
62 | (CModProj n1, CModProj n2) => n1 = n2
|
adamc@313
|
63 | _ => false
|
adamc@313
|
64
|
adamc@313
|
65 fun patCon pc =
|
adamc@313
|
66 let
|
adamc@313
|
67 fun unravel (t, _) =
|
adamc@313
|
68 case t of
|
adamc@313
|
69 TCFun (_, _, _, t) => unravel t
|
adamc@313
|
70 | TFun (dom, _) => dom
|
adamc@313
|
71 | _ => raise Fail "Termination: Unexpected constructor type"
|
adamc@313
|
72 in
|
adamc@313
|
73 case pc of
|
adamc@313
|
74 PConVar i =>
|
adamc@313
|
75 let
|
adamc@313
|
76 val (_, t) = E.lookupENamed env i
|
adamc@313
|
77 in
|
adamc@313
|
78 unravel t
|
adamc@313
|
79 end
|
adamc@313
|
80 | PConProj (m1, ms, x) =>
|
adamc@313
|
81 let
|
adamc@313
|
82 val (str, sgn) = E.chaseMpath env (m1, ms)
|
adamc@313
|
83 in
|
adamc@313
|
84 case E.projectVal env {str = str, sgn = sgn, field = x} of
|
adamc@313
|
85 NONE => raise Fail "Termination: Bad constructor projection"
|
adamc@313
|
86 | SOME t => unravel t
|
adamc@313
|
87 end
|
adamc@313
|
88 end
|
adamc@313
|
89
|
adamc@313
|
90 fun pat penv (p, (pt, _)) =
|
adamc@313
|
91 let
|
adamc@313
|
92 fun con (i, j, pc, pt') = pat penv (Subarg (i, j, patCon pc), pt')
|
adamc@313
|
93
|
adamc@313
|
94 fun record (i, j, t, xps) =
|
adamc@313
|
95 case t of
|
adamc@313
|
96 (TRecord (CRecord (_, xts), _), _) =>
|
adamc@313
|
97 foldl (fn ((x, pt', _), penv) =>
|
adamc@313
|
98 let
|
adamc@313
|
99 val p' =
|
adamc@313
|
100 case List.find (fn (x', _) =>
|
adamc@313
|
101 namesEq ((CName x, ErrorMsg.dummySpan), x')) xts of
|
adamc@313
|
102 NONE => Rabble
|
adamc@313
|
103 | SOME (_, t) => Subarg (i, j, t)
|
adamc@313
|
104 in
|
adamc@313
|
105 pat penv (p', pt')
|
adamc@313
|
106 end) penv xps
|
adamc@313
|
107 | _ => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps
|
adamc@313
|
108 in
|
adamc@313
|
109 case (p, pt) of
|
adamc@313
|
110 (_, PWild) => penv
|
adamc@313
|
111 | (_, PVar _) => p :: penv
|
adamc@313
|
112 | (_, PPrim _) => penv
|
adamc@313
|
113 | (_, PCon (_, _, _, NONE)) => penv
|
adamc@313
|
114 | (Arg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt')
|
adamc@313
|
115 | (Subarg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt')
|
adamc@313
|
116 | (_, PCon (_, _, _, SOME pt')) => pat penv (Rabble, pt')
|
adamc@313
|
117 | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps)
|
adamc@313
|
118 | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps)
|
adamc@313
|
119 | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps
|
adamc@313
|
120 end
|
adamc@313
|
121
|
adamc@410
|
122 fun exp parent (penv, calls) e =
|
adamc@313
|
123 let
|
adamc@313
|
124 val default = (Rabble, calls)
|
adamc@313
|
125
|
adamc@313
|
126 fun apps () =
|
adamc@313
|
127 let
|
adamc@313
|
128 fun combiner calls e =
|
adamc@313
|
129 case #1 e of
|
adamc@314
|
130 EApp ((ECApp (
|
adamc@314
|
131 (ECApp (
|
adamc@314
|
132 (ECApp (
|
adamc@314
|
133 (ECApp (
|
adamc@314
|
134 (ECApp (
|
adamc@314
|
135 (ECApp (
|
adamc@314
|
136 (ECApp (
|
adamc@314
|
137 (ECApp (
|
adamc@314
|
138 (EModProj (m, [], "tag"), _),
|
adamc@314
|
139 _), _),
|
adamc@314
|
140 _), _),
|
adamc@314
|
141 _), _),
|
adamc@314
|
142 _), _),
|
adamc@314
|
143 _), _),
|
adamc@314
|
144 _), _),
|
adamc@314
|
145 _), _),
|
adamc@314
|
146 _), _),
|
adamc@314
|
147 (ERecord xets, _)) =>
|
adamc@314
|
148 let
|
adamc@314
|
149 val checkName =
|
adamc@314
|
150 case E.lookupStrNamed env m of
|
adamc@314
|
151 ("Basis", _) => (fn x : con => case #1 x of
|
adamc@314
|
152 CName s => s = "Link"
|
adamc@314
|
153 orelse s = "Action"
|
adamc@314
|
154 | _ => false)
|
adamc@314
|
155 | _ => (fn _ => false)
|
adamc@314
|
156
|
adamc@314
|
157 val calls = foldl (fn ((x, e, _), calls) =>
|
adamc@314
|
158 if checkName x then
|
adamc@314
|
159 calls
|
adamc@314
|
160 else
|
adamc@410
|
161 #2 (exp parent (penv, calls) e)) calls xets
|
adamc@314
|
162 in
|
adamc@314
|
163 (Rabble, [Rabble], calls)
|
adamc@314
|
164 end
|
adamc@314
|
165
|
adamc@314
|
166 | EApp (e1, e2) =>
|
adamc@313
|
167 let
|
adamc@313
|
168 val (p1, ps, calls) = combiner calls e1
|
adamc@410
|
169 val (p2, calls) = exp parent (penv, calls) e2
|
adamc@313
|
170
|
adamc@313
|
171 val p = case p1 of
|
adamc@313
|
172 Rabble => Rabble
|
adamc@313
|
173 | Arg _ => Rabble
|
adamc@313
|
174 | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran)
|
adamc@313
|
175 | Subarg _ => Rabble
|
adamc@313
|
176 | Func _ => Rabble
|
adamc@313
|
177 in
|
adamc@313
|
178 (p, ps @ [p2], calls)
|
adamc@313
|
179 end
|
adamc@313
|
180 | ECApp (e, _) =>
|
adamc@313
|
181 let
|
adamc@313
|
182 val (p, ps, calls) = combiner calls e
|
adamc@313
|
183
|
adamc@313
|
184 val p = case p of
|
adamc@313
|
185 Rabble => Rabble
|
adamc@313
|
186 | Arg _ => Rabble
|
adamc@313
|
187 | Subarg (i, j, (TCFun (_, _, _, ran), _)) => Subarg (i, j, ran)
|
adamc@313
|
188 | Subarg _ => Rabble
|
adamc@313
|
189 | Func _ => Rabble
|
adamc@313
|
190 in
|
adamc@313
|
191 (p, ps, calls)
|
adamc@313
|
192 end
|
adamc@313
|
193 | _ =>
|
adamc@313
|
194 let
|
adamc@410
|
195 val (p, calls) = exp parent (penv, calls) e
|
adamc@313
|
196 in
|
adamc@313
|
197 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)];
|
adamc@313
|
198 print (p2s p ^ "\n");*)
|
adamc@313
|
199 (p, [p], calls)
|
adamc@313
|
200 end
|
adamc@313
|
201
|
adamc@313
|
202 val (p, ps, calls) = combiner calls e
|
adamc@313
|
203
|
adamc@313
|
204 val calls =
|
adamc@313
|
205 case ps of
|
adamc@313
|
206 [] => raise Fail "Termination: Empty ps"
|
adamc@313
|
207 | f :: ps =>
|
adamc@313
|
208 case f of
|
adamc@410
|
209 Func i => (parent, i, ps) :: calls
|
adamc@313
|
210 | _ => calls
|
adamc@313
|
211 in
|
adamc@313
|
212 (p, calls)
|
adamc@313
|
213 end
|
adamc@313
|
214 in
|
adamc@313
|
215 case #1 e of
|
adamc@313
|
216 EPrim _ => default
|
adamc@313
|
217 | ERel n => (List.nth (penv, n), calls)
|
adamc@313
|
218 | ENamed n =>
|
adamc@313
|
219 let
|
adamc@313
|
220 val p = case IM.find (fenv, n) of
|
adamc@313
|
221 NONE => Rabble
|
adamc@313
|
222 | SOME n' => Func n'
|
adamc@313
|
223 in
|
adamc@313
|
224 (p, calls)
|
adamc@313
|
225 end
|
adamc@313
|
226 | EModProj _ => default
|
adamc@314
|
227
|
adamc@313
|
228 | EApp _ => apps ()
|
adamc@313
|
229 | EAbs (_, _, _, e) =>
|
adamc@313
|
230 let
|
adamc@410
|
231 val (_, calls) = exp parent (Rabble :: penv, calls) e
|
adamc@313
|
232 in
|
adamc@313
|
233 (Rabble, calls)
|
adamc@313
|
234 end
|
adamc@313
|
235 | ECApp _ => apps ()
|
adamc@313
|
236 | ECAbs (_, _, _, e) =>
|
adamc@313
|
237 let
|
adamc@410
|
238 val (_, calls) = exp parent (penv, calls) e
|
adamc@313
|
239 in
|
adamc@313
|
240 (Rabble, calls)
|
adamc@313
|
241 end
|
adamc@313
|
242
|
adamc@313
|
243 | ERecord xets =>
|
adamc@313
|
244 let
|
adamc@410
|
245 val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets
|
adamc@313
|
246 in
|
adamc@313
|
247 (Rabble, calls)
|
adamc@313
|
248 end
|
adamc@313
|
249 | EField (e, x, _) =>
|
adamc@313
|
250 let
|
adamc@410
|
251 val (p, calls) = exp parent (penv, calls) e
|
adamc@313
|
252 val p =
|
adamc@313
|
253 case p of
|
adamc@313
|
254 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) =>
|
adamc@313
|
255 (case List.find (fn (x', _) => namesEq (x, x')) xts of
|
adamc@313
|
256 NONE => Rabble
|
adamc@313
|
257 | SOME (_, t) => Subarg (i, j, t))
|
adamc@313
|
258 | _ => Rabble
|
adamc@313
|
259 in
|
adamc@313
|
260 (p, calls)
|
adamc@313
|
261 end
|
adamc@313
|
262 | ECut (e, _, _) =>
|
adamc@313
|
263 let
|
adamc@410
|
264 val (_, calls) = exp parent (penv, calls) e
|
adamc@313
|
265 in
|
adamc@313
|
266 (Rabble, calls)
|
adamc@313
|
267 end
|
adamc@493
|
268 | ECutMulti (e, _, _) =>
|
adamc@493
|
269 let
|
adamc@493
|
270 val (_, calls) = exp parent (penv, calls) e
|
adamc@493
|
271 in
|
adamc@493
|
272 (Rabble, calls)
|
adamc@493
|
273 end
|
adamc@445
|
274 | EConcat (e1, _, e2, _) =>
|
adamc@339
|
275 let
|
adamc@410
|
276 val (_, calls) = exp parent (penv, calls) e1
|
adamc@410
|
277 val (_, calls) = exp parent (penv, calls) e2
|
adamc@339
|
278 in
|
adamc@339
|
279 (Rabble, calls)
|
adamc@339
|
280 end
|
adamc@313
|
281 | EFold _ => (Rabble, calls)
|
adamc@313
|
282
|
adamc@313
|
283 | ECase (e, pes, _) =>
|
adamc@313
|
284 let
|
adamc@410
|
285 val (p, calls) = exp parent (penv, calls) e
|
adamc@313
|
286
|
adamc@313
|
287 val calls = foldl (fn ((pt, e), calls) =>
|
adamc@313
|
288 let
|
adamc@313
|
289 val penv = pat penv (p, pt)
|
adamc@410
|
290 val (_, calls) = exp parent (penv, calls) e
|
adamc@313
|
291 in
|
adamc@313
|
292 calls
|
adamc@313
|
293 end) calls pes
|
adamc@313
|
294 in
|
adamc@313
|
295 (Rabble, calls)
|
adamc@313
|
296 end
|
adamc@313
|
297
|
adamc@313
|
298 | EError => (Rabble, calls)
|
adamc@410
|
299 | EUnif (ref (SOME e)) => exp parent (penv, calls) e
|
adamc@313
|
300 | EUnif (ref NONE) => (Rabble, calls)
|
adamc@448
|
301
|
adamc@453
|
302 | ELet (eds, e) =>
|
adamc@453
|
303 let
|
adamc@453
|
304 fun extPenv ((ed, _), penv) =
|
adamc@453
|
305 case ed of
|
adamc@453
|
306 EDVal _ => Rabble :: penv
|
adamc@453
|
307 | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis
|
adamc@453
|
308 in
|
adamc@453
|
309 exp parent (foldl extPenv penv eds, calls) e
|
adamc@453
|
310 end
|
adamc@313
|
311 end
|
adamc@313
|
312
|
adamc@313
|
313 fun doVali (i, (_, f, _, e), calls) =
|
adamc@313
|
314 let
|
adamc@313
|
315 fun unravel (e, j, penv) =
|
adamc@313
|
316 case #1 e of
|
adamc@313
|
317 EAbs (_, t, _, e) =>
|
adamc@313
|
318 unravel (e, j + 1, Arg (i, j, t) :: penv)
|
adamc@313
|
319 | ECAbs (_, _, _, e) =>
|
adamc@313
|
320 unravel (e, j, penv)
|
adamc@410
|
321 | _ => (j, #2 (exp f (penv, calls) e))
|
adamc@313
|
322 in
|
adamc@313
|
323 unravel (e, 0, [])
|
adamc@313
|
324 end
|
adamc@313
|
325
|
adamc@313
|
326 val (ns, calls) = ListUtil.foldliMap doVali [] vis
|
adamc@313
|
327
|
adamc@410
|
328 fun isRecursive (from, to, _) =
|
adamc@410
|
329 let
|
adamc@410
|
330 fun search (at, soFar) =
|
adamc@410
|
331 at = from
|
adamc@410
|
332 orelse List.exists (fn (from', to', _) =>
|
adamc@410
|
333 from' = at
|
adamc@410
|
334 andalso not (IS.member (soFar, to'))
|
adamc@410
|
335 andalso search (to', IS.add (soFar, to')))
|
adamc@410
|
336 calls
|
adamc@410
|
337 in
|
adamc@410
|
338 search (to, IS.empty)
|
adamc@410
|
339 end
|
adamc@410
|
340
|
adamc@410
|
341 val calls = List.filter isRecursive calls
|
adamc@410
|
342
|
adamc@313
|
343 fun search (ns, choices) =
|
adamc@313
|
344 case ns of
|
adamc@313
|
345 [] =>
|
adamc@313
|
346 let
|
adamc@313
|
347 val choices = rev choices
|
adamc@313
|
348 in
|
adamc@410
|
349 List.all (fn (_, f, args) =>
|
adamc@313
|
350 let
|
adamc@313
|
351 val recArg = List.nth (choices, f)
|
adamc@313
|
352
|
adamc@313
|
353 fun isDatatype (t, _) =
|
adamc@313
|
354 case t of
|
adamc@313
|
355 CNamed _ => true
|
adamc@313
|
356 | CModProj _ => true
|
adamc@313
|
357 | CApp (t, _) => isDatatype t
|
adamc@313
|
358 | _ => false
|
adamc@313
|
359 in
|
adamc@313
|
360 length args > recArg andalso
|
adamc@313
|
361 case List.nth (args, recArg) of
|
adamc@313
|
362 Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i)
|
adamc@313
|
363 | _ => false
|
adamc@313
|
364 end) calls
|
adamc@313
|
365 end
|
adamc@313
|
366 | n :: ns' =>
|
adamc@313
|
367 let
|
adamc@313
|
368 fun search' i =
|
adamc@313
|
369 i < n andalso (search (ns', i :: choices) orelse search' (i + 1))
|
adamc@313
|
370 in
|
adamc@313
|
371 search' 0
|
adamc@313
|
372 end
|
adamc@313
|
373 in
|
adamc@313
|
374 if search (ns, []) then
|
adamc@313
|
375 ()
|
adamc@313
|
376 else
|
adamc@313
|
377 ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)"
|
adamc@313
|
378 end
|
adamc@313
|
379
|
adamc@313
|
380 | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds)
|
adamc@313
|
381
|
adamc@313
|
382 | _ => ()
|
adamc@313
|
383
|
adamc@313
|
384 and declOk (d, env) =
|
adamc@313
|
385 (declOk' env d;
|
adamc@313
|
386 E.declBinds env d)
|
adamc@313
|
387
|
adamc@313
|
388 fun check ds = ignore (foldl declOk E.empty ds)
|
adamc@313
|
389
|
adamc@313
|
390 end
|