Mercurial > urweb

annotate src/elab_ops.sml @ 853:19fdeef40ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Factor out common request functionality, in preparation for supporting different protocols
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 14:05:12 -0400
parents 12b73f3c108e
children 7a4b026e45dd
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)
adamc@516 100 (*| CUnif _ => raise SynUnif*)
adamc@516 101 | _ => c,
adamc@623 102 bind = fn (bound, U.Con.RelC _) => bound + 1
adamc@516 103 | (bound, _) => bound}
adamc@81 104
adamc@516 105 fun subConInCon' rep =
adamc@623 106 U.Con.mapB {kind = fn _ => fn k => k,
adamc@516 107 con = fn (by, xn) => fn c =>
adamc@516 108 case c of
adamc@516 109 CRel xn' =>
adamc@516 110 (case Int.compare (xn', xn) of
adamc@516 111 EQUAL => #1 (liftConInCon by 0 rep)
adamc@516 112 | GREATER => CRel (xn' - 1)
adamc@516 113 | LESS => c)
adamc@516 114 (*| CUnif _ => raise SynUnif*)
adamc@516 115 | _ => c,
adamc@623 116 bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
adamc@81 117 | (ctx, _) => ctx}
adamc@81 118
adamc@516 119 val liftConInCon = liftConInCon 1
adamc@516 120
adamc@516 121 fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
adamc@516 122
adamc@81 123 fun subStrInSgn (m1, m2) =
adamc@81 124 U.Sgn.map {kind = fn k => k,
adamc@81 125 con = fn c as CModProj (m1', ms, x) =>
adamc@81 126 if m1 = m1' then
adamc@81 127 CModProj (m2, ms, x)
adamc@81 128 else
adamc@81 129 c
adamc@81 130 | c => c,
adamc@81 131 sgn_item = fn sgi => sgi,
adamc@81 132 sgn = fn sgn => sgn}
adamc@81 133
adamc@81 134
adamc@81 135 fun hnormCon env (cAll as (c, loc)) =
adamc@81 136 case c of
adamc@81 137 CUnif (_, _, _, ref (SOME c)) => hnormCon env c
adamc@81 138
adamc@81 139 | CNamed xn =>
adamc@81 140 (case E.lookupCNamed env xn of
adamc@81 141 (_, _, SOME c') => hnormCon env c'
adamc@81 142 | _ => cAll)
adamc@81 143
adamc@81 144 | CModProj (n, ms, x) =>
adamc@81 145 let
adamc@81 146 val (_, sgn) = E.lookupStrNamed env n
adamc@81 147 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@81 148 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@81 149 NONE => raise Fail "hnormCon: Unknown substructure"
adamc@81 150 | SOME sgn => ((StrProj (str, m), loc), sgn))
adamc@81 151 ((StrVar n, loc), sgn) ms
adamc@81 152 in
adamc@81 153 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@81 154 NONE => raise Fail "kindof: Unknown con in structure"
adamc@81 155 | SOME (_, NONE) => cAll
adamc@81 156 | SOME (_, SOME c) => hnormCon env c
adamc@81 157 end
adamc@81 158
adamc@81 159 | CApp (c1, c2) =>
adamc@81 160 (case #1 (hnormCon env c1) of
adamc@81 161 CAbs (x, k, cb) =>
adamc@81 162 let
adamc@81 163 val sc = (hnormCon env (subConInCon (0, c2) cb))
adamc@81 164 handle SynUnif => cAll
adamc@81 165 (*val env' = E.pushCRel env x k*)
adamc@81 166 in
adamc@328 167 (*Print.eprefaces "Subst" [("x", Print.PD.string x),
adamc@328 168 ("cb", ElabPrint.p_con env' cb),
adamc@328 169 ("c2", ElabPrint.p_con env c2),
adamc@328 170 ("sc", ElabPrint.p_con env sc)];*)
adamc@81 171 sc
adamc@81 172 end
adamc@621 173 | c1' as CApp (c', f) =>
adamc@326 174 let
adamc@326 175 fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
adamc@326 176 in
adamc@326 177 case #1 (hnormCon env c') of
adamc@621 178 CMap (ks as (k1, k2)) =>
adamc@621 179 (case #1 (hnormCon env c2) of
adamc@621 180 CRecord (_, []) => (CRecord (k2, []), loc)
adamc@621 181 | CRecord (_, (x, c) :: rest) =>
adamc@621 182 hnormCon env
adamc@621 183 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
adamc@621 184 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
adamc@621 185 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
adamc@621 186 let
adamc@621 187 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
adamc@621 188 in
adamc@621 189 hnormCon env
adamc@621 190 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
adamc@621 191 (CApp (c1, rest''), loc)), loc)
adamc@621 192 end
adamc@621 193 | _ =>
adamc@621 194 let
adamc@621 195 fun unconstraint c =
adamc@621 196 case hnormCon env c of
adamc@628 197 (TDisjoint (_, _, c), _) => unconstraint c
adamc@621 198 | c => c
adamc@81 199
adamc@621 200 fun tryDistributivity () =
adamc@621 201 case hnormCon env c2 of
adamc@621 202 (CConcat (c1, c2'), _) =>
adamc@621 203 let
adamc@621 204 val c = (CMap ks, loc)
adamc@621 205 val c = (CApp (c, f), loc)
adamc@621 206
adamc@621 207 val c1 = (CApp (c, c1), loc)
adamc@621 208 val c2 = (CApp (c, c2'), loc)
adamc@621 209 val c = (CConcat (c1, c2), loc)
adamc@621 210 in
adamc@621 211 hnormCon env c
adamc@621 212 end
adamc@621 213 | _ => default ()
adamc@329 214
adamc@621 215 fun tryFusion () =
adamc@621 216 case #1 (hnormCon env c2) of
adamc@621 217 CApp (f', r') =>
adamc@621 218 (case #1 (hnormCon env f') of
adamc@621 219 CApp (f', inner_f) =>
adamc@621 220 (case #1 (hnormCon env f') of
adamc@621 221 CMap (dom, _) =>
adamc@621 222 let
adamc@621 223 val f' = (CApp (inner_f, (CRel 0, loc)), loc)
adamc@621 224 val f' = (CApp (f, f'), loc)
adamc@621 225 val f' = (CAbs ("v", dom, f'), loc)
adamc@329 226
adamc@621 227 val c = (CMap (dom, k2), loc)
adamc@621 228 val c = (CApp (c, f'), loc)
adamc@621 229 val c = (CApp (c, r'), loc)
adamc@621 230 in
adamc@621 231 hnormCon env c
adamc@621 232 end
adamc@621 233 | _ => tryDistributivity ())
adamc@621 234 | _ => tryDistributivity ())
adamc@621 235 | _ => tryDistributivity ()
adamc@339 236
adamc@621 237 fun tryIdentity () =
adamc@621 238 let
adamc@621 239 fun cunif () =
adamc@621 240 let
adamc@621 241 val r = ref NONE
adamc@621 242 in
adamc@621 243 (r, (CUnif (loc, (KType, loc), "_", r), loc))
adamc@621 244 end
adamc@621 245
adamc@621 246 val (vR, v) = cunif ()
adamc@494 247
adamc@621 248 val c = (CApp (f, v), loc)
adamc@621 249 in
adamc@621 250 case unconstraint c of
adamc@621 251 (CUnif (_, _, _, vR'), _) =>
adamc@621 252 if vR' = vR then
adamc@621 253 hnormCon env c2
adamc@621 254 else
adamc@621 255 tryFusion ()
adamc@621 256 | _ => tryFusion ()
adamc@621 257 end
adamc@621 258 in
adamc@621 259 tryIdentity ()
adamc@621 260 end)
adamc@326 261 | _ => default ()
adamc@326 262 end
adamc@326 263 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
adamc@623 264
adamc@623 265 | CKApp (c1, k) =>
adamc@623 266 (case hnormCon env c1 of
adamc@623 267 (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body)
adamc@623 268 | _ => cAll)
adamc@621 269
adamc@81 270 | CConcat (c1, c2) =>
adamc@81 271 (case (hnormCon env c1, hnormCon env c2) of
adamc@81 272 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
adamc@81 273 (CRecord (k, xcs1 @ xcs2), loc)
adamc@81 274 | ((CRecord (_, []), _), c2') => c2'
adamc@81 275 | ((CConcat (c11, c12), loc), c2') =>
adamc@81 276 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
adamc@209 277 | (c1', (CRecord (_, []), _)) => c1'
adamc@329 278 | (c1', c2') => (CConcat (c1', c2'), loc))
adamc@81 279
adamc@207 280 | CProj (c, n) =>
adamc@207 281 (case hnormCon env c of
adamc@207 282 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
adamc@207 283 | _ => cAll)
adamc@207 284
adamc@81 285 | _ => cAll
adamc@81 286
adamc@81 287 end