Mercurial > urweb

annotate src/elab_ops.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents c7b9a33c26c8
children 20f898c29525
rev   line source
adamc@81 1 (* Copyright (c) 2008, Adam Chlipala
adamc@81 2 * All rights reserved.
adamc@81 3 *
adamc@81 4 * Redistribution and use in source and binary forms, with or without
adamc@81 5 * modification, are permitted provided that the following conditions are met:
adamc@81 6 *
adamc@81 7 * - Redistributions of source code must retain the above copyright notice,
adamc@81 8 * this list of conditions and the following disclaimer.
adamc@81 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@81 10 * this list of conditions and the following disclaimer in the documentation
adamc@81 11 * and/or other materials provided with the distribution.
adamc@81 12 * - The names of contributors may not be used to endorse or promote products
adamc@81 13 * derived from this software without specific prior written permission.
adamc@81 14 *
adamc@81 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@81 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@81 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@81 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@81 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@81 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@81 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@81 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@81 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@81 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@81 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@81 26 *)
adamc@81 27
adamc@81 28 structure ElabOps :> ELAB_OPS = struct
adamc@81 29
adamc@81 30 open Elab
adamc@81 31
adamc@81 32 structure E = ElabEnv
adamc@81 33 structure U = ElabUtil
adamc@81 34
adamc@623 35 fun liftKindInKind' by =
adamc@623 36 U.Kind.mapB {kind = fn bound => fn k =>
adamc@623 37 case k of
adamc@623 38 KRel xn =>
adamc@623 39 if xn < bound then
adamc@623 40 k
adamc@623 41 else
adamc@623 42 KRel (xn + by)
adamc@623 43 | _ => k,
adamc@623 44 bind = fn (bound, _) => bound + 1}
adamc@623 45
adamc@623 46 fun subKindInKind' rep =
adamc@623 47 U.Kind.mapB {kind = fn (by, xn) => fn k =>
adamc@623 48 case k of
adamc@623 49 KRel xn' =>
adamc@623 50 (case Int.compare (xn', xn) of
adamc@623 51 EQUAL => #1 (liftKindInKind' by 0 rep)
adamc@623 52 | GREATER => KRel (xn' - 1)
adamc@623 53 | LESS => k)
adamc@623 54 | _ => k,
adamc@623 55 bind = fn ((by, xn), _) => (by+1, xn+1)}
adamc@623 56
adamc@623 57 val liftKindInKind = liftKindInKind' 1
adamc@623 58
adamc@623 59 fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn)
adamc@623 60
adamc@623 61 fun liftKindInCon by =
adamc@623 62 U.Con.mapB {kind = fn bound => fn k =>
adamc@623 63 case k of
adamc@623 64 KRel xn =>
adamc@623 65 if xn < bound then
adamc@623 66 k
adamc@623 67 else
adamc@623 68 KRel (xn + by)
adamc@623 69 | _ => k,
adamc@623 70 con = fn _ => fn c => c,
adamc@623 71 bind = fn (bound, U.Con.RelK _) => bound + 1
adamc@623 72 | (bound, _) => bound}
adamc@623 73
adamc@623 74 fun subKindInCon' rep =
adamc@623 75 U.Con.mapB {kind = fn (by, xn) => fn k =>
adamc@623 76 case k of
adamc@623 77 KRel xn' =>
adamc@623 78 (case Int.compare (xn', xn) of
adamc@623 79 EQUAL => #1 (liftKindInKind' by 0 rep)
adamc@623 80 | GREATER => KRel (xn' - 1)
adamc@623 81 | LESS => k)
adamc@623 82 | _ => k,
adamc@623 83 con = fn _ => fn c => c,
adamc@623 84 bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1)
adamc@623 85 | (st, _) => st}
adamc@623 86
adamc@623 87 val liftKindInCon = liftKindInCon 1
adamc@623 88
adamc@623 89 fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn)
adamc@623 90
adamc@516 91 fun liftConInCon by =
adamc@623 92 U.Con.mapB {kind = fn _ => fn k => k,
adamc@516 93 con = fn bound => fn c =>
adamc@516 94 case c of
adamc@516 95 CRel xn =>
adamc@516 96 if xn < bound then
adamc@516 97 c
adamc@516 98 else
adamc@516 99 CRel (xn + by)
adam@1303 100 | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r)
adamc@516 101 | _ => c,
adamc@623 102 bind = fn (bound, U.Con.RelC _) => bound + 1
adamc@516 103 | (bound, _) => bound}
adamc@81 104
adam@1303 105 exception SubUnif
adam@1303 106
adamc@516 107 fun subConInCon' rep =
adamc@623 108 U.Con.mapB {kind = fn _ => fn k => k,
adamc@516 109 con = fn (by, xn) => fn c =>
adamc@516 110 case c of
adamc@516 111 CRel xn' =>
adamc@516 112 (case Int.compare (xn', xn) of
adamc@516 113 EQUAL => #1 (liftConInCon by 0 rep)
adamc@516 114 | GREATER => CRel (xn' - 1)
adamc@516 115 | LESS => c)
adam@1303 116 | CUnif (0, _, _, _, _) => raise SubUnif
adam@1303 117 | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r)
adamc@516 118 | _ => c,
adamc@623 119 bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
adamc@81 120 | (ctx, _) => ctx}
adamc@81 121
adamc@516 122 val liftConInCon = liftConInCon 1
adamc@516 123
adamc@516 124 fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
adamc@516 125
adamc@81 126 fun subStrInSgn (m1, m2) =
adamc@81 127 U.Sgn.map {kind = fn k => k,
adamc@81 128 con = fn c as CModProj (m1', ms, x) =>
adamc@81 129 if m1 = m1' then
adamc@81 130 CModProj (m2, ms, x)
adamc@81 131 else
adamc@81 132 c
adamc@81 133 | c => c,
adamc@81 134 sgn_item = fn sgi => sgi,
adamc@81 135 sgn = fn sgn => sgn}
adamc@81 136
adamc@905 137 val occurs =
adamc@905 138 U.Con.existsB {kind = fn _ => false,
adamc@905 139 con = fn (n, c) =>
adamc@905 140 case c of
adamc@905 141 CRel n' => n' = n
adamc@905 142 | _ => false,
adamc@905 143 bind = fn (n, b) =>
adamc@905 144 case b of
adamc@905 145 U.Con.RelC _ => n + 1
adamc@905 146 | _ => n}
adamc@905 147 0
adamc@905 148
adamc@1034 149 val identity = ref 0
adamc@1034 150 val distribute = ref 0
adamc@1034 151 val fuse = ref 0
adamc@1034 152
adamc@1034 153 fun reset () = (identity := 0;
adamc@1034 154 distribute := 0;
adamc@1034 155 fuse := 0)
adamc@81 156
adamc@81 157 fun hnormCon env (cAll as (c, loc)) =
adamc@81 158 case c of
adam@1303 159 CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c)
adamc@81 160
adamc@81 161 | CNamed xn =>
adamc@81 162 (case E.lookupCNamed env xn of
adamc@81 163 (_, _, SOME c') => hnormCon env c'
adamc@81 164 | _ => cAll)
adamc@81 165
adamc@81 166 | CModProj (n, ms, x) =>
adamc@81 167 let
adamc@81 168 val (_, sgn) = E.lookupStrNamed env n
adamc@81 169 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@81 170 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@81 171 NONE => raise Fail "hnormCon: Unknown substructure"
adamc@81 172 | SOME sgn => ((StrProj (str, m), loc), sgn))
adamc@81 173 ((StrVar n, loc), sgn) ms
adamc@81 174 in
adamc@81 175 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@81 176 NONE => raise Fail "kindof: Unknown con in structure"
adamc@81 177 | SOME (_, NONE) => cAll
adamc@81 178 | SOME (_, SOME c) => hnormCon env c
adamc@81 179 end
adamc@81 180
adamc@905 181 (* Eta reduction *)
adamc@905 182 | CAbs (x, k, b) =>
adamc@905 183 (case #1 (hnormCon (E.pushCRel env x k) b) of
adamc@905 184 CApp (f, (CRel 0, _)) =>
adamc@905 185 if occurs f then
adamc@905 186 cAll
adamc@905 187 else
adamc@905 188 hnormCon env (subConInCon (0, (CUnit, loc)) f)
adamc@905 189 | _ => cAll)
adamc@905 190
adamc@81 191 | CApp (c1, c2) =>
adamc@81 192 (case #1 (hnormCon env c1) of
adamc@81 193 CAbs (x, k, cb) =>
adamc@81 194 let
adamc@81 195 val sc = (hnormCon env (subConInCon (0, c2) cb))
adamc@81 196 handle SynUnif => cAll
adamc@81 197 (*val env' = E.pushCRel env x k*)
adamc@81 198 in
adamc@328 199 (*Print.eprefaces "Subst" [("x", Print.PD.string x),
adamc@328 200 ("cb", ElabPrint.p_con env' cb),
adamc@328 201 ("c2", ElabPrint.p_con env c2),
adamc@328 202 ("sc", ElabPrint.p_con env sc)];*)
adamc@81 203 sc
adamc@81 204 end
adamc@621 205 | c1' as CApp (c', f) =>
adamc@326 206 let
adamc@326 207 fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
adamc@326 208 in
adamc@326 209 case #1 (hnormCon env c') of
adamc@621 210 CMap (ks as (k1, k2)) =>
adamc@621 211 (case #1 (hnormCon env c2) of
adamc@621 212 CRecord (_, []) => (CRecord (k2, []), loc)
adamc@621 213 | CRecord (_, (x, c) :: rest) =>
adamc@621 214 hnormCon env
adamc@621 215 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
adamc@621 216 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
adamc@621 217 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
adamc@621 218 let
adamc@621 219 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
adamc@621 220 in
adamc@621 221 hnormCon env
adamc@621 222 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
adamc@621 223 (CApp (c1, rest''), loc)), loc)
adamc@621 224 end
adamc@621 225 | _ =>
adamc@621 226 let
adamc@621 227 fun unconstraint c =
adamc@621 228 case hnormCon env c of
adamc@628 229 (TDisjoint (_, _, c), _) => unconstraint c
adamc@621 230 | c => c
adamc@81 231
adamc@1034 232 fun inc r = r := !r + 1
adamc@1034 233
adamc@621 234 fun tryDistributivity () =
adamc@621 235 case hnormCon env c2 of
adamc@621 236 (CConcat (c1, c2'), _) =>
adamc@621 237 let
adamc@621 238 val c = (CMap ks, loc)
adamc@621 239 val c = (CApp (c, f), loc)
adamc@621 240
adamc@621 241 val c1 = (CApp (c, c1), loc)
adamc@621 242 val c2 = (CApp (c, c2'), loc)
adamc@621 243 val c = (CConcat (c1, c2), loc)
adamc@621 244 in
adamc@1034 245 inc distribute;
adamc@621 246 hnormCon env c
adamc@621 247 end
adamc@621 248 | _ => default ()
adamc@329 249
adamc@621 250 fun tryFusion () =
adamc@621 251 case #1 (hnormCon env c2) of
adamc@621 252 CApp (f', r') =>
adamc@621 253 (case #1 (hnormCon env f') of
adamc@621 254 CApp (f', inner_f) =>
adamc@621 255 (case #1 (hnormCon env f') of
adamc@621 256 CMap (dom, _) =>
adamc@621 257 let
adamc@990 258 val inner_f = liftConInCon 0 inner_f
adamc@990 259 val f = liftConInCon 0 f
adamc@990 260
adamc@621 261 val f' = (CApp (inner_f, (CRel 0, loc)), loc)
adamc@621 262 val f' = (CApp (f, f'), loc)
adamc@621 263 val f' = (CAbs ("v", dom, f'), loc)
adamc@329 264
adamc@621 265 val c = (CMap (dom, k2), loc)
adamc@621 266 val c = (CApp (c, f'), loc)
adamc@621 267 val c = (CApp (c, r'), loc)
adamc@621 268 in
adamc@1034 269 inc fuse;
adamc@621 270 hnormCon env c
adamc@621 271 end
adamc@621 272 | _ => tryDistributivity ())
adamc@621 273 | _ => tryDistributivity ())
adamc@621 274 | _ => tryDistributivity ()
adamc@339 275
adamc@621 276 fun tryIdentity () =
adamc@621 277 let
adamc@621 278 fun cunif () =
adamc@621 279 let
adamc@621 280 val r = ref NONE
adamc@621 281 in
adam@1303 282 (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
adamc@621 283 end
adamc@621 284
adamc@621 285 val (vR, v) = cunif ()
adamc@494 286
adamc@621 287 val c = (CApp (f, v), loc)
adamc@621 288 in
adamc@621 289 case unconstraint c of
adam@1303 290 (CUnif (_, _, _, _, vR'), _) =>
adamc@621 291 if vR' = vR then
adamc@1034 292 (inc identity;
adamc@1034 293 hnormCon env c2)
adamc@621 294 else
adamc@621 295 tryFusion ()
adamc@621 296 | _ => tryFusion ()
adamc@621 297 end
adamc@621 298 in
adamc@621 299 tryIdentity ()
adamc@621 300 end)
adamc@326 301 | _ => default ()
adamc@326 302 end
adamc@326 303 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
adamc@623 304
adamc@623 305 | CKApp (c1, k) =>
adamc@623 306 (case hnormCon env c1 of
adamc@623 307 (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body)
adamc@623 308 | _ => cAll)
adamc@621 309
adamc@81 310 | CConcat (c1, c2) =>
adamc@81 311 (case (hnormCon env c1, hnormCon env c2) of
adamc@81 312 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
adamc@81 313 (CRecord (k, xcs1 @ xcs2), loc)
adamc@81 314 | ((CRecord (_, []), _), c2') => c2'
adamc@81 315 | ((CConcat (c11, c12), loc), c2') =>
adamc@81 316 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
adamc@209 317 | (c1', (CRecord (_, []), _)) => c1'
adamc@329 318 | (c1', c2') => (CConcat (c1', c2'), loc))
adamc@81 319
adamc@207 320 | CProj (c, n) =>
adamc@207 321 (case hnormCon env c of
adamc@207 322 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
adamc@207 323 | _ => cAll)
adamc@207 324
adamc@81 325 | _ => cAll
adamc@81 326
adamc@81 327 end