Mercurial > urweb

annotate src/cloconv.sml @ 79:37847b504cc6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More hardcore unification
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Jun 2008 11:20:34 -0400
parents 144d082b47ae
children 40d146f467c5
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@74 58 (case Int.compare (xn', xn) of
adamc@74 59 EQUAL => #1 rep
adamc@74 60 | GREATER => L'.ERel (xn' - 1)
adamc@74 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@52 72 | L.TFfi mx => (L'.TFfi mx, loc)
adamc@26 73
adamc@26 74 structure Ds :> sig
adamc@26 75 type t
adamc@26 76
adamc@26 77 val empty : t
adamc@26 78
adamc@26 79 val exp : t -> string * int * L'.typ * L'.exp -> t
adamc@26 80 val func : t -> string * L'.typ * L'.typ * L'.exp -> t * int
adamc@26 81 val decls : t -> L'.decl list
adamc@26 82
adamc@26 83 val enter : t -> t
adamc@26 84 val used : t * int -> t
adamc@26 85 val leave : t -> t
adamc@26 86 val listUsed : t -> int list
adamc@26 87 end = struct
adamc@26 88
adamc@26 89 type t = int * L'.decl list * IS.set
adamc@26 90
adamc@26 91 val empty = (0, [], IS.empty)
adamc@26 92
adamc@26 93 fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm)
adamc@26 94
adamc@26 95 fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) =
adamc@26 96 ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc)
adamc@26 97
adamc@26 98 fun decls (_, ds, _) = rev ds
adamc@26 99
adamc@26 100 fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm)
adamc@26 101 fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n))
adamc@26 102 fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm))
adamc@26 103
adamc@26 104 fun listUsed (_, _, vm) = IS.listItems vm
adamc@26 105
adamc@26 106 end
adamc@26 107
adamc@26 108
adamc@26 109 fun ccExp env ((e, loc), D) =
adamc@26 110 case e of
adamc@26 111 L.EPrim p => ((L'.EPrim p, loc), D)
adamc@26 112 | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n))
adamc@26 113 | L.ENamed n => ((L'.ENamed n, loc), D)
adamc@52 114 | L.EFfi mx => ((L'.EFfi mx, loc), D)
adamc@52 115 | L.EFfiApp (m, x, es) =>
adamc@52 116 let
adamc@52 117 val (es, D) = ListUtil.foldlMap (ccExp env) D es
adamc@52 118 in
adamc@52 119 ((L'.EFfiApp (m, x, es), loc), D)
adamc@52 120 end
adamc@26 121 | L.EApp (e1, e2) =>
adamc@26 122 let
adamc@26 123 val (e1, D) = ccExp env (e1, D)
adamc@26 124 val (e2, D) = ccExp env (e2, D)
adamc@26 125 in
adamc@29 126 ((L'.ELet ([("closure", (L'.TTop, loc), e1),
adamc@29 127 ("arg", (L'.TTop, loc), liftExpInExp 0 e2),
adamc@29 128 ("code", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "func"), loc)),
adamc@29 129 ("env", (L'.TTop, loc), (L'.EField ((L'.ERel 2, loc), "env"), loc))],
adamc@26 130 (L'.EApp ((L'.ERel 1, loc),
adamc@29 131 (L'.ERecord [("env", (L'.ERel 0, loc), (L'.TTop, loc)),
adamc@29 132 ("arg", (L'.ERel 2, loc), (L'.TTop, loc))], loc)), loc)), loc), D)
adamc@26 133 end
adamc@26 134 | L.EAbs (x, dom, ran, e) =>
adamc@26 135 let
adamc@26 136 val dom = ccTyp dom
adamc@26 137 val ran = ccTyp ran
adamc@26 138 val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D)
adamc@26 139 val ns = Ds.listUsed D
adamc@26 140 val ns = List.filter (fn n => n <> 0) ns
adamc@26 141 val D = Ds.leave D
adamc@26 142
adamc@26 143 (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e)
adamc@26 144 val () = List.app (fn (x, t) => preface ("Bound", box [string x,
adamc@26 145 space,
adamc@26 146 string ":",
adamc@26 147 space,
adamc@26 148 FlatPrint.p_typ env t]))
adamc@26 149 (E.listERels env)
adamc@26 150 val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom)
adamc@26 151 (L'.ERel n, loc))) ns*)
adamc@26 152 val body = foldl (fn (n, e) =>
adamc@26 153 subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e)
adamc@26 154 e ns
adamc@26 155 (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*)
adamc@29 156 val body = (L'.ELet ([("env", (L'.TTop, loc), (L'.EField ((L'.ERel 0, loc), "env"), loc)),
adamc@29 157 ("arg", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
adamc@26 158 body), loc)
adamc@26 159
adamc@26 160 val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc)
adamc@26 161 val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
adamc@26 162 in
adamc@29 163 ((L'.ERecord [("code", (L'.ECode fi, loc), (L'.TTop, loc)),
adamc@26 164 ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n,
adamc@29 165 (L'.ERel (n-1), loc),
adamc@29 166 #2 (E.lookupERel env (n-1)))) ns), loc),
adamc@29 167 envT)], loc), D)
adamc@26 168 end
adamc@26 169
adamc@26 170 | L.ERecord xes =>
adamc@26 171 let
adamc@29 172 val (xes, D) = ListUtil.foldlMap (fn ((x, e, t), D) =>
adamc@26 173 let
adamc@26 174 val (e, D) = ccExp env (e, D)
adamc@26 175 in
adamc@29 176 ((x, e, ccTyp t), D)
adamc@26 177 end) D xes
adamc@26 178 in
adamc@26 179 ((L'.ERecord xes, loc), D)
adamc@26 180 end
adamc@26 181 | L.EField (e1, x) =>
adamc@26 182 let
adamc@26 183 val (e1, D) = ccExp env (e1, D)
adamc@26 184 in
adamc@26 185 ((L'.EField (e1, x), loc), D)
adamc@26 186 end
adamc@26 187
adamc@26 188 fun ccDecl ((d, loc), D) =
adamc@26 189 case d of
adamc@26 190 L.DVal (x, n, t, e) =>
adamc@26 191 let
adamc@26 192 val t = ccTyp t
adamc@56 193 val (e, D) = ccExp E.empty (e, D)
adamc@26 194 in
adamc@26 195 Ds.exp D (x, n, t, e)
adamc@26 196 end
adamc@26 197
adamc@26 198 fun cloconv ds =
adamc@26 199 let
adamc@26 200 val D = foldl ccDecl Ds.empty ds
adamc@26 201 in
adamc@26 202 Ds.decls D
adamc@26 203 end
adamc@26 204
adamc@26 205 end