Mercurial > urweb

annotate src/termination.sml @ 2258:b1ba35ce2613

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug where pure caching didn't treat FFI applications as effectful.
author Ziv Scully <ziv@mit.edu>
date Sun, 27 Sep 2015 17:02:14 -0400
parents 7f871c03e3a1
children
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@623 193 | EKApp (e, _) => combiner calls e
adamc@313 194 | _ =>
adamc@313 195 let
adamc@410 196 val (p, calls) = exp parent (penv, calls) e
adamc@313 197 in
adamc@313 198 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)];
adamc@313 199 print (p2s p ^ "\n");*)
adamc@313 200 (p, [p], calls)
adamc@313 201 end
adamc@313 202
adamc@313 203 val (p, ps, calls) = combiner calls e
adamc@313 204
adamc@313 205 val calls =
adamc@313 206 case ps of
adamc@313 207 [] => raise Fail "Termination: Empty ps"
adamc@313 208 | f :: ps =>
adamc@313 209 case f of
adamc@410 210 Func i => (parent, i, ps) :: calls
adamc@313 211 | _ => calls
adamc@313 212 in
adamc@313 213 (p, calls)
adamc@313 214 end
adamc@313 215 in
adamc@313 216 case #1 e of
adamc@313 217 EPrim _ => default
adamc@313 218 | ERel n => (List.nth (penv, n), calls)
adamc@313 219 | ENamed n =>
adamc@313 220 let
adamc@313 221 val p = case IM.find (fenv, n) of
adamc@313 222 NONE => Rabble
adamc@313 223 | SOME n' => Func n'
adamc@313 224 in
adamc@313 225 (p, calls)
adamc@313 226 end
adamc@313 227 | EModProj _ => default
adamc@314 228
adamc@313 229 | EApp _ => apps ()
adamc@313 230 | EAbs (_, _, _, e) =>
adamc@313 231 let
adamc@410 232 val (_, calls) = exp parent (Rabble :: penv, calls) e
adamc@313 233 in
adamc@313 234 (Rabble, calls)
adamc@313 235 end
adamc@313 236 | ECApp _ => apps ()
adamc@313 237 | ECAbs (_, _, _, e) =>
adamc@313 238 let
adamc@410 239 val (_, calls) = exp parent (penv, calls) e
adamc@313 240 in
adamc@313 241 (Rabble, calls)
adamc@313 242 end
adamc@623 243 | EKApp _ => apps ()
adamc@623 244 | EKAbs (_, e) =>
adamc@623 245 let
adamc@623 246 val (_, calls) = exp parent (penv, calls) e
adamc@623 247 in
adamc@623 248 (Rabble, calls)
adamc@623 249 end
adamc@313 250
adamc@313 251 | ERecord xets =>
adamc@313 252 let
adamc@410 253 val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets
adamc@313 254 in
adamc@313 255 (Rabble, calls)
adamc@313 256 end
adamc@313 257 | EField (e, x, _) =>
adamc@313 258 let
adamc@410 259 val (p, calls) = exp parent (penv, calls) e
adamc@313 260 val p =
adamc@313 261 case p of
adamc@313 262 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) =>
adamc@313 263 (case List.find (fn (x', _) => namesEq (x, x')) xts of
adamc@313 264 NONE => Rabble
adamc@313 265 | SOME (_, t) => Subarg (i, j, t))
adamc@313 266 | _ => Rabble
adamc@313 267 in
adamc@313 268 (p, calls)
adamc@313 269 end
adamc@313 270 | ECut (e, _, _) =>
adamc@313 271 let
adamc@410 272 val (_, calls) = exp parent (penv, calls) e
adamc@313 273 in
adamc@313 274 (Rabble, calls)
adamc@313 275 end
adamc@493 276 | ECutMulti (e, _, _) =>
adamc@493 277 let
adamc@493 278 val (_, calls) = exp parent (penv, calls) e
adamc@493 279 in
adamc@493 280 (Rabble, calls)
adamc@493 281 end
adamc@445 282 | EConcat (e1, _, e2, _) =>
adamc@339 283 let
adamc@410 284 val (_, calls) = exp parent (penv, calls) e1
adamc@410 285 val (_, calls) = exp parent (penv, calls) e2
adamc@339 286 in
adamc@339 287 (Rabble, calls)
adamc@339 288 end
adamc@313 289
adamc@313 290 | ECase (e, pes, _) =>
adamc@313 291 let
adamc@410 292 val (p, calls) = exp parent (penv, calls) e
adamc@313 293
adamc@313 294 val calls = foldl (fn ((pt, e), calls) =>
adamc@313 295 let
adamc@313 296 val penv = pat penv (p, pt)
adamc@410 297 val (_, calls) = exp parent (penv, calls) e
adamc@313 298 in
adamc@313 299 calls
adamc@313 300 end) calls pes
adamc@313 301 in
adamc@313 302 (Rabble, calls)
adamc@313 303 end
adamc@313 304
adamc@313 305 | EError => (Rabble, calls)
adamc@410 306 | EUnif (ref (SOME e)) => exp parent (penv, calls) e
adamc@313 307 | EUnif (ref NONE) => (Rabble, calls)
adamc@448 308
adamc@825 309 | ELet (eds, e, _) =>
adamc@453 310 let
adamc@453 311 fun extPenv ((ed, _), penv) =
adamc@453 312 case ed of
adamc@453 313 EDVal _ => Rabble :: penv
adamc@453 314 | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis
adamc@453 315 in
adamc@453 316 exp parent (foldl extPenv penv eds, calls) e
adamc@453 317 end
adamc@313 318 end
adamc@313 319
adamc@313 320 fun doVali (i, (_, f, _, e), calls) =
adamc@313 321 let
adamc@313 322 fun unravel (e, j, penv) =
adamc@313 323 case #1 e of
adamc@313 324 EAbs (_, t, _, e) =>
adamc@313 325 unravel (e, j + 1, Arg (i, j, t) :: penv)
adamc@313 326 | ECAbs (_, _, _, e) =>
adamc@313 327 unravel (e, j, penv)
adamc@410 328 | _ => (j, #2 (exp f (penv, calls) e))
adamc@313 329 in
adamc@313 330 unravel (e, 0, [])
adamc@313 331 end
adamc@313 332
adamc@313 333 val (ns, calls) = ListUtil.foldliMap doVali [] vis
adamc@313 334
adamc@410 335 fun isRecursive (from, to, _) =
adamc@410 336 let
adamc@410 337 fun search (at, soFar) =
adamc@410 338 at = from
adamc@410 339 orelse List.exists (fn (from', to', _) =>
adamc@410 340 from' = at
adamc@410 341 andalso not (IS.member (soFar, to'))
adamc@410 342 andalso search (to', IS.add (soFar, to')))
adamc@410 343 calls
adamc@410 344 in
adamc@410 345 search (to, IS.empty)
adamc@410 346 end
adamc@410 347
adamc@410 348 val calls = List.filter isRecursive calls
adamc@410 349
adamc@313 350 fun search (ns, choices) =
adamc@313 351 case ns of
adamc@313 352 [] =>
adamc@313 353 let
adamc@313 354 val choices = rev choices
adamc@313 355 in
adamc@410 356 List.all (fn (_, f, args) =>
adamc@313 357 let
adamc@313 358 val recArg = List.nth (choices, f)
adamc@313 359
adamc@313 360 fun isDatatype (t, _) =
adamc@313 361 case t of
adamc@313 362 CNamed _ => true
adamc@313 363 | CModProj _ => true
adamc@313 364 | CApp (t, _) => isDatatype t
adamc@313 365 | _ => false
adamc@313 366 in
adamc@313 367 length args > recArg andalso
adamc@313 368 case List.nth (args, recArg) of
adamc@313 369 Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i)
adamc@313 370 | _ => false
adamc@313 371 end) calls
adamc@313 372 end
adamc@313 373 | n :: ns' =>
adamc@313 374 let
adamc@313 375 fun search' i =
adamc@313 376 i < n andalso (search (ns', i :: choices) orelse search' (i + 1))
adamc@313 377 in
adamc@313 378 search' 0
adamc@313 379 end
adamc@313 380 in
adamc@313 381 if search (ns, []) then
adamc@313 382 ()
adamc@313 383 else
adamc@313 384 ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)"
adamc@313 385 end
adamc@313 386
adamc@313 387 | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds)
adamc@313 388
adamc@313 389 | _ => ()
adamc@313 390
adamc@313 391 and declOk (d, env) =
adamc@313 392 (declOk' env d;
adamc@313 393 E.declBinds env d)
adamc@313 394
adamc@313 395 fun check ds = ignore (foldl declOk E.empty ds)
adamc@313 396
adamc@313 397 end