Mercurial > urweb

annotate src/termination.sml @ 328:58f1260f293f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed a mind-numbing De Bruijn bug
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 19:59:31 -0400
parents a07f476d9b61
children 075b36dbb1a4
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@313 34
adamc@313 35 datatype pedigree =
adamc@313 36 Func of int
adamc@313 37 | Arg of int * int * con
adamc@313 38 | Subarg of int * int * con
adamc@313 39 | Rabble
adamc@313 40
adamc@313 41 fun p2s p =
adamc@313 42 case p of
adamc@313 43 Func i => "Func" ^ Int.toString i
adamc@313 44 | Arg (i, j, _) => "Arg" ^ Int.toString i ^ "," ^ Int.toString j
adamc@313 45 | Subarg (i, j, _) => "Subarg" ^ Int.toString i ^ "," ^ Int.toString j
adamc@313 46 | Rabble => "Rabble"
adamc@313 47
adamc@313 48 fun declOk' env (d, loc) =
adamc@313 49 case d of
adamc@313 50 DValRec vis =>
adamc@313 51 let
adamc@313 52 val nfns = length vis
adamc@313 53
adamc@313 54 val fenv = ListUtil.foldli (fn (i, (_, j, _, _), fenv) => IM.insert (fenv, j, i)) IM.empty vis
adamc@313 55
adamc@313 56 fun namesEq ((c1, _), (c2, _)) =
adamc@313 57 case (c1, c2) of
adamc@313 58 (CName s1, CName s2) => s1 = s2
adamc@313 59 | (CRel n1, CRel n2) => n1 = n2
adamc@313 60 | (CNamed n1, CNamed n2) => n1 = n2
adamc@313 61 | (CModProj n1, CModProj n2) => n1 = n2
adamc@313 62 | _ => false
adamc@313 63
adamc@313 64 fun patCon pc =
adamc@313 65 let
adamc@313 66 fun unravel (t, _) =
adamc@313 67 case t of
adamc@313 68 TCFun (_, _, _, t) => unravel t
adamc@313 69 | TFun (dom, _) => dom
adamc@313 70 | _ => raise Fail "Termination: Unexpected constructor type"
adamc@313 71 in
adamc@313 72 case pc of
adamc@313 73 PConVar i =>
adamc@313 74 let
adamc@313 75 val (_, t) = E.lookupENamed env i
adamc@313 76 in
adamc@313 77 unravel t
adamc@313 78 end
adamc@313 79 | PConProj (m1, ms, x) =>
adamc@313 80 let
adamc@313 81 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@313 82 in
adamc@313 83 case E.projectVal env {str = str, sgn = sgn, field = x} of
adamc@313 84 NONE => raise Fail "Termination: Bad constructor projection"
adamc@313 85 | SOME t => unravel t
adamc@313 86 end
adamc@313 87 end
adamc@313 88
adamc@313 89 fun pat penv (p, (pt, _)) =
adamc@313 90 let
adamc@313 91 fun con (i, j, pc, pt') = pat penv (Subarg (i, j, patCon pc), pt')
adamc@313 92
adamc@313 93 fun record (i, j, t, xps) =
adamc@313 94 case t of
adamc@313 95 (TRecord (CRecord (_, xts), _), _) =>
adamc@313 96 foldl (fn ((x, pt', _), penv) =>
adamc@313 97 let
adamc@313 98 val p' =
adamc@313 99 case List.find (fn (x', _) =>
adamc@313 100 namesEq ((CName x, ErrorMsg.dummySpan), x')) xts of
adamc@313 101 NONE => Rabble
adamc@313 102 | SOME (_, t) => Subarg (i, j, t)
adamc@313 103 in
adamc@313 104 pat penv (p', pt')
adamc@313 105 end) penv xps
adamc@313 106 | _ => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps
adamc@313 107 in
adamc@313 108 case (p, pt) of
adamc@313 109 (_, PWild) => penv
adamc@313 110 | (_, PVar _) => p :: penv
adamc@313 111 | (_, PPrim _) => penv
adamc@313 112 | (_, PCon (_, _, _, NONE)) => penv
adamc@313 113 | (Arg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt')
adamc@313 114 | (Subarg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt')
adamc@313 115 | (_, PCon (_, _, _, SOME pt')) => pat penv (Rabble, pt')
adamc@313 116 | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps)
adamc@313 117 | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps)
adamc@313 118 | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps
adamc@313 119 end
adamc@313 120
adamc@313 121 fun exp (penv, calls) e =
adamc@313 122 let
adamc@313 123 val default = (Rabble, calls)
adamc@313 124
adamc@313 125 fun apps () =
adamc@313 126 let
adamc@313 127 fun combiner calls e =
adamc@313 128 case #1 e of
adamc@314 129 EApp ((ECApp (
adamc@314 130 (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 (EModProj (m, [], "tag"), _),
adamc@314 138 _), _),
adamc@314 139 _), _),
adamc@314 140 _), _),
adamc@314 141 _), _),
adamc@314 142 _), _),
adamc@314 143 _), _),
adamc@314 144 _), _),
adamc@314 145 _), _),
adamc@314 146 (ERecord xets, _)) =>
adamc@314 147 let
adamc@314 148 val checkName =
adamc@314 149 case E.lookupStrNamed env m of
adamc@314 150 ("Basis", _) => (fn x : con => case #1 x of
adamc@314 151 CName s => s = "Link"
adamc@314 152 orelse s = "Action"
adamc@314 153 | _ => false)
adamc@314 154 | _ => (fn _ => false)
adamc@314 155
adamc@314 156 val calls = foldl (fn ((x, e, _), calls) =>
adamc@314 157 if checkName x then
adamc@314 158 calls
adamc@314 159 else
adamc@314 160 #2 (exp (penv, calls) e)) calls xets
adamc@314 161 in
adamc@314 162 (Rabble, [Rabble], calls)
adamc@314 163 end
adamc@314 164
adamc@314 165 | EApp (e1, e2) =>
adamc@313 166 let
adamc@313 167 val (p1, ps, calls) = combiner calls e1
adamc@313 168 val (p2, calls) = exp (penv, calls) e2
adamc@313 169
adamc@313 170 val p = case p1 of
adamc@313 171 Rabble => Rabble
adamc@313 172 | Arg _ => Rabble
adamc@313 173 | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran)
adamc@313 174 | Subarg _ => Rabble
adamc@313 175 | Func _ => Rabble
adamc@313 176 in
adamc@313 177 (p, ps @ [p2], calls)
adamc@313 178 end
adamc@313 179 | ECApp (e, _) =>
adamc@313 180 let
adamc@313 181 val (p, ps, calls) = combiner calls e
adamc@313 182
adamc@313 183 val p = case p of
adamc@313 184 Rabble => Rabble
adamc@313 185 | Arg _ => Rabble
adamc@313 186 | Subarg (i, j, (TCFun (_, _, _, ran), _)) => Subarg (i, j, ran)
adamc@313 187 | Subarg _ => Rabble
adamc@313 188 | Func _ => Rabble
adamc@313 189 in
adamc@313 190 (p, ps, calls)
adamc@313 191 end
adamc@313 192 | _ =>
adamc@313 193 let
adamc@313 194 val (p, calls) = exp (penv, calls) e
adamc@313 195 in
adamc@313 196 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)];
adamc@313 197 print (p2s p ^ "\n");*)
adamc@313 198 (p, [p], calls)
adamc@313 199 end
adamc@313 200
adamc@313 201 val (p, ps, calls) = combiner calls e
adamc@313 202
adamc@313 203 val calls =
adamc@313 204 case ps of
adamc@313 205 [] => raise Fail "Termination: Empty ps"
adamc@313 206 | f :: ps =>
adamc@313 207 case f of
adamc@313 208 Func i => (i, ps) :: calls
adamc@313 209 | _ => calls
adamc@313 210 in
adamc@313 211 (p, calls)
adamc@313 212 end
adamc@313 213 in
adamc@313 214 case #1 e of
adamc@313 215 EPrim _ => default
adamc@313 216 | ERel n => (List.nth (penv, n), calls)
adamc@313 217 | ENamed n =>
adamc@313 218 let
adamc@313 219 val p = case IM.find (fenv, n) of
adamc@313 220 NONE => Rabble
adamc@313 221 | SOME n' => Func n'
adamc@313 222 in
adamc@313 223 (p, calls)
adamc@313 224 end
adamc@313 225 | EModProj _ => default
adamc@314 226
adamc@313 227 | EApp _ => apps ()
adamc@313 228 | EAbs (_, _, _, e) =>
adamc@313 229 let
adamc@313 230 val (_, calls) = exp (Rabble :: penv, calls) e
adamc@313 231 in
adamc@313 232 (Rabble, calls)
adamc@313 233 end
adamc@313 234 | ECApp _ => apps ()
adamc@313 235 | ECAbs (_, _, _, e) =>
adamc@313 236 let
adamc@313 237 val (_, calls) = exp (penv, calls) e
adamc@313 238 in
adamc@313 239 (Rabble, calls)
adamc@313 240 end
adamc@313 241
adamc@313 242 | ERecord xets =>
adamc@313 243 let
adamc@313 244 val calls = foldl (fn ((_, e, _), calls) => #2 (exp (penv, calls) e)) calls xets
adamc@313 245 in
adamc@313 246 (Rabble, calls)
adamc@313 247 end
adamc@313 248 | EField (e, x, _) =>
adamc@313 249 let
adamc@313 250 val (p, calls) = exp (penv, calls) e
adamc@313 251 val p =
adamc@313 252 case p of
adamc@313 253 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) =>
adamc@313 254 (case List.find (fn (x', _) => namesEq (x, x')) xts of
adamc@313 255 NONE => Rabble
adamc@313 256 | SOME (_, t) => Subarg (i, j, t))
adamc@313 257 | _ => Rabble
adamc@313 258 in
adamc@313 259 (p, calls)
adamc@313 260 end
adamc@313 261 | ECut (e, _, _) =>
adamc@313 262 let
adamc@313 263 val (_, calls) = exp (penv, calls) e
adamc@313 264 in
adamc@313 265 (Rabble, calls)
adamc@313 266 end
adamc@313 267 | EFold _ => (Rabble, calls)
adamc@313 268
adamc@313 269 | ECase (e, pes, _) =>
adamc@313 270 let
adamc@313 271 val (p, calls) = exp (penv, calls) e
adamc@313 272
adamc@313 273 val calls = foldl (fn ((pt, e), calls) =>
adamc@313 274 let
adamc@313 275 val penv = pat penv (p, pt)
adamc@313 276 val (_, calls) = exp (penv, calls) e
adamc@313 277 in
adamc@313 278 calls
adamc@313 279 end) calls pes
adamc@313 280 in
adamc@313 281 (Rabble, calls)
adamc@313 282 end
adamc@313 283
adamc@313 284 | EError => (Rabble, calls)
adamc@313 285 | EUnif (ref (SOME e)) => exp (penv, calls) e
adamc@313 286 | EUnif (ref NONE) => (Rabble, calls)
adamc@313 287 end
adamc@313 288
adamc@313 289 fun doVali (i, (_, f, _, e), calls) =
adamc@313 290 let
adamc@313 291 fun unravel (e, j, penv) =
adamc@313 292 case #1 e of
adamc@313 293 EAbs (_, t, _, e) =>
adamc@313 294 unravel (e, j + 1, Arg (i, j, t) :: penv)
adamc@313 295 | ECAbs (_, _, _, e) =>
adamc@313 296 unravel (e, j, penv)
adamc@313 297 | _ => (j, #2 (exp (penv, calls) e))
adamc@313 298 in
adamc@313 299 unravel (e, 0, [])
adamc@313 300 end
adamc@313 301
adamc@313 302 val (ns, calls) = ListUtil.foldliMap doVali [] vis
adamc@313 303
adamc@313 304 fun search (ns, choices) =
adamc@313 305 case ns of
adamc@313 306 [] =>
adamc@313 307 let
adamc@313 308 val choices = rev choices
adamc@313 309 in
adamc@313 310 List.all (fn (f, args) =>
adamc@313 311 let
adamc@313 312 val recArg = List.nth (choices, f)
adamc@313 313
adamc@313 314 fun isDatatype (t, _) =
adamc@313 315 case t of
adamc@313 316 CNamed _ => true
adamc@313 317 | CModProj _ => true
adamc@313 318 | CApp (t, _) => isDatatype t
adamc@313 319 | _ => false
adamc@313 320 in
adamc@313 321 length args > recArg andalso
adamc@313 322 case List.nth (args, recArg) of
adamc@313 323 Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i)
adamc@313 324 | _ => false
adamc@313 325 end) calls
adamc@313 326 end
adamc@313 327 | n :: ns' =>
adamc@313 328 let
adamc@313 329 fun search' i =
adamc@313 330 i < n andalso (search (ns', i :: choices) orelse search' (i + 1))
adamc@313 331 in
adamc@313 332 search' 0
adamc@313 333 end
adamc@313 334 in
adamc@313 335 if search (ns, []) then
adamc@313 336 ()
adamc@313 337 else
adamc@313 338 ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)"
adamc@313 339 end
adamc@313 340
adamc@313 341 | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds)
adamc@313 342
adamc@313 343 | _ => ()
adamc@313 344
adamc@313 345 and declOk (d, env) =
adamc@313 346 (declOk' env d;
adamc@313 347 E.declBinds env d)
adamc@313 348
adamc@313 349 fun check ds = ignore (foldl declOk E.empty ds)
adamc@313 350
adamc@313 351 end