Mercurial > urweb

annotate src/reduce_local.sml @ 953:301530da2062

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Bad sort functions tested
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 14:57:38 -0400
parents ed06e25c70ef
children 2a50da66ffd8
rev   line source
adamc@482 1 (* Copyright (c) 2008, Adam Chlipala
adamc@482 2 * All rights reserved.
adamc@482 3 *
adamc@482 4 * Redistribution and use in source and binary forms, with or without
adamc@482 5 * modification, are permitted provided that the following conditions are met:
adamc@482 6 *
adamc@482 7 * - Redistributions of source code must retain the above copyright notice,
adamc@482 8 * this list of conditions and the following disclaimer.
adamc@482 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@482 10 * this list of conditions and the following disclaimer in the documentation
adamc@482 11 * and/or other materials provided with the distribution.
adamc@482 12 * - The names of contributors may not be used to endorse or promote products
adamc@482 13 * derived from this software without specific prior written permission.
adamc@482 14 *
adamc@482 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@482 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@482 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@482 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@482 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@482 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@482 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@482 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@482 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@482 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@482 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@482 26 *)
adamc@482 27
adamc@482 28 (* Simplify a Core program algebraically, without unfolding definitions *)
adamc@482 29
adamc@482 30 structure ReduceLocal :> REDUCE_LOCAL = struct
adamc@482 31
adamc@482 32 open Core
adamc@482 33
adamc@512 34 structure IM = IntBinaryMap
adamc@482 35
adamc@512 36 datatype env_item =
adamc@512 37 Unknown
adamc@512 38 | Known of exp
adamc@482 39
adamc@512 40 | Lift of int
adamc@482 41
adamc@512 42 type env = env_item list
adamc@512 43
adamc@512 44 val deKnown = List.filter (fn Known _ => false
adamc@512 45 | _ => true)
adamc@512 46
adamc@512 47 fun exp env (all as (e, loc)) =
adamc@512 48 case e of
adamc@512 49 EPrim _ => all
adamc@512 50 | ERel n =>
adamc@512 51 let
adamc@512 52 fun find (n', env, nudge, lift) =
adamc@512 53 case env of
adamc@642 54 [] => (ERel (n + nudge), loc)
adamc@512 55 | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
adamc@512 56 | Unknown :: rest =>
adamc@512 57 if n' = 0 then
adamc@512 58 (ERel (n + nudge), loc)
adamc@512 59 else
adamc@512 60 find (n' - 1, rest, nudge, lift + 1)
adamc@512 61 | Known e :: rest =>
adamc@512 62 if n' = 0 then
adamc@512 63 ((*print "SUBSTITUTING\n";*)
adamc@512 64 exp (Lift lift :: rest) e)
adamc@512 65 else
adamc@512 66 find (n' - 1, rest, nudge - 1, lift)
adamc@512 67 in
adamc@512 68 find (n, env, 0, 0)
adamc@512 69 end
adamc@512 70 | ENamed _ => all
adamc@512 71 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
adamc@512 72 | EFfi _ => all
adamc@512 73 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@512 74
adamc@721 75 | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
adamc@721 76 (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
adamc@721 77 t), _), e) =>
adamc@721 78 (ECon (dk, pc, [t], SOME (exp env e)), loc)
adamc@721 79
adamc@512 80 | EApp (e1, e2) =>
adamc@512 81 let
adamc@512 82 val e1 = exp env e1
adamc@512 83 val e2 = exp env e2
adamc@512 84 in
adamc@512 85 case #1 e1 of
adamc@512 86 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
adamc@512 87 | _ => (EApp (e1, e2), loc)
adamc@512 88 end
adamc@512 89
adamc@512 90 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
adamc@512 91
adamc@721 92 | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
adamc@721 93 (ECon (dk, pc, [t], NONE), loc)
adamc@721 94
adamc@512 95 | ECApp (e, c) => (ECApp (exp env e, c), loc)
adamc@626 96 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
adamc@512 97
adamc@626 98 | EKApp (e, k) => (EKApp (exp env e, k), loc)
adamc@626 99 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
adamc@512 100
adamc@512 101 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
adamc@512 102 | EField (e, c, others) =>
adamc@512 103 let
adamc@512 104 val e = exp env e
adamc@512 105
adamc@512 106 fun default () = (EField (e, c, others), loc)
adamc@512 107 in
adamc@512 108 case (#1 e, #1 c) of
adamc@512 109 (ERecord xcs, CName x) =>
adamc@512 110 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@512 111 NONE => default ()
adamc@512 112 | SOME (_, e, _) => e)
adamc@512 113 | _ => default ()
adamc@512 114 end
adamc@512 115
adamc@512 116 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
adamc@512 117 | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
adamc@512 118 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
adamc@512 119
adamc@512 120 | ECase (e, pes, others) =>
adamc@512 121 let
adamc@512 122 fun patBinds (p, _) =
adamc@512 123 case p of
adamc@512 124 PWild => 0
adamc@512 125 | PVar _ => 1
adamc@512 126 | PPrim _ => 0
adamc@512 127 | PCon (_, _, _, NONE) => 0
adamc@512 128 | PCon (_, _, _, SOME p) => patBinds p
adamc@512 129 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@512 130 in
adamc@512 131 (ECase (exp env e,
adamc@512 132 map (fn (p, e) => (p,
adamc@512 133 exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e))
adamc@512 134 pes, others), loc)
adamc@512 135 end
adamc@512 136
adamc@512 137 | EWrite e => (EWrite (exp env e), loc)
adamc@512 138 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@512 139
adamc@512 140 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
adamc@512 141
adamc@908 142 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e, t1, t2), loc)
adamc@607 143
adamc@512 144 fun reduce file =
adamc@482 145 let
adamc@512 146 fun doDecl (d as (_, loc)) =
adamc@512 147 case #1 d of
adamc@512 148 DCon _ => d
adamc@512 149 | DDatatype _ => d
adamc@512 150 | DVal (x, n, t, e, s) =>
adamc@512 151 let
adamc@512 152 val e = exp [] e
adamc@512 153 in
adamc@512 154 (DVal (x, n, t, e, s), loc)
adamc@512 155 end
adamc@512 156 | DValRec vis =>
adamc@512 157 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
adamc@512 158 | DExport _ => d
adamc@512 159 | DTable _ => d
adamc@512 160 | DSequence _ => d
adamc@754 161 | DView _ => d
adamc@512 162 | DDatabase _ => d
adamc@512 163 | DCookie _ => d
adamc@718 164 | DStyle _ => d
adamc@482 165 in
adamc@512 166 map doDecl file
adamc@482 167 end
adamc@482 168
adamc@642 169 val reduceExp = exp []
adamc@642 170
adamc@482 171 end