Mercurial > urweb

comparison src/unpoly.sml @ 315:e21d0dddda09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unpoly non-recursive function
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 09:36:47 -0400
parents
children 04ebfe929a98
comparison
equal deleted inserted replaced
314:a07f476d9b61 315:e21d0dddda09
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 (* Simplify a Core program by repeating polymorphic function definitions *)
29
30 structure Unpoly :> UNPOLY = struct
31
32 open Core
33
34 structure E = CoreEnv
35 structure U = CoreUtil
36
37 structure IS = IntBinarySet
38 structure IM = IntBinaryMap
39
40
41 (** The actual specialization *)
42
43 val liftConInCon = E.liftConInCon
44 val subConInCon = E.subConInCon
45
46 val liftConInExp = E.liftConInExp
47 val subConInExp = E.subConInExp
48
49 type state = {
50 funcs : (kind list * (string * int * con * exp * string) list) IM.map,
51 decls : decl list,
52 nextName : int
53 }
54
55 fun kind (k, st) = (k, st)
56
57 fun con (c, st) = (c, st)
58
59 fun exp (e, st : state) =
60 case e of
61 ECApp _ =>
62 let
63 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
64
65 fun unravel (e, cargs) =
66 case e of
67 ECApp ((e, _), c) => unravel (e, c :: cargs)
68 | ENamed n => SOME (n, rev cargs)
69 | _ => NONE
70 in
71 case unravel (e, []) of
72 NONE => (e, st)
73 | SOME (n, cargs) =>
74 case IM.find (#funcs st, n) of
75 NONE => (e, st)
76 | SOME (ks, vis) =>
77 let
78 val (vis, nextName) = ListUtil.foldlMap
79 (fn ((x, n, t, e, s), nextName) =>
80 ((x, nextName, n, t, e, s), nextName + 1))
81 (#nextName st) vis
82
83 fun specialize (x, n, n_old, t, e, s) =
84 let
85 fun trim (t, e, cargs) =
86 case (t, e, cargs) of
87 ((TCFun (_, _, t), _),
88 (ECAbs (_, _, e), _),
89 carg :: cargs) =>
90 let
91 val t = subConInCon (length cargs, carg) t
92 val e = subConInExp (length cargs, carg) e
93 in
94 trim (t, e, cargs)
95 end
96 | (_, _, []) => SOME (t, e)
97 | _ => NONE
98 in
99 (*Print.prefaces "specialize"
100 [("t", CorePrint.p_con CoreEnv.empty t),
101 ("e", CorePrint.p_exp CoreEnv.empty e),
102 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
103 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
104 (trim (t, e, cargs))
105 end
106
107 val vis = List.map specialize vis
108 in
109 if List.exists (not o Option.isSome) vis then
110 (e, st)
111 else
112 let
113 val vis = List.mapPartial (fn x => x) vis
114 val vis' = map (fn (x, n, _, t, e, s) =>
115 (x ^ "_unpoly", n, t, e, s)) vis
116 in
117 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of
118 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record"
119 | SOME (_, n, _, _, _, _) =>
120 (ENamed n,
121 {funcs = #funcs st,
122 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
123 nextName = nextName})
124 end
125 end
126 end
127 | _ => (e, st)
128
129 fun decl (d, st : state) =
130 case d of
131 DValRec (vis as ((x, n, t, e, s) :: rest)) =>
132 let
133 fun unravel (e, cargs) =
134 case e of
135 (ECAbs (_, k, e), _) =>
136 unravel (e, k :: cargs)
137 | _ => rev cargs
138
139 val cargs = unravel (e, [])
140
141 fun unravel (e, cargs) =
142 case (e, cargs) of
143 ((ECAbs (_, k, e), _), k' :: cargs) =>
144 U.Kind.compare (k, k') = EQUAL
145 andalso unravel (e, cargs)
146 | (_, []) => true
147 | _ => false
148 in
149 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
150 (d, st)
151 else
152 let
153 val ns = IS.addList (IS.empty, map #2 vis)
154 val nargs = length cargs
155
156 fun deAbs (e, cargs) =
157 case (e, cargs) of
158 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
159 | (_, []) => e
160 | _ => raise Fail "Unpoly: deAbs"
161
162 (** Verifying lack of polymorphic recursion *)
163
164 fun kind _ = false
165 fun con _ = false
166
167 fun exp e =
168 case e of
169 ECApp (e, c) =>
170 let
171 fun isIrregular (e, pos) =
172 case #1 e of
173 ENamed n =>
174 IS.member (ns, n)
175 andalso
176 (case #1 c of
177 CRel i => i <> nargs - pos
178 | _ => true)
179 | ECApp (e, _) => isIrregular (e, pos + 1)
180 | _ => false
181 in
182 isIrregular (e, 1)
183 end
184 | ECAbs _ => true
185 | _ => false
186
187 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
188 in
189 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
190 (d, st)
191 else
192 (d, {funcs = foldl (fn (vi, funcs) =>
193 IM.insert (funcs, #2 vi, (cargs, vis)))
194 (#funcs st) vis,
195 decls = #decls st,
196 nextName = #nextName st})
197 end
198 end
199
200 | _ => (d, st)
201
202 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
203
204 fun unpoly file =
205 let
206 fun doDecl (d : decl, st : state) =
207 let
208 val (d, st) = polyDecl st d
209 in
210 (rev (d :: #decls st),
211 {funcs = #funcs st,
212 decls = [],
213 nextName = #nextName st})
214 end
215
216 val (ds, _) = ListUtil.foldlMapConcat doDecl
217 {funcs = IM.empty,
218 decls = [],
219 nextName = U.File.maxName file + 1} file
220 in
221 ds
222 end
223
224 end