Mercurial > urweb

annotate src/reduce.sml @ 508:04053089878a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of new Reduce
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 12:13:00 -0500
parents ae03d09043c1
children 140c68046598
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@508 62 | _ => raise Fail "Reduce.con: CRel [1]"
adamc@508 63 else
adamc@508 64 case env of
adamc@508 65 UnknownC :: rest => find (n' - 1, rest, lift + 1)
adamc@508 66 | KnownC _ :: rest => find (n' - 1, rest, lift)
adamc@508 67 | UnknownE :: rest => find (n' - 1, rest, lift)
adamc@508 68 | KnownE _ :: rest => find (n' - 1, rest, lift)
adamc@508 69 | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift')
adamc@508 70 | [] => raise Fail "Reduce.con: CRel [2]"
adamc@508 71 in
adamc@508 72 find (n, env, 0)
adamc@508 73 end
adamc@508 74 | CNamed n =>
adamc@508 75 (case IM.find (namedC, n) of
adamc@508 76 NONE => all
adamc@508 77 | SOME c => c)
adamc@508 78 | CFfi _ => all
adamc@508 79 | CApp (c1, c2) =>
adamc@508 80 let
adamc@508 81 val c1 = con env c1
adamc@508 82 val c2 = con env c2
adamc@508 83 in
adamc@508 84 case #1 c1 of
adamc@508 85 CAbs (_, _, b) =>
adamc@508 86 con (KnownC c2 :: env) b
adamc@215 87
adamc@508 88 | CApp ((CApp (fold as (CFold _, _), f), _), i) =>
adamc@508 89 (case #1 c2 of
adamc@508 90 CRecord (_, []) => i
adamc@508 91 | CRecord (k, (x, c) :: rest) =>
adamc@508 92 con env (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@508 93 (CApp ((CApp ((CApp (fold, f), loc), i), loc),
adamc@508 94 (CRecord (k, rest), loc)), loc)), loc)
adamc@508 95 | _ => (CApp (c1, c2), loc))
adamc@20 96
adamc@508 97 | _ => (CApp (c1, c2), loc)
adamc@508 98 end
adamc@508 99 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
adamc@20 100
adamc@508 101 | CName _ => all
adamc@21 102
adamc@508 103 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@508 104 | CConcat (c1, c2) =>
adamc@508 105 let
adamc@508 106 val c1 = con env c1
adamc@508 107 val c2 = con env c2
adamc@508 108 in
adamc@508 109 case (#1 c1, #1 c2) of
adamc@508 110 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@508 111 (CRecord (k, xcs1 @ xcs2), loc)
adamc@508 112 | _ => (CConcat (c1, c2), loc)
adamc@508 113 end
adamc@508 114 | CFold _ => all
adamc@74 115
adamc@508 116 | CUnit => all
adamc@21 117
adamc@508 118 | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@508 119 | CProj (c, n) =>
adamc@508 120 let
adamc@508 121 val c = con env c
adamc@508 122 in
adamc@508 123 case #1 c of
adamc@508 124 CTuple cs => List.nth (cs, n - 1)
adamc@508 125 | _ => (CProj (c, n), loc)
adamc@508 126 end
adamc@22 127
adamc@508 128 fun exp env e = e
adamc@417 129 in
adamc@508 130 {con = con, exp = exp}
adamc@417 131 end
adamc@21 132
adamc@508 133 fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c
adamc@508 134 fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e
adamc@20 135
adamc@508 136 fun reduce file =
adamc@508 137 let
adamc@508 138 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
adamc@508 139 case #1 d of
adamc@508 140 DCon (x, n, k, c) =>
adamc@508 141 let
adamc@508 142 val c = con namedC c
adamc@508 143 in
adamc@508 144 ((DCon (x, n, k, c), loc),
adamc@508 145 (IM.insert (namedC, n, c), namedE))
adamc@508 146 end
adamc@508 147 | DDatatype (x, n, ps, cs) =>
adamc@508 148 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc),
adamc@508 149 st)
adamc@508 150 | DVal (x, n, t, e, s) =>
adamc@508 151 let
adamc@508 152 val t = con namedC t
adamc@508 153 val e = exp (namedC, namedE) e
adamc@508 154 in
adamc@508 155 ((DVal (x, n, t, e, s), loc),
adamc@508 156 (namedC, IM.insert (namedE, n, e)))
adamc@508 157 end
adamc@508 158 | DValRec vis =>
adamc@508 159 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc),
adamc@508 160 st)
adamc@508 161 | DExport _ => (d, st)
adamc@508 162 | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st)
adamc@508 163 | DSequence _ => (d, st)
adamc@508 164 | DDatabase _ => (d, st)
adamc@508 165 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st)
adamc@20 166
adamc@508 167 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
adamc@508 168 in
adamc@508 169 file
adamc@508 170 end
adamc@20 171
adamc@20 172 end