Mercurial > urweb

annotate src/cloconv.sml @ 37:367f058aba23

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Beefier nested selfification test
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 17:14:21 -0400
parents 537db4ee89f4
children 92361a008a10
rev   line source
adamc@26 1 (* Copyright (c) 2008, Adam Chlipala
adamc@26 2 * All rights reserved.
adamc@26 3 *
adamc@26 4 * Redistribution and use in source and binary forms, with or without
adamc@26 5 * modification, are permitted provided that the following conditions are met:
adamc@26 6 *
adamc@26 7 * - Redistributions of source code must retain the above copyright notice,
adamc@26 8 * this list of conditions and the following disclaimer.
adamc@26 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@26 10 * this list of conditions and the following disclaimer in the documentation
adamc@26 11 * and/or other materials provided with the distribution.
adamc@26 12 * - The names of contributors may not be used to endorse or promote products
adamc@26 13 * derived from this software without specific prior written permission.
adamc@26 14 *
adamc@26 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@26 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@26 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@26 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@26 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@26 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@26 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@26 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@26 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@26 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@26 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@26 26 *)
adamc@26 27
adamc@26 28 structure Cloconv :> CLOCONV = struct
adamc@26 29
adamc@26 30 structure L = Mono
adamc@26 31 structure L' = Flat
adamc@26 32
adamc@26 33 structure IS = IntBinarySet
adamc@26 34
adamc@26 35 structure U = FlatUtil
adamc@26 36 structure E = FlatEnv
adamc@26 37
adamc@26 38 open Print.PD
adamc@26 39 open Print
adamc@26 40
adamc@26 41 val liftExpInExp =
adamc@26 42 U.Exp.mapB {typ = fn t => t,
adamc@26 43 exp = fn bound => fn e =>
adamc@26 44 case e of
adamc@26 45 L'.ERel xn =>
adamc@26 46 if xn < bound then
adamc@26 47 e
adamc@26 48 else
adamc@26 49 L'.ERel (xn + 1)
adamc@26 50 | _ => e,
adamc@26 51 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@26 52 | (bound, _) => bound}
adamc@26 53 val subExpInExp =
adamc@26 54 U.Exp.mapB {typ = fn t => t,
adamc@26 55 exp = fn (xn, rep) => fn e =>
adamc@26 56 case e of
adamc@26 57 L'.ERel xn' =>
adamc@26 58 if xn = xn' then
adamc@26 59 #1 rep
adamc@26 60 else
adamc@26 61 e
adamc@26 62 | _ => e,
adamc@26 63 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
adamc@26 64 | (ctx, _) => ctx}
adamc@26 65
adamc@26 66
adamc@26 67 fun ccTyp (t, loc) =
adamc@26 68 case t of
adamc@26 69 L.TFun (t1, t2) => (L'.TFun (ccTyp t1, ccTyp t2), loc)
adamc@26 70 | L.TRecord xts => (L'.TRecord (map (fn (x, t) => (x, ccTyp t)) xts), loc)
adamc@26 71 | L.TNamed n => (L'.TNamed n, loc)
adamc@26 72
adamc@26 73 structure Ds :> sig
adamc@26 74 type t
adamc@26 75
adamc@26 76 val empty : t
adamc@26 77
adamc@26 78 val exp : t -> string * int * L'.typ * L'.exp -> t
adamc@26 79 val func : t -> string * L'.typ * L'.typ * L'.exp -> t * int
adamc@26 80 val decls : t -> L'.decl list
adamc@26 81
adamc@26 82 val enter : t -> t
adamc@26 83 val used : t * int -> t
adamc@26 84 val leave : t -> t
adamc@26 85 val listUsed : t -> int list
adamc@26 86 end = struct
adamc@26 87
adamc@26 88 type t = int * L'.decl list * IS.set
adamc@26 89
adamc@26 90 val empty = (0, [], IS.empty)
adamc@26 91
adamc@26 92 fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm)
adamc@26 93
adamc@26 94 fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) =
adamc@26 95 ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc)
adamc@26 96
adamc@26 97 fun decls (_, ds, _) = rev ds
adamc@26 98
adamc@26 99 fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm)
adamc@26 100 fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n))
adamc@26 101 fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm))
adamc@26 102
adamc@26 103 fun listUsed (_, _, vm) = IS.listItems vm
adamc@26 104
adamc@26 105 end
adamc@26 106
adamc@26 107
adamc@26 108 fun ccExp env ((e, loc), D) =
adamc@26 109 case e of
adamc@26 110 L.EPrim p => ((L'.EPrim p, loc), D)
adamc@26 111 | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n))
adamc@26 112 | L.ENamed n => ((L'.ENamed n, loc), D)
adamc@26 113 | L.EApp (e1, e2) =>
adamc@26 114 let
adamc@26 115 val (e1, D) = ccExp env (e1, D)
adamc@26 116 val (e2, D) = ccExp env (e2, D)
adamc@26 117 in
adamc@29 118 ((L'.ELet ([("closure", (L'.TTop, loc), e1),
adamc@29 119 ("arg", (L'.TTop, loc), liftExpInExp 0 e2),
adamc@29 120 ("code", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "func"), loc)),
adamc@29 121 ("env", (L'.TTop, loc), (L'.EField ((L'.ERel 2, loc), "env"), loc))],
adamc@26 122 (L'.EApp ((L'.ERel 1, loc),
adamc@29 123 (L'.ERecord [("env", (L'.ERel 0, loc), (L'.TTop, loc)),
adamc@29 124 ("arg", (L'.ERel 2, loc), (L'.TTop, loc))], loc)), loc)), loc), D)
adamc@26 125 end
adamc@26 126 | L.EAbs (x, dom, ran, e) =>
adamc@26 127 let
adamc@26 128 val dom = ccTyp dom
adamc@26 129 val ran = ccTyp ran
adamc@26 130 val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D)
adamc@26 131 val ns = Ds.listUsed D
adamc@26 132 val ns = List.filter (fn n => n <> 0) ns
adamc@26 133 val D = Ds.leave D
adamc@26 134
adamc@26 135 (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e)
adamc@26 136 val () = List.app (fn (x, t) => preface ("Bound", box [string x,
adamc@26 137 space,
adamc@26 138 string ":",
adamc@26 139 space,
adamc@26 140 FlatPrint.p_typ env t]))
adamc@26 141 (E.listERels env)
adamc@26 142 val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom)
adamc@26 143 (L'.ERel n, loc))) ns*)
adamc@26 144 val body = foldl (fn (n, e) =>
adamc@26 145 subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e)
adamc@26 146 e ns
adamc@26 147 (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*)
adamc@29 148 val body = (L'.ELet ([("env", (L'.TTop, loc), (L'.EField ((L'.ERel 0, loc), "env"), loc)),
adamc@29 149 ("arg", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
adamc@26 150 body), loc)
adamc@26 151
adamc@26 152 val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc)
adamc@26 153 val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
adamc@26 154 in
adamc@29 155 ((L'.ERecord [("code", (L'.ECode fi, loc), (L'.TTop, loc)),
adamc@26 156 ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n,
adamc@29 157 (L'.ERel (n-1), loc),
adamc@29 158 #2 (E.lookupERel env (n-1)))) ns), loc),
adamc@29 159 envT)], loc), D)
adamc@26 160 end
adamc@26 161
adamc@26 162 | L.ERecord xes =>
adamc@26 163 let
adamc@29 164 val (xes, D) = ListUtil.foldlMap (fn ((x, e, t), D) =>
adamc@26 165 let
adamc@26 166 val (e, D) = ccExp env (e, D)
adamc@26 167 in
adamc@29 168 ((x, e, ccTyp t), D)
adamc@26 169 end) D xes
adamc@26 170 in
adamc@26 171 ((L'.ERecord xes, loc), D)
adamc@26 172 end
adamc@26 173 | L.EField (e1, x) =>
adamc@26 174 let
adamc@26 175 val (e1, D) = ccExp env (e1, D)
adamc@26 176 in
adamc@26 177 ((L'.EField (e1, x), loc), D)
adamc@26 178 end
adamc@26 179
adamc@26 180 fun ccDecl ((d, loc), D) =
adamc@26 181 case d of
adamc@26 182 L.DVal (x, n, t, e) =>
adamc@26 183 let
adamc@26 184 val t = ccTyp t
adamc@26 185 val (e, D) = ccExp E.basis (e, D)
adamc@26 186 in
adamc@26 187 Ds.exp D (x, n, t, e)
adamc@26 188 end
adamc@26 189
adamc@26 190 fun cloconv ds =
adamc@26 191 let
adamc@26 192 val D = foldl ccDecl Ds.empty ds
adamc@26 193 in
adamc@26 194 Ds.decls D
adamc@26 195 end
adamc@26 196
adamc@26 197 end