Mercurial > urweb

annotate 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
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@313 129 EApp (e1, e2) =>
adamc@313 130 let
adamc@313 131 val (p1, ps, calls) = combiner calls e1
adamc@313 132 val (p2, calls) = exp (penv, calls) e2
adamc@313 133
adamc@313 134 val p = case p1 of
adamc@313 135 Rabble => Rabble
adamc@313 136 | Arg _ => Rabble
adamc@313 137 | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran)
adamc@313 138 | Subarg _ => Rabble
adamc@313 139 | Func _ => Rabble
adamc@313 140 in
adamc@313 141 (p, ps @ [p2], calls)
adamc@313 142 end
adamc@313 143 | ECApp (e, _) =>
adamc@313 144 let
adamc@313 145 val (p, ps, calls) = combiner calls e
adamc@313 146
adamc@313 147 val p = case p of
adamc@313 148 Rabble => Rabble
adamc@313 149 | Arg _ => Rabble
adamc@313 150 | Subarg (i, j, (TCFun (_, _, _, ran), _)) => Subarg (i, j, ran)
adamc@313 151 | Subarg _ => Rabble
adamc@313 152 | Func _ => Rabble
adamc@313 153 in
adamc@313 154 (p, ps, calls)
adamc@313 155 end
adamc@313 156 | _ =>
adamc@313 157 let
adamc@313 158 val (p, calls) = exp (penv, calls) e
adamc@313 159 in
adamc@313 160 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)];
adamc@313 161 print (p2s p ^ "\n");*)
adamc@313 162 (p, [p], calls)
adamc@313 163 end
adamc@313 164
adamc@313 165 val (p, ps, calls) = combiner calls e
adamc@313 166
adamc@313 167 val calls =
adamc@313 168 case ps of
adamc@313 169 [] => raise Fail "Termination: Empty ps"
adamc@313 170 | f :: ps =>
adamc@313 171 case f of
adamc@313 172 Func i => (i, ps) :: calls
adamc@313 173 | _ => calls
adamc@313 174 in
adamc@313 175 (p, calls)
adamc@313 176 end
adamc@313 177 in
adamc@313 178 case #1 e of
adamc@313 179 EPrim _ => default
adamc@313 180 | ERel n => (List.nth (penv, n), calls)
adamc@313 181 | ENamed n =>
adamc@313 182 let
adamc@313 183 val p = case IM.find (fenv, n) of
adamc@313 184 NONE => Rabble
adamc@313 185 | SOME n' => Func n'
adamc@313 186 in
adamc@313 187 (p, calls)
adamc@313 188 end
adamc@313 189 | EModProj _ => default
adamc@313 190 | EApp _ => apps ()
adamc@313 191 | EAbs (_, _, _, e) =>
adamc@313 192 let
adamc@313 193 val (_, calls) = exp (Rabble :: penv, calls) e
adamc@313 194 in
adamc@313 195 (Rabble, calls)
adamc@313 196 end
adamc@313 197 | ECApp _ => apps ()
adamc@313 198 | ECAbs (_, _, _, e) =>
adamc@313 199 let
adamc@313 200 val (_, calls) = exp (penv, calls) e
adamc@313 201 in
adamc@313 202 (Rabble, calls)
adamc@313 203 end
adamc@313 204
adamc@313 205 | ERecord xets =>
adamc@313 206 let
adamc@313 207 val calls = foldl (fn ((_, e, _), calls) => #2 (exp (penv, calls) e)) calls xets
adamc@313 208 in
adamc@313 209 (Rabble, calls)
adamc@313 210 end
adamc@313 211 | EField (e, x, _) =>
adamc@313 212 let
adamc@313 213 val (p, calls) = exp (penv, calls) e
adamc@313 214 val p =
adamc@313 215 case p of
adamc@313 216 Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) =>
adamc@313 217 (case List.find (fn (x', _) => namesEq (x, x')) xts of
adamc@313 218 NONE => Rabble
adamc@313 219 | SOME (_, t) => Subarg (i, j, t))
adamc@313 220 | _ => Rabble
adamc@313 221 in
adamc@313 222 (p, calls)
adamc@313 223 end
adamc@313 224 | ECut (e, _, _) =>
adamc@313 225 let
adamc@313 226 val (_, calls) = exp (penv, calls) e
adamc@313 227 in
adamc@313 228 (Rabble, calls)
adamc@313 229 end
adamc@313 230 | EFold _ => (Rabble, calls)
adamc@313 231
adamc@313 232 | ECase (e, pes, _) =>
adamc@313 233 let
adamc@313 234 val (p, calls) = exp (penv, calls) e
adamc@313 235
adamc@313 236 val calls = foldl (fn ((pt, e), calls) =>
adamc@313 237 let
adamc@313 238 val penv = pat penv (p, pt)
adamc@313 239 val (_, calls) = exp (penv, calls) e
adamc@313 240 in
adamc@313 241 calls
adamc@313 242 end) calls pes
adamc@313 243 in
adamc@313 244 (Rabble, calls)
adamc@313 245 end
adamc@313 246
adamc@313 247 | EError => (Rabble, calls)
adamc@313 248 | EUnif (ref (SOME e)) => exp (penv, calls) e
adamc@313 249 | EUnif (ref NONE) => (Rabble, calls)
adamc@313 250 end
adamc@313 251
adamc@313 252 fun doVali (i, (_, f, _, e), calls) =
adamc@313 253 let
adamc@313 254 fun unravel (e, j, penv) =
adamc@313 255 case #1 e of
adamc@313 256 EAbs (_, t, _, e) =>
adamc@313 257 unravel (e, j + 1, Arg (i, j, t) :: penv)
adamc@313 258 | ECAbs (_, _, _, e) =>
adamc@313 259 unravel (e, j, penv)
adamc@313 260 | _ => (j, #2 (exp (penv, calls) e))
adamc@313 261 in
adamc@313 262 unravel (e, 0, [])
adamc@313 263 end
adamc@313 264
adamc@313 265 val (ns, calls) = ListUtil.foldliMap doVali [] vis
adamc@313 266
adamc@313 267 fun search (ns, choices) =
adamc@313 268 case ns of
adamc@313 269 [] =>
adamc@313 270 let
adamc@313 271 val choices = rev choices
adamc@313 272 in
adamc@313 273 List.all (fn (f, args) =>
adamc@313 274 let
adamc@313 275 val recArg = List.nth (choices, f)
adamc@313 276
adamc@313 277 fun isDatatype (t, _) =
adamc@313 278 case t of
adamc@313 279 CNamed _ => true
adamc@313 280 | CModProj _ => true
adamc@313 281 | CApp (t, _) => isDatatype t
adamc@313 282 | _ => false
adamc@313 283 in
adamc@313 284 length args > recArg andalso
adamc@313 285 case List.nth (args, recArg) of
adamc@313 286 Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i)
adamc@313 287 | _ => false
adamc@313 288 end) calls
adamc@313 289 end
adamc@313 290 | n :: ns' =>
adamc@313 291 let
adamc@313 292 fun search' i =
adamc@313 293 i < n andalso (search (ns', i :: choices) orelse search' (i + 1))
adamc@313 294 in
adamc@313 295 search' 0
adamc@313 296 end
adamc@313 297 in
adamc@313 298 if search (ns, []) then
adamc@313 299 ()
adamc@313 300 else
adamc@313 301 ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)"
adamc@313 302 end
adamc@313 303
adamc@313 304 | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds)
adamc@313 305
adamc@313 306 | _ => ()
adamc@313 307
adamc@313 308 and declOk (d, env) =
adamc@313 309 (declOk' env d;
adamc@313 310 E.declBinds env d)
adamc@313 311
adamc@313 312 fun check ds = ignore (foldl declOk E.empty ds)
adamc@313 313
adamc@313 314 end