Mercurial > urweb

annotate src/reduce_local.sml @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 230654093b51
children 4a125bbc602d
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@512 54 [] => raise Fail "ReduceLocal.exp: ERel"
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@512 75 | EApp (e1, e2) =>
adamc@512 76 let
adamc@512 77 val e1 = exp env e1
adamc@512 78 val e2 = exp env e2
adamc@512 79 in
adamc@512 80 case #1 e1 of
adamc@512 81 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
adamc@512 82 | _ => (EApp (e1, e2), loc)
adamc@512 83 end
adamc@512 84
adamc@512 85 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
adamc@512 86
adamc@512 87 | ECApp (e, c) => (ECApp (exp env e, c), loc)
adamc@626 88 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
adamc@512 89
adamc@626 90 | EKApp (e, k) => (EKApp (exp env e, k), loc)
adamc@626 91 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
adamc@512 92
adamc@512 93 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
adamc@512 94 | EField (e, c, others) =>
adamc@512 95 let
adamc@512 96 val e = exp env e
adamc@512 97
adamc@512 98 fun default () = (EField (e, c, others), loc)
adamc@512 99 in
adamc@512 100 case (#1 e, #1 c) of
adamc@512 101 (ERecord xcs, CName x) =>
adamc@512 102 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@512 103 NONE => default ()
adamc@512 104 | SOME (_, e, _) => e)
adamc@512 105 | _ => default ()
adamc@512 106 end
adamc@512 107
adamc@512 108 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
adamc@512 109 | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
adamc@512 110 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
adamc@512 111
adamc@512 112 | ECase (e, pes, others) =>
adamc@512 113 let
adamc@512 114 fun patBinds (p, _) =
adamc@512 115 case p of
adamc@512 116 PWild => 0
adamc@512 117 | PVar _ => 1
adamc@512 118 | PPrim _ => 0
adamc@512 119 | PCon (_, _, _, NONE) => 0
adamc@512 120 | PCon (_, _, _, SOME p) => patBinds p
adamc@512 121 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@512 122 in
adamc@512 123 (ECase (exp env e,
adamc@512 124 map (fn (p, e) => (p,
adamc@512 125 exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e))
adamc@512 126 pes, others), loc)
adamc@512 127 end
adamc@512 128
adamc@512 129 | EWrite e => (EWrite (exp env e), loc)
adamc@512 130 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@512 131
adamc@512 132 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
adamc@512 133
adamc@609 134 | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, t), loc)
adamc@607 135
adamc@512 136 fun reduce file =
adamc@482 137 let
adamc@512 138 fun doDecl (d as (_, loc)) =
adamc@512 139 case #1 d of
adamc@512 140 DCon _ => d
adamc@512 141 | DDatatype _ => d
adamc@512 142 | DVal (x, n, t, e, s) =>
adamc@512 143 let
adamc@512 144 val e = exp [] e
adamc@512 145 in
adamc@512 146 (DVal (x, n, t, e, s), loc)
adamc@512 147 end
adamc@512 148 | DValRec vis =>
adamc@512 149 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
adamc@512 150 | DExport _ => d
adamc@512 151 | DTable _ => d
adamc@512 152 | DSequence _ => d
adamc@512 153 | DDatabase _ => d
adamc@512 154 | DCookie _ => d
adamc@482 155 in
adamc@512 156 map doDecl file
adamc@482 157 end
adamc@482 158
adamc@482 159 end