Mercurial > urweb

comparison src/termination.sml @ 313:e0ed0d4dabc9

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