Mercurial > urweb

annotate src/termination.sml @ 1874:11d8e220f36f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add xhead type
author Sergey Mironov <grrwlf@gmail.com>
date Mon, 07 Oct 2013 14:07:31 +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