Mercurial > urweb

annotate src/defunc.sml @ 665:910bf013da4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mention src/coq in CHANGELOG
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Mar 2009 12:37:02 -0400
parents 230654093b51
children
rev   line source
adamc@484 1 (* Copyright (c) 2008, Adam Chlipala
adamc@484 2 * All rights reserved.
adamc@484 3 *
adamc@484 4 * Redistribution and use in source and binary forms, with or without
adamc@484 5 * modification, are permitted provided that the following conditions are met:
adamc@484 6 *
adamc@484 7 * - Redistributions of source code must retain the above copyright notice,
adamc@484 8 * this list of conditions and the following disclaimer.
adamc@484 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@484 10 * this list of conditions and the following disclaimer in the documentation
adamc@484 11 * and/or other materials provided with the distribution.
adamc@484 12 * - The names of contributors may not be used to endorse or promote products
adamc@484 13 * derived from this software without specific prior written permission.
adamc@484 14 *
adamc@484 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@484 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@484 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@484 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@484 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@484 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@484 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@484 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@484 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@484 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@484 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@484 26 *)
adamc@484 27
adamc@484 28 structure Defunc :> DEFUNC = struct
adamc@484 29
adamc@484 30 open Core
adamc@484 31
adamc@484 32 structure E = CoreEnv
adamc@484 33 structure U = CoreUtil
adamc@484 34
adamc@484 35 structure IS = IntBinarySet
adamc@484 36
adamc@484 37 val functionInside = U.Con.exists {kind = fn _ => false,
adamc@484 38 con = fn TFun _ => true
adamc@484 39 | CFfi ("Basis", "transaction") => true
adamc@484 40 | _ => false}
adamc@484 41
adamc@626 42 val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs,
adamc@484 43 con = fn (_, _, xs) => xs,
adamc@484 44 exp = fn (bound, e, xs) =>
adamc@484 45 case e of
adamc@484 46 ERel x =>
adamc@484 47 if x >= bound then
adamc@484 48 IS.add (xs, x - bound)
adamc@484 49 else
adamc@484 50 xs
adamc@484 51 | _ => xs,
adamc@484 52 bind = fn (bound, b) =>
adamc@484 53 case b of
adamc@484 54 U.Exp.RelE _ => bound + 1
adamc@484 55 | _ => bound}
adamc@484 56 0 IS.empty
adamc@484 57
adamc@484 58 fun positionOf (v : int, ls) =
adamc@484 59 let
adamc@484 60 fun pof (pos, ls) =
adamc@484 61 case ls of
adamc@484 62 [] => raise Fail "Defunc.positionOf"
adamc@484 63 | v' :: ls' =>
adamc@484 64 if v = v' then
adamc@484 65 pos
adamc@484 66 else
adamc@484 67 pof (pos + 1, ls')
adamc@484 68 in
adamc@484 69 pof (0, ls)
adamc@484 70 end
adamc@484 71
adamc@484 72 fun squish fvs =
adamc@626 73 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@484 74 con = fn _ => fn c => c,
adamc@484 75 exp = fn bound => fn e =>
adamc@484 76 case e of
adamc@484 77 ERel x =>
adamc@484 78 if x >= bound then
adamc@484 79 ERel (positionOf (x - bound, fvs) + bound)
adamc@484 80 else
adamc@484 81 e
adamc@484 82 | _ => e,
adamc@484 83 bind = fn (bound, b) =>
adamc@484 84 case b of
adamc@484 85 U.Exp.RelE _ => bound + 1
adamc@484 86 | _ => bound}
adamc@484 87 0
adamc@484 88
adamc@484 89 fun default (_, x, st) = (x, st)
adamc@484 90
adamc@484 91 datatype 'a search =
adamc@484 92 Yes
adamc@484 93 | No
adamc@484 94 | Maybe of 'a
adamc@484 95
adamc@484 96 structure EK = struct
adamc@484 97 type ord_key = exp
adamc@484 98 val compare = U.Exp.compare
adamc@484 99 end
adamc@484 100
adamc@484 101 structure EM = BinaryMapFn(EK)
adamc@484 102
adamc@484 103 type state = {
adamc@484 104 maxName : int,
adamc@484 105 funcs : int EM.map,
adamc@484 106 vis : (string * int * con * exp * string) list
adamc@484 107 }
adamc@484 108
adamc@484 109 fun exp (env, e, st) =
adamc@484 110 case e of
adamc@484 111 ERecord xes =>
adamc@484 112 let
adamc@484 113 val (xes, st) =
adamc@484 114 ListUtil.foldlMap
adamc@484 115 (fn (tup as (fnam as (CName x, loc), e, xt), st) =>
adamc@485 116 if (x <> "Link" andalso x <> "Action")
adamc@485 117 orelse case #1 e of
adamc@485 118 ENamed _ => true
adamc@485 119 | _ => false then
adamc@484 120 (tup, st)
adamc@484 121 else
adamc@484 122 let
adamc@484 123 fun needsAttention (e, _) =
adamc@484 124 case e of
adamc@484 125 ENamed f => Maybe (#2 (E.lookupENamed env f))
adamc@484 126 | EApp (f, _) =>
adamc@484 127 (case needsAttention f of
adamc@484 128 No => No
adamc@484 129 | Yes => Yes
adamc@484 130 | Maybe t =>
adamc@484 131 case t of
adamc@484 132 (TFun (dom, _), _) =>
adamc@484 133 if functionInside dom then
adamc@484 134 Yes
adamc@484 135 else
adamc@484 136 No
adamc@484 137 | _ => No)
adamc@484 138 | _ => No
adamc@484 139
adamc@484 140 fun headSymbol (e, _) =
adamc@484 141 case e of
adamc@484 142 ENamed f => f
adamc@484 143 | EApp (e, _) => headSymbol e
adamc@484 144 | _ => raise Fail "Defunc: headSymbol"
adamc@484 145
adamc@484 146 fun rtype (e, _) =
adamc@484 147 case e of
adamc@484 148 ENamed f => #2 (E.lookupENamed env f)
adamc@484 149 | EApp (f, _) =>
adamc@484 150 (case rtype f of
adamc@484 151 (TFun (_, ran), _) => ran
adamc@484 152 | _ => raise Fail "Defunc: rtype [1]")
adamc@484 153 | _ => raise Fail "Defunc: rtype [2]"
adamc@484 154 in
adamc@484 155 (*Print.prefaces "Found one!"
adamc@484 156 [("e", CorePrint.p_exp env e)];*)
adamc@484 157 case needsAttention e of
adamc@484 158 Yes =>
adamc@484 159 let
adamc@484 160 (*val () = print "Yes\n"*)
adamc@484 161 val f = headSymbol e
adamc@484 162
adamc@484 163 val fvs = IS.listItems (freeVars e)
adamc@484 164
adamc@484 165 val e = squish fvs e
adamc@484 166 val (e, t) = foldl (fn (n, (e, t)) =>
adamc@484 167 let
adamc@484 168 val (x, xt) = E.lookupERel env n
adamc@484 169 in
adamc@484 170 ((EAbs (x, xt, t, e), loc),
adamc@484 171 (TFun (xt, t), loc))
adamc@484 172 end)
adamc@484 173 (e, rtype e) fvs
adamc@484 174
adamc@484 175 val (f', st) =
adamc@484 176 case EM.find (#funcs st, e) of
adamc@484 177 SOME f' => (f', st)
adamc@484 178 | NONE =>
adamc@484 179 let
adamc@484 180 val (fx, _, _, tag) = E.lookupENamed env f
adamc@484 181 val f' = #maxName st
adamc@484 182
adamc@484 183 val vi = (fx, f', t, e, tag)
adamc@484 184 in
adamc@484 185 (f', {maxName = f' + 1,
adamc@484 186 funcs = EM.insert (#funcs st, e, f'),
adamc@484 187 vis = vi :: #vis st})
adamc@484 188 end
adamc@484 189
adamc@484 190 val e = foldr (fn (n, e) =>
adamc@484 191 (EApp (e, (ERel n, loc)), loc))
adamc@484 192 (ENamed f', loc) fvs
adamc@484 193 in
adamc@484 194 (*app (fn n => Print.prefaces
adamc@484 195 "Free"
adamc@484 196 [("n", CorePrint.p_exp env (ERel n, ErrorMsg.dummySpan))])
adamc@484 197 fvs;
adamc@484 198 Print.prefaces "Squished"
adamc@484 199 [("e", CorePrint.p_exp CoreEnv.empty e)];*)
adamc@484 200
adamc@484 201 ((fnam, e, xt), st)
adamc@484 202 end
adamc@484 203 | _ => (tup, st)
adamc@484 204 end
adamc@484 205 | (tup, st) => (tup, st))
adamc@484 206 st xes
adamc@484 207 in
adamc@484 208 (ERecord xes, st)
adamc@484 209 end
adamc@484 210 | _ => (e, st)
adamc@484 211
adamc@484 212 fun bind (env, b) =
adamc@484 213 case b of
adamc@626 214 U.Decl.RelK x => E.pushKRel env x
adamc@626 215 | U.Decl.RelC (x, k) => E.pushCRel env x k
adamc@484 216 | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
adamc@484 217 | U.Decl.RelE (x, t) => E.pushERel env x t
adamc@484 218 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
adamc@484 219
adamc@626 220 fun doDecl env = U.Decl.foldMapB {kind = default,
adamc@484 221 con = default,
adamc@484 222 exp = exp,
adamc@484 223 decl = default,
adamc@484 224 bind = bind}
adamc@484 225 env
adamc@484 226
adamc@484 227 fun defunc file =
adamc@484 228 let
adamc@484 229 fun doDecl' (d, (env, st)) =
adamc@484 230 let
adamc@484 231 val env = E.declBinds env d
adamc@484 232
adamc@484 233 val (d, st) = doDecl env st d
adamc@484 234
adamc@484 235 val ds =
adamc@484 236 case #vis st of
adamc@484 237 [] => [d]
adamc@484 238 | vis =>
adamc@484 239 case d of
adamc@484 240 (DValRec vis', loc) => [(DValRec (vis' @ vis), loc)]
adamc@484 241 | _ => [(DValRec vis, #2 d), d]
adamc@484 242 in
adamc@484 243 (ds,
adamc@484 244 (env,
adamc@484 245 {maxName = #maxName st,
adamc@484 246 funcs = #funcs st,
adamc@484 247 vis = []}))
adamc@484 248 end
adamc@484 249
adamc@484 250 val (file, _) = ListUtil.foldlMapConcat doDecl'
adamc@484 251 (E.empty,
adamc@484 252 {maxName = U.File.maxName file + 1,
adamc@484 253 funcs = EM.empty,
adamc@484 254 vis = []})
adamc@484 255 file
adamc@484 256 in
adamc@484 257 file
adamc@484 258 end
adamc@484 259
adamc@484 260 end