annotate src/checknest.sml @ 1231:5fa8ae2a34e3

Avoid pointless rebuilding of hypothesis E-graphs
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:25:45 -0400
parents 7a31e0cf25e9
children acabf3935060
rev   line source
adamc@879 1 (* Copyright (c) 2009, Adam Chlipala
adamc@879 2 * All rights reserved.
adamc@879 3 *
adamc@879 4 * Redistribution and use in source and binary forms, with or without
adamc@879 5 * modification, are permitted provided that the following conditions are met:
adamc@879 6 *
adamc@879 7 * - Redistributions of source code must retain the above copyright notice,
adamc@879 8 * this list of conditions and the following disclaimer.
adamc@879 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@879 10 * this list of conditions and the following disclaimer in the documentation
adamc@879 11 * and/or other materials provided with the distribution.
adamc@879 12 * - The names of contributors may not be used to endorse or promote products
adamc@879 13 * derived from this software without specific prior written permission.
adamc@879 14 *
adamc@879 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@879 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@879 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@879 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@879 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@879 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@879 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@879 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@879 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@879 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@879 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@879 26 *)
adamc@879 27
adamc@879 28 structure Checknest :> CHECKNEST = struct
adamc@879 29
adamc@879 30 open Cjr
adamc@879 31
adamc@879 32 structure IS = IntBinarySet
adamc@879 33 structure IM = IntBinaryMap
adamc@879 34
adamc@879 35 fun expUses globals =
adamc@879 36 let
adamc@879 37 fun eu (e, _) =
adamc@879 38 case e of
adamc@879 39 EPrim _ => IS.empty
adamc@879 40 | ERel _ => IS.empty
adamc@879 41 | ENamed n => Option.getOpt (IM.find (globals, n), IS.empty)
adamc@879 42 | ECon (_, _, NONE) => IS.empty
adamc@879 43 | ECon (_, _, SOME e) => eu e
adamc@879 44 | ENone _ => IS.empty
adamc@879 45 | ESome (_, e) => eu e
adamc@879 46 | EFfi _ => IS.empty
adamc@879 47 | EFfiApp (_, _, es) => foldl IS.union IS.empty (map eu es)
adamc@879 48 | EApp (e, es) => foldl IS.union (eu e) (map eu es)
adamc@879 49
adamc@879 50 | EUnop (_, e) => eu e
adamc@879 51 | EBinop (_, e1, e2) => IS.union (eu e1, eu e2)
adamc@879 52
adamc@879 53 | ERecord (_, xes) => foldl (fn ((_, e), s) => IS.union (eu e, s)) IS.empty xes
adamc@879 54 | EField (e, _) => eu e
adamc@879 55
adamc@879 56 | ECase (e, pes, _) => foldl (fn ((_, e), s) => IS.union (eu e, s)) (eu e) pes
adamc@879 57
adamc@879 58 | EError (e, _) => eu e
adamc@879 59 | EReturnBlob {blob, mimeType, ...} => IS.union (eu blob, eu mimeType)
adamc@1065 60 | ERedirect (e, _) => eu e
adamc@879 61
adamc@879 62 | EWrite e => eu e
adamc@879 63 | ESeq (e1, e2) => IS.union (eu e1, eu e2)
adamc@879 64 | ELet (_, _, e1, e2) => IS.union (eu e1, eu e2)
adamc@879 65
adamc@879 66 | EQuery {query, body, initial, prepared, ...} =>
adamc@879 67 let
adamc@879 68 val s = IS.union (eu query, IS.union (eu body, eu initial))
adamc@879 69 in
adamc@879 70 case prepared of
adamc@879 71 SOME {id, ...} => IS.add (s, id)
adamc@879 72 | _ => s
adamc@879 73 end
adamc@879 74 | EDml {dml, prepared, ...} =>
adamc@879 75 let
adamc@879 76 val s = eu dml
adamc@879 77 in
adamc@879 78 case prepared of
adamc@879 79 SOME {id, ...} => IS.add (s, id)
adamc@879 80 | _ => s
adamc@879 81 end
adamc@879 82 | ENextval {seq, prepared, ...} =>
adamc@879 83 let
adamc@879 84 val s = eu seq
adamc@879 85 in
adamc@879 86 case prepared of
adamc@879 87 SOME {id, ...} => IS.add (s, id)
adamc@879 88 | _ => s
adamc@879 89 end
adamc@1073 90 | ESetval {seq, count} => IS.union (eu seq, eu count)
adamc@879 91
adamc@1112 92 | EUnurlify (e, _, _) => eu e
adamc@879 93 in
adamc@879 94 eu
adamc@879 95 end
adamc@879 96
adamc@879 97 fun annotateExp globals =
adamc@879 98 let
adamc@879 99 fun ae (e as (_, loc)) =
adamc@879 100 case #1 e of
adamc@879 101 EPrim _ => e
adamc@879 102 | ERel _ => e
adamc@879 103 | ENamed n => e
adamc@879 104 | ECon (_, _, NONE) => e
adamc@879 105 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (ae e)), loc)
adamc@879 106 | ENone _ => e
adamc@879 107 | ESome (t, e) => (ESome (t, ae e), loc)
adamc@879 108 | EFfi _ => e
adamc@879 109 | EFfiApp (m, f, es) => (EFfiApp (m, f, map ae es), loc)
adamc@879 110 | EApp (e, es) => (EApp (ae e, map ae es), loc)
adamc@879 111
adamc@879 112 | EUnop (uo, e) => (EUnop (uo, ae e), loc)
adamc@879 113 | EBinop (bo, e1, e2) => (EBinop (bo, ae e1, ae e2), loc)
adamc@879 114
adamc@879 115 | ERecord (n, xes) => (ERecord (n, map (fn (x, e) => (x, ae e)) xes), loc)
adamc@879 116 | EField (e, f) => (EField (ae e, f), loc)
adamc@879 117
adamc@879 118 | ECase (e, pes, ts) => (ECase (ae e, map (fn (p, e) => (p, ae e)) pes, ts), loc)
adamc@879 119
adamc@879 120 | EError (e, t) => (EError (ae e, t), loc)
adamc@879 121 | EReturnBlob {blob, mimeType, t} => (EReturnBlob {blob = ae blob, mimeType = ae mimeType, t = t}, loc)
adamc@1065 122 | ERedirect (e, t) => (ERedirect (ae e, t), loc)
adamc@879 123
adamc@879 124 | EWrite e => (EWrite (ae e), loc)
adamc@879 125 | ESeq (e1, e2) => (ESeq (ae e1, ae e2), loc)
adamc@879 126 | ELet (x, t, e1, e2) => (ELet (x, t, ae e1, ae e2), loc)
adamc@879 127
adamc@879 128 | EQuery {exps, tables, rnum, state, query, body, initial, prepared} =>
adamc@879 129 (EQuery {exps = exps,
adamc@879 130 tables = tables,
adamc@879 131 rnum = rnum,
adamc@879 132 state = state,
adamc@879 133 query = ae query,
adamc@879 134 body = ae body,
adamc@879 135 initial = ae initial,
adamc@879 136 prepared = case prepared of
adamc@879 137 NONE => NONE
adamc@879 138 | SOME {id, query, ...} => SOME {id = id, query = query,
adamc@879 139 nested = IS.member (expUses globals body, id)}},
adamc@879 140 loc)
adamc@879 141 | EDml {dml, prepared} =>
adamc@879 142 (EDml {dml = ae dml,
adamc@879 143 prepared = prepared}, loc)
adamc@879 144
adamc@879 145 | ENextval {seq, prepared} =>
adamc@879 146 (ENextval {seq = ae seq,
adamc@879 147 prepared = prepared}, loc)
adamc@1073 148 | ESetval {seq, count} =>
adamc@1073 149 (ESetval {seq = ae seq,
adamc@1073 150 count = ae count}, loc)
adamc@879 151
adamc@1112 152 | EUnurlify (e, t, b) => (EUnurlify (ae e, t, b), loc)
adamc@879 153 in
adamc@879 154 ae
adamc@879 155 end
adamc@879 156
adamc@879 157 fun annotate (ds, syms) =
adamc@879 158 let
adamc@879 159 val globals =
adamc@879 160 foldl (fn ((d, _), globals) =>
adamc@879 161 case d of
adamc@879 162 DVal (_, n, _, e) => IM.insert (globals, n, expUses globals e)
adamc@879 163 | DFun (_, n, _, _, e) => IM.insert (globals, n, expUses globals e)
adamc@879 164 | DFunRec fs =>
adamc@879 165 let
adamc@879 166 val s = foldl (fn ((_, _, _, _, e), s) => IS.union (expUses globals e, s)) IS.empty fs
adamc@879 167 in
adamc@879 168 foldl (fn ((_, n, _, _, _), globals) => IM.insert (globals, n, s)) globals fs
adamc@879 169 end
adamc@879 170 | _ => globals) IM.empty ds
adamc@879 171
adamc@879 172 val ds =
adamc@879 173 map (fn d as (_, loc) =>
adamc@879 174 case #1 d of
adamc@879 175 DVal (x, n, t, e) => (DVal (x, n, t, annotateExp globals e), loc)
adamc@879 176 | DFun (x, n, ts, t, e) => (DFun (x, n, ts, t, annotateExp globals e), loc)
adamc@879 177 | DFunRec fs => (DFunRec
adamc@879 178 (map (fn (x, n, ts, t, e) => (x, n, ts, t, annotateExp globals e)) fs), loc)
adamc@879 179 | _ => d) ds
adamc@879 180 in
adamc@879 181 (ds, syms)
adamc@879 182 end
adamc@879 183
adamc@879 184 end