Mercurial > urweb

annotate src/reduce.sml @ 509:140c68046598

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most exp rules for new Reduce
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 12:59:32 -0500
parents 04053089878a
children c644ec94866d
rev   line source
adamc@20 1 (* Copyright (c) 2008, Adam Chlipala
adamc@20 2 * All rights reserved.
adamc@20 3 *
adamc@20 4 * Redistribution and use in source and binary forms, with or without
adamc@20 5 * modification, are permitted provided that the following conditions are met:
adamc@20 6 *
adamc@20 7 * - Redistributions of source code must retain the above copyright notice,
adamc@20 8 * this list of conditions and the following disclaimer.
adamc@20 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@20 10 * this list of conditions and the following disclaimer in the documentation
adamc@20 11 * and/or other materials provided with the distribution.
adamc@20 12 * - The names of contributors may not be used to endorse or promote products
adamc@20 13 * derived from this software without specific prior written permission.
adamc@20 14 *
adamc@20 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@20 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@20 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@20 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@20 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@20 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@20 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@20 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@20 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@20 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@20 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@20 26 *)
adamc@20 27
adamc@20 28 (* Simplify a Core program algebraically *)
adamc@20 29
adamc@20 30 structure Reduce :> REDUCE = struct
adamc@20 31
adamc@20 32 open Core
adamc@20 33
adamc@508 34 structure IM = IntBinaryMap
adamc@20 35
adamc@508 36 datatype env_item =
adamc@508 37 UnknownC
adamc@508 38 | KnownC of con
adamc@21 39
adamc@508 40 | UnknownE
adamc@508 41 | KnownE of exp
adamc@20 42
adamc@508 43 | Lift of int * int
adamc@20 44
adamc@508 45 type env = env_item list
adamc@20 46
adamc@508 47 fun conAndExp (namedC, namedE) =
adamc@508 48 let
adamc@508 49 fun con env (all as (c, loc)) =
adamc@508 50 case c of
adamc@508 51 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
adamc@508 52 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
adamc@508 53 | TRecord c => (TRecord (con env c), loc)
adamc@215 54
adamc@508 55 | CRel n =>
adamc@508 56 let
adamc@508 57 fun find (n', env, lift) =
adamc@508 58 if n' = 0 then
adamc@508 59 case env of
adamc@508 60 UnknownC :: _ => (CRel (n + lift), loc)
adamc@508 61 | KnownC c :: _ => con (Lift (lift, 0) :: env) c
adamc@509 62 | Lift (lift', _) :: rest => find (0, rest, lift + lift')
adamc@508 63 | _ => raise Fail "Reduce.con: CRel [1]"
adamc@508 64 else
adamc@508 65 case env of
adamc@508 66 UnknownC :: rest => find (n' - 1, rest, lift + 1)
adamc@508 67 | KnownC _ :: rest => find (n' - 1, rest, lift)
adamc@508 68 | UnknownE :: rest => find (n' - 1, rest, lift)
adamc@508 69 | KnownE _ :: rest => find (n' - 1, rest, lift)
adamc@509 70 | Lift (lift', _) :: rest => find (n', rest, lift + lift')
adamc@508 71 | [] => raise Fail "Reduce.con: CRel [2]"
adamc@508 72 in
adamc@508 73 find (n, env, 0)
adamc@508 74 end
adamc@508 75 | CNamed n =>
adamc@508 76 (case IM.find (namedC, n) of
adamc@508 77 NONE => all
adamc@508 78 | SOME c => c)
adamc@508 79 | CFfi _ => all
adamc@508 80 | CApp (c1, c2) =>
adamc@508 81 let
adamc@508 82 val c1 = con env c1
adamc@508 83 val c2 = con env c2
adamc@508 84 in
adamc@508 85 case #1 c1 of
adamc@508 86 CAbs (_, _, b) =>
adamc@508 87 con (KnownC c2 :: env) b
adamc@215 88
adamc@508 89 | CApp ((CApp (fold as (CFold _, _), f), _), i) =>
adamc@508 90 (case #1 c2 of
adamc@508 91 CRecord (_, []) => i
adamc@508 92 | CRecord (k, (x, c) :: rest) =>
adamc@508 93 con env (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@508 94 (CApp ((CApp ((CApp (fold, f), loc), i), loc),
adamc@508 95 (CRecord (k, rest), loc)), loc)), loc)
adamc@508 96 | _ => (CApp (c1, c2), loc))
adamc@20 97
adamc@508 98 | _ => (CApp (c1, c2), loc)
adamc@508 99 end
adamc@508 100 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
adamc@20 101
adamc@508 102 | CName _ => all
adamc@21 103
adamc@508 104 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@508 105 | CConcat (c1, c2) =>
adamc@508 106 let
adamc@508 107 val c1 = con env c1
adamc@508 108 val c2 = con env c2
adamc@508 109 in
adamc@508 110 case (#1 c1, #1 c2) of
adamc@508 111 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@508 112 (CRecord (k, xcs1 @ xcs2), loc)
adamc@508 113 | _ => (CConcat (c1, c2), loc)
adamc@508 114 end
adamc@508 115 | CFold _ => all
adamc@74 116
adamc@508 117 | CUnit => all
adamc@21 118
adamc@508 119 | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@508 120 | CProj (c, n) =>
adamc@508 121 let
adamc@508 122 val c = con env c
adamc@508 123 in
adamc@508 124 case #1 c of
adamc@508 125 CTuple cs => List.nth (cs, n - 1)
adamc@508 126 | _ => (CProj (c, n), loc)
adamc@508 127 end
adamc@22 128
adamc@509 129 fun patCon pc =
adamc@509 130 case pc of
adamc@509 131 PConVar _ => pc
adamc@509 132 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
adamc@509 133 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
adamc@509 134 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
adamc@509 135 kind = kind}
adamc@509 136
adamc@509 137
adamc@509 138 val k = (KType, ErrorMsg.dummySpan)
adamc@509 139 fun doPart e (this as (x, t), rest) =
adamc@509 140 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
adamc@509 141 this :: rest)
adamc@509 142
adamc@509 143 fun exp env (all as (e, loc)) =
adamc@509 144 case e of
adamc@509 145 EPrim _ => all
adamc@509 146 | ERel n =>
adamc@509 147 let
adamc@509 148 fun find (n', env, liftC, liftE) =
adamc@509 149 if n' = 0 then
adamc@509 150 case env of
adamc@509 151 UnknownE :: _ => (ERel (n + liftE), loc)
adamc@509 152 | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e
adamc@509 153 | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE')
adamc@509 154 | _ => raise Fail "Reduce.exp: ERel [1]"
adamc@509 155 else
adamc@509 156 case env of
adamc@509 157 UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE)
adamc@509 158 | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE)
adamc@509 159 | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1)
adamc@509 160 | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE)
adamc@509 161 | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE')
adamc@509 162 | [] => raise Fail "Reduce.exp: ERel [2]"
adamc@509 163 in
adamc@509 164 find (n, env, 0, 0)
adamc@509 165 end
adamc@509 166 | ENamed n =>
adamc@509 167 (case IM.find (namedE, n) of
adamc@509 168 NONE => all
adamc@509 169 | SOME e => e)
adamc@509 170 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
adamc@509 171 map (con env) cs, Option.map (exp env) eo), loc)
adamc@509 172 | EFfi _ => all
adamc@509 173 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@509 174
adamc@509 175 | EApp (e1, e2) =>
adamc@509 176 let
adamc@509 177 val e1 = exp env e1
adamc@509 178 val e2 = exp env e2
adamc@509 179 in
adamc@509 180 case #1 e1 of
adamc@509 181 EAbs (_, _, _, b) => exp (KnownE e2 :: env) b
adamc@509 182 | _ => (EApp (e1, e2), loc)
adamc@509 183 end
adamc@509 184
adamc@509 185 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
adamc@509 186
adamc@509 187 | ECApp (e, c) =>
adamc@509 188 let
adamc@509 189 val e = exp env e
adamc@509 190 val c = con env c
adamc@509 191 in
adamc@509 192 case #1 e of
adamc@509 193 ECAbs (_, _, b) => exp (KnownC c :: env) b
adamc@509 194 | _ => (ECApp (e, c), loc)
adamc@509 195 end
adamc@509 196
adamc@509 197 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
adamc@509 198
adamc@509 199 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
adamc@509 200 | EField (e, c, {field, rest}) =>
adamc@509 201 let
adamc@509 202 val e = exp env e
adamc@509 203 val c = con env c
adamc@509 204
adamc@509 205 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
adamc@509 206 in
adamc@509 207 case (#1 e, #1 c) of
adamc@509 208 (ERecord xcs, CName x) =>
adamc@509 209 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@509 210 NONE => default ()
adamc@509 211 | SOME (_, e, _) => e)
adamc@509 212 | _ => default ()
adamc@509 213 end
adamc@509 214
adamc@509 215 | EConcat (e1, c1, e2, c2) =>
adamc@509 216 let
adamc@509 217 val e1 = exp env e1
adamc@509 218 val e2 = exp env e2
adamc@509 219 in
adamc@509 220 case (#1 e1, #1 e2) of
adamc@509 221 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
adamc@509 222 | _ =>
adamc@509 223 let
adamc@509 224 val c1 = con env c1
adamc@509 225 val c2 = con env c2
adamc@509 226 in
adamc@509 227 case (#1 c1, #1 c2) of
adamc@509 228 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@509 229 let
adamc@509 230 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
adamc@509 231 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
adamc@509 232 in
adamc@509 233 exp env (ERecord (xes1 @ xes2), loc)
adamc@509 234 end
adamc@509 235 | _ => (EConcat (e1, c1, e2, c2), loc)
adamc@509 236 end
adamc@509 237 end
adamc@509 238
adamc@509 239 | ECut (e, c, {field, rest}) =>
adamc@509 240 let
adamc@509 241 val e = exp env e
adamc@509 242 val c = con env c
adamc@509 243
adamc@509 244 fun default () =
adamc@509 245 let
adamc@509 246 val rest = con env rest
adamc@509 247 in
adamc@509 248 case #1 rest of
adamc@509 249 CRecord (k, xcs) =>
adamc@509 250 let
adamc@509 251 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@509 252 in
adamc@509 253 exp env (ERecord xes, loc)
adamc@509 254 end
adamc@509 255 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
adamc@509 256 end
adamc@509 257 in
adamc@509 258 case (#1 e, #1 c) of
adamc@509 259 (ERecord xes, CName x) =>
adamc@509 260 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
adamc@509 261 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
adamc@509 262 | _ => raise Fail "Reduce: ECut") xes), loc)
adamc@509 263 else
adamc@509 264 default ()
adamc@509 265 | _ => default ()
adamc@509 266 end
adamc@509 267
adamc@509 268 | ECutMulti (e, c, {rest}) =>
adamc@509 269 let
adamc@509 270 val e = exp env e
adamc@509 271 val c = con env c
adamc@509 272
adamc@509 273 fun default () =
adamc@509 274 let
adamc@509 275 val rest = con env rest
adamc@509 276 in
adamc@509 277 case #1 rest of
adamc@509 278 CRecord (k, xcs) =>
adamc@509 279 let
adamc@509 280 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@509 281 in
adamc@509 282 exp env (ERecord xes, loc)
adamc@509 283 end
adamc@509 284 | _ => (ECutMulti (e, c, {rest = rest}), loc)
adamc@509 285 end
adamc@509 286 in
adamc@509 287 case (#1 e, #1 c) of
adamc@509 288 (ERecord xes, CRecord (_, xcs)) =>
adamc@509 289 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
adamc@509 290 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
adamc@509 291 (ERecord (List.filter (fn ((CName x', _), _, _) =>
adamc@509 292 List.all (fn ((CName x, _), _) => x' <> x
adamc@509 293 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
adamc@509 294 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
adamc@509 295 else
adamc@509 296 default ()
adamc@509 297 | _ => default ()
adamc@509 298 end
adamc@509 299
adamc@509 300 | EFold _ => all
adamc@509 301
adamc@509 302 | ECase (e, pes, {disc, result}) =>
adamc@509 303 let
adamc@509 304 fun patBinds (p, _) =
adamc@509 305 case p of
adamc@509 306 PWild => 0
adamc@509 307 | PVar _ => 1
adamc@509 308 | PPrim _ => 0
adamc@509 309 | PCon (_, _, _, NONE) => 0
adamc@509 310 | PCon (_, _, _, SOME p) => patBinds p
adamc@509 311 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@509 312
adamc@509 313 fun pat (all as (p, loc)) =
adamc@509 314 case p of
adamc@509 315 PWild => all
adamc@509 316 | PVar (x, t) => (PVar (x, con env t), loc)
adamc@509 317 | PPrim _ => all
adamc@509 318 | PCon (dk, pc, cs, po) =>
adamc@509 319 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
adamc@509 320 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
adamc@509 321 in
adamc@509 322 (ECase (exp env e,
adamc@509 323 map (fn (p, e) => (pat p,
adamc@509 324 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
adamc@509 325 pes, {disc = con env disc, result = con env result}), loc)
adamc@509 326 end
adamc@509 327
adamc@509 328 | EWrite e => (EWrite (exp env e), loc)
adamc@509 329 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@509 330
adamc@509 331 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
adamc@417 332 in
adamc@508 333 {con = con, exp = exp}
adamc@417 334 end
adamc@21 335
adamc@509 336 fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c
adamc@509 337 fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e
adamc@20 338
adamc@508 339 fun reduce file =
adamc@508 340 let
adamc@508 341 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
adamc@508 342 case #1 d of
adamc@508 343 DCon (x, n, k, c) =>
adamc@508 344 let
adamc@509 345 val c = con namedC [] c
adamc@508 346 in
adamc@508 347 ((DCon (x, n, k, c), loc),
adamc@508 348 (IM.insert (namedC, n, c), namedE))
adamc@508 349 end
adamc@508 350 | DDatatype (x, n, ps, cs) =>
adamc@509 351 let
adamc@509 352 val env = map (fn _ => UnknownC) ps
adamc@509 353 in
adamc@509 354 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc),
adamc@509 355 st)
adamc@509 356 end
adamc@508 357 | DVal (x, n, t, e, s) =>
adamc@508 358 let
adamc@509 359 val t = con namedC [] t
adamc@509 360 val e = exp (namedC, namedE) [] e
adamc@508 361 in
adamc@508 362 ((DVal (x, n, t, e, s), loc),
adamc@508 363 (namedC, IM.insert (namedE, n, e)))
adamc@508 364 end
adamc@508 365 | DValRec vis =>
adamc@509 366 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc),
adamc@508 367 st)
adamc@508 368 | DExport _ => (d, st)
adamc@509 369 | DTable (s, n, c, s') => ((DTable (s, n, con namedC [] c, s'), loc), st)
adamc@508 370 | DSequence _ => (d, st)
adamc@508 371 | DDatabase _ => (d, st)
adamc@509 372 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
adamc@20 373
adamc@508 374 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
adamc@508 375 in
adamc@508 376 file
adamc@508 377 end
adamc@20 378
adamc@20 379 end