Mercurial > urweb

annotate src/termination.sml @ 416:679b2fbbd4d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Counter demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 11:59:48 -0400
parents c5a3d223f157
children dfc8c991abd0
rev   line source
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@339 268 | EWith (e1, _, e2, _) =>
adamc@339 269 let
adamc@410 270 val (_, calls) = exp parent (penv, calls) e1
adamc@410 271 val (_, calls) = exp parent (penv, calls) e2
adamc@339 272 in
adamc@339 273 (Rabble, calls)
adamc@339 274 end
adamc@313 275 | EFold _ => (Rabble, calls)
adamc@313 276
adamc@313 277 | ECase (e, pes, _) =>
adamc@313 278 let
adamc@410 279 val (p, calls) = exp parent (penv, calls) e
adamc@313 280
adamc@313 281 val calls = foldl (fn ((pt, e), calls) =>
adamc@313 282 let
adamc@313 283 val penv = pat penv (p, pt)
adamc@410 284 val (_, calls) = exp parent (penv, calls) e
adamc@313 285 in
adamc@313 286 calls
adamc@313 287 end) calls pes
adamc@313 288 in
adamc@313 289 (Rabble, calls)
adamc@313 290 end
adamc@313 291
adamc@313 292 | EError => (Rabble, calls)
adamc@410 293 | EUnif (ref (SOME e)) => exp parent (penv, calls) e
adamc@313 294 | EUnif (ref NONE) => (Rabble, calls)
adamc@313 295 end
adamc@313 296
adamc@313 297 fun doVali (i, (_, f, _, e), calls) =
adamc@313 298 let
adamc@313 299 fun unravel (e, j, penv) =
adamc@313 300 case #1 e of
adamc@313 301 EAbs (_, t, _, e) =>
adamc@313 302 unravel (e, j + 1, Arg (i, j, t) :: penv)
adamc@313 303 | ECAbs (_, _, _, e) =>
adamc@313 304 unravel (e, j, penv)
adamc@410 305 | _ => (j, #2 (exp f (penv, calls) e))
adamc@313 306 in
adamc@313 307 unravel (e, 0, [])
adamc@313 308 end
adamc@313 309
adamc@313 310 val (ns, calls) = ListUtil.foldliMap doVali [] vis
adamc@313 311
adamc@410 312 fun isRecursive (from, to, _) =
adamc@410 313 let
adamc@410 314 fun search (at, soFar) =
adamc@410 315 at = from
adamc@410 316 orelse List.exists (fn (from', to', _) =>
adamc@410 317 from' = at
adamc@410 318 andalso not (IS.member (soFar, to'))
adamc@410 319 andalso search (to', IS.add (soFar, to')))
adamc@410 320 calls
adamc@410 321 in
adamc@410 322 search (to, IS.empty)
adamc@410 323 end
adamc@410 324
adamc@410 325 val calls = List.filter isRecursive calls
adamc@410 326
adamc@313 327 fun search (ns, choices) =
adamc@313 328 case ns of
adamc@313 329 [] =>
adamc@313 330 let
adamc@313 331 val choices = rev choices
adamc@313 332 in
adamc@410 333 List.all (fn (_, f, args) =>
adamc@313 334 let
adamc@313 335 val recArg = List.nth (choices, f)
adamc@313 336
adamc@313 337 fun isDatatype (t, _) =
adamc@313 338 case t of
adamc@313 339 CNamed _ => true
adamc@313 340 | CModProj _ => true
adamc@313 341 | CApp (t, _) => isDatatype t
adamc@313 342 | _ => false
adamc@313 343 in
adamc@313 344 length args > recArg andalso
adamc@313 345 case List.nth (args, recArg) of
adamc@313 346 Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i)
adamc@313 347 | _ => false
adamc@313 348 end) calls
adamc@313 349 end
adamc@313 350 | n :: ns' =>
adamc@313 351 let
adamc@313 352 fun search' i =
adamc@313 353 i < n andalso (search (ns', i :: choices) orelse search' (i + 1))
adamc@313 354 in
adamc@313 355 search' 0
adamc@313 356 end
adamc@313 357 in
adamc@313 358 if search (ns, []) then
adamc@313 359 ()
adamc@313 360 else
adamc@313 361 ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)"
adamc@313 362 end
adamc@313 363
adamc@313 364 | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds)
adamc@313 365
adamc@313 366 | _ => ()
adamc@313 367
adamc@313 368 and declOk (d, env) =
adamc@313 369 (declOk' env d;
adamc@313 370 E.declBinds env d)
adamc@313 371
adamc@313 372 fun check ds = ignore (foldl declOk E.empty ds)
adamc@313 373
adamc@313 374 end