Mercurial > urweb

annotate src/elab_util.sml @ 10:dde5c52e5e5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of elaborating expressions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 13:59:03 -0400
parents 14b533dbe6cc
children e97c6d335869
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure ElabUtil :> ELAB_UTIL = struct
adamc@2 29
adamc@2 30 open Elab
adamc@2 31
adamc@2 32 structure S = Search
adamc@2 33
adamc@2 34 structure Kind = struct
adamc@2 35
adamc@6 36 fun mapfold f =
adamc@2 37 let
adamc@2 38 fun mfk k acc =
adamc@2 39 S.bindP (mfk' k acc, f)
adamc@2 40
adamc@2 41 and mfk' (kAll as (k, loc)) =
adamc@2 42 case k of
adamc@2 43 KType => S.return2 kAll
adamc@2 44
adamc@2 45 | KArrow (k1, k2) =>
adamc@2 46 S.bind2 (mfk k1,
adamc@2 47 fn k1' =>
adamc@2 48 S.map2 (mfk k2,
adamc@2 49 fn k2' =>
adamc@2 50 (KArrow (k1', k2'), loc)))
adamc@2 51
adamc@2 52 | KName => S.return2 kAll
adamc@2 53
adamc@2 54 | KRecord k =>
adamc@2 55 S.map2 (mfk k,
adamc@2 56 fn k' =>
adamc@2 57 (KRecord k', loc))
adamc@2 58
adamc@2 59 | KError => S.return2 kAll
adamc@2 60
adamc@2 61 | KUnif (_, ref (SOME k)) => mfk' k
adamc@2 62 | KUnif _ => S.return2 kAll
adamc@2 63 in
adamc@2 64 mfk
adamc@2 65 end
adamc@2 66
adamc@2 67 fun exists f k =
adamc@6 68 case mapfold (fn k => fn () =>
adamc@6 69 if f k then
adamc@6 70 S.Return ()
adamc@6 71 else
adamc@6 72 S.Continue (k, ())) k () of
adamc@6 73 S.Return _ => true
adamc@6 74 | S.Continue _ => false
adamc@6 75
adamc@6 76 end
adamc@6 77
adamc@6 78 structure Con = struct
adamc@6 79
adamc@6 80 fun mapfold {kind = fk, con = fc} =
adamc@6 81 let
adamc@6 82 val mfk = Kind.mapfold fk
adamc@6 83
adamc@6 84 fun mfc c acc =
adamc@6 85 S.bindP (mfc' c acc, fc)
adamc@6 86
adamc@6 87 and mfc' (cAll as (c, loc)) =
adamc@6 88 case c of
adamc@6 89 TFun (c1, c2) =>
adamc@6 90 S.bind2 (mfc c1,
adamc@6 91 fn c1' =>
adamc@6 92 S.map2 (mfc c2,
adamc@6 93 fn c2' =>
adamc@6 94 (TFun (c1', c2'), loc)))
adamc@6 95 | TCFun (e, x, k, c) =>
adamc@6 96 S.bind2 (mfk k,
adamc@6 97 fn k' =>
adamc@6 98 S.map2 (mfc c,
adamc@6 99 fn c' =>
adamc@6 100 (TCFun (e, x, k', c'), loc)))
adamc@6 101 | TRecord c =>
adamc@6 102 S.map2 (mfc c,
adamc@6 103 fn c' =>
adamc@6 104 (TRecord c', loc))
adamc@6 105
adamc@6 106 | CRel _ => S.return2 cAll
adamc@6 107 | CNamed _ => S.return2 cAll
adamc@6 108 | CApp (c1, c2) =>
adamc@6 109 S.bind2 (mfc c1,
adamc@6 110 fn c1' =>
adamc@6 111 S.map2 (mfc c2,
adamc@6 112 fn c2' =>
adamc@6 113 (CApp (c1', c2'), loc)))
adamc@8 114 | CAbs (x, k, c) =>
adamc@6 115 S.bind2 (mfk k,
adamc@6 116 fn k' =>
adamc@6 117 S.map2 (mfc c,
adamc@6 118 fn c' =>
adamc@8 119 (CAbs (x, k', c'), loc)))
adamc@6 120
adamc@6 121 | CName _ => S.return2 cAll
adamc@6 122
adamc@6 123 | CRecord (k, xcs) =>
adamc@6 124 S.bind2 (mfk k,
adamc@6 125 fn k' =>
adamc@6 126 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@6 127 S.bind2 (mfc x,
adamc@6 128 fn x' =>
adamc@6 129 S.map2 (mfc c,
adamc@6 130 fn c' =>
adamc@6 131 (x', c'))))
adamc@6 132 xcs,
adamc@6 133 fn xcs' =>
adamc@6 134 (CRecord (k', xcs'), loc)))
adamc@6 135 | CConcat (c1, c2) =>
adamc@6 136 S.bind2 (mfc c1,
adamc@6 137 fn c1' =>
adamc@6 138 S.map2 (mfc c2,
adamc@6 139 fn c2' =>
adamc@6 140 (CConcat (c1', c2'), loc)))
adamc@6 141
adamc@6 142 | CError => S.return2 cAll
adamc@6 143 | CUnif (_, _, ref (SOME c)) => mfc' c
adamc@6 144 | CUnif _ => S.return2 cAll
adamc@6 145 in
adamc@6 146 mfc
adamc@6 147 end
adamc@6 148
adamc@6 149 fun exists {kind, con} k =
adamc@6 150 case mapfold {kind = fn k => fn () =>
adamc@6 151 if kind k then
adamc@6 152 S.Return ()
adamc@6 153 else
adamc@6 154 S.Continue (k, ()),
adamc@6 155 con = fn c => fn () =>
adamc@6 156 if con c then
adamc@6 157 S.Return ()
adamc@6 158 else
adamc@6 159 S.Continue (c, ())} k () of
adamc@2 160 S.Return _ => true
adamc@2 161 | S.Continue _ => false
adamc@2 162
adamc@2 163 end
adamc@2 164
adamc@10 165 structure Exp = struct
adamc@10 166
adamc@10 167 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@10 168 let
adamc@10 169 val mfk = Kind.mapfold fk
adamc@10 170 val mfc = Con.mapfold {kind = fk, con = fc}
adamc@10 171
adamc@10 172 fun mfe e acc =
adamc@10 173 S.bindP (mfe' e acc, fe)
adamc@10 174
adamc@10 175 and mfe' (eAll as (e, loc)) =
adamc@10 176 case e of
adamc@10 177 ERel _ => S.return2 eAll
adamc@10 178 | ENamed _ => S.return2 eAll
adamc@10 179 | EApp (e1, e2) =>
adamc@10 180 S.bind2 (mfe e1,
adamc@10 181 fn e1' =>
adamc@10 182 S.map2 (mfe e2,
adamc@10 183 fn e2' =>
adamc@10 184 (EApp (e1', e2'), loc)))
adamc@10 185 | EAbs (x, t, e) =>
adamc@10 186 S.bind2 (mfc t,
adamc@10 187 fn t' =>
adamc@10 188 S.map2 (mfe e,
adamc@10 189 fn e' =>
adamc@10 190 (EAbs (x, t', e'), loc)))
adamc@10 191
adamc@10 192 | ECApp (e, c) =>
adamc@10 193 S.bind2 (mfe e,
adamc@10 194 fn e' =>
adamc@10 195 S.map2 (mfc c,
adamc@10 196 fn c' =>
adamc@10 197 (ECApp (e', c'), loc)))
adamc@10 198 | ECAbs (expl, x, k, e) =>
adamc@10 199 S.bind2 (mfk k,
adamc@10 200 fn k' =>
adamc@10 201 S.map2 (mfe e,
adamc@10 202 fn e' =>
adamc@10 203 (ECAbs (expl, x, k', e'), loc)))
adamc@10 204
adamc@10 205 | EError => S.return2 eAll
adamc@10 206 in
adamc@10 207 mfe
adamc@10 208 end
adamc@10 209
adamc@10 210 fun exists {kind, con, exp} k =
adamc@10 211 case mapfold {kind = fn k => fn () =>
adamc@10 212 if kind k then
adamc@10 213 S.Return ()
adamc@10 214 else
adamc@10 215 S.Continue (k, ()),
adamc@10 216 con = fn c => fn () =>
adamc@10 217 if con c then
adamc@10 218 S.Return ()
adamc@10 219 else
adamc@10 220 S.Continue (c, ()),
adamc@10 221 exp = fn e => fn () =>
adamc@10 222 if exp e then
adamc@10 223 S.Return ()
adamc@10 224 else
adamc@10 225 S.Continue (e, ())} k () of
adamc@10 226 S.Return _ => true
adamc@10 227 | S.Continue _ => false
adamc@10 228
adamc@10 229 end
adamc@10 230
adamc@3 231 structure E = ElabEnv
adamc@3 232
adamc@3 233 fun declBinds env (d, _) =
adamc@3 234 case d of
adamc@5 235 DCon (x, n, k, _) => E.pushCNamedAs env x n k
adamc@9 236 | DVal (x, n, t, _) => E.pushENamedAs env x n t
adamc@3 237
adamc@2 238 end