Mercurial > urweb

comparison src/unpoly.sml @ 794:dc3fc3f3b834

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improving/reordering Unpoly and Especialize; pathmaps
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 May 2009 08:13:54 -0400
parents 2d64457eedb1
children 6271f0e3c272
comparison
equal deleted inserted replaced
793:3e5d1c6ae30c 794:dc3fc3f3b834
70 else 70 else
71 e 71 e
72 end 72 end
73 | _ => e} 73 | _ => e}
74 74
75 structure M = BinaryMapFn(struct
76 type ord_key = con list
77 val compare = Order.joinL U.Con.compare
78 end)
79
80 type func = {
81 kinds : kind list,
82 defs : (string * int * con * exp * string) list,
83 replacements : int M.map
84 }
85
75 type state = { 86 type state = {
76 funcs : (kind list * (string * int * con * exp * string) list) IM.map, 87 funcs : func IM.map,
77 decls : decl list, 88 decls : decl list,
78 nextName : int 89 nextName : int
79 } 90 }
80 91
81 fun kind (k, st) = (k, st) 92 fun kind (k, st) = (k, st)
84 95
85 fun exp (e, st : state) = 96 fun exp (e, st : state) =
86 case e of 97 case e of
87 ECApp _ => 98 ECApp _ =>
88 let 99 let
89 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
90
91 fun unravel (e, cargs) = 100 fun unravel (e, cargs) =
92 case e of 101 case e of
93 ECApp ((e, _), c) => unravel (e, c :: cargs) 102 ECApp ((e, _), c) => unravel (e, c :: cargs)
94 | ENamed n => SOME (n, rev cargs) 103 | ENamed n => SOME (n, rev cargs)
95 | _ => NONE 104 | _ => NONE
100 if List.exists isOpen cargs then 109 if List.exists isOpen cargs then
101 (e, st) 110 (e, st)
102 else 111 else
103 case IM.find (#funcs st, n) of 112 case IM.find (#funcs st, n) of
104 NONE => (e, st) 113 NONE => (e, st)
105 | SOME (ks, vis) => 114 | SOME {kinds = ks, defs = vis, replacements} =>
106 let 115 case M.find (replacements, cargs) of
107 val (vis, nextName) = ListUtil.foldlMap 116 SOME n => (ENamed n, st)
108 (fn ((x, n, t, e, s), nextName) => 117 | NONE =>
109 ((x, nextName, n, t, e, s), nextName + 1)) 118 let
110 (#nextName st) vis 119 val old_vis = vis
111 120 val (vis, (thisName, nextName)) =
112 fun specialize (x, n, n_old, t, e, s) = 121 ListUtil.foldlMap
113 let 122 (fn ((x, n', t, e, s), (thisName, nextName)) =>
114 fun trim (t, e, cargs) = 123 ((x, nextName, n', t, e, s),
115 case (t, e, cargs) of 124 (if n' = n then nextName else thisName,
116 ((TCFun (_, _, t), _), 125 nextName + 1)))
117 (ECAbs (_, _, e), _), 126 (0, #nextName st) vis
118 carg :: cargs) => 127
119 let 128 fun specialize (x, n, n_old, t, e, s) =
120 val t = subConInCon (length cargs, carg) t 129 let
121 val e = subConInExp (length cargs, carg) e 130 fun trim (t, e, cargs) =
122 in 131 case (t, e, cargs) of
123 trim (t, e, cargs) 132 ((TCFun (_, _, t), _),
124 end 133 (ECAbs (_, _, e), _),
125 | (_, _, []) => 134 carg :: cargs) =>
126 let 135 let
127 val e = foldl (fn ((_, n, n_old, _, _, _), e) => 136 val t = subConInCon (length cargs, carg) t
128 unpolyNamed (n_old, ENamed n) e) 137 val e = subConInExp (length cargs, carg) e
129 e vis 138 in
130 in 139 trim (t, e, cargs)
131 SOME (t, e) 140 end
132 end 141 | (_, _, []) =>
133 | _ => NONE 142 (*let
134 in 143 val e = foldl (fn ((_, n, n_old, _, _, _), e) =>
135 (*Print.prefaces "specialize" 144 unpolyNamed (n_old, ENamed n) e)
136 [("t", CorePrint.p_con CoreEnv.empty t), 145 e vis
137 ("e", CorePrint.p_exp CoreEnv.empty e), 146 in*)
138 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) 147 SOME (t, e)
139 Option.map (fn (t, e) => (x, n, n_old, t, e, s)) 148 (*end*)
140 (trim (t, e, cargs)) 149 | _ => NONE
141 end 150 in
142 151 (*Print.prefaces "specialize"
143 val vis = List.map specialize vis 152 [("t", CorePrint.p_con CoreEnv.empty t),
144 in 153 ("e", CorePrint.p_exp CoreEnv.empty e),
145 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then 154 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
146 (e, st) 155 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
147 else 156 (trim (t, e, cargs))
148 let 157 end
149 val vis = List.mapPartial (fn x => x) vis 158
150 val vis = map (fn (x, n, n_old, t, e, s) => 159 val vis = List.map specialize vis
151 (x ^ "_unpoly", n, n_old, t, e, s)) vis 160 in
152 val vis' = map (fn (x, n, _, t, e, s) => 161 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
153 (x, n, t, e, s)) vis 162 (e, st)
154 163 else
155 val ks' = List.drop (ks, length cargs) 164 let
156 in 165 val vis = List.mapPartial (fn x => x) vis
157 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of 166
158 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" 167 val vis = map (fn (x, n, n_old, t, e, s) =>
159 | SOME (_, n, _, _, _, _) => 168 (x ^ "_unpoly", n, n_old, t, e, s)) vis
160 (ENamed n, 169 val vis' = map (fn (x, n, _, t, e, s) =>
161 {funcs = foldl (fn (vi, funcs) => 170 (x, n, t, e, s)) vis
162 IM.insert (funcs, #2 vi, (ks', vis'))) 171
163 (#funcs st) vis', 172 val funcs = IM.insert (#funcs st, n,
173 {kinds = ks,
174 defs = old_vis,
175 replacements = M.insert (replacements,
176 cargs,
177 thisName)})
178
179 val ks' = List.drop (ks, length cargs)
180
181 val st = {funcs = foldl (fn (vi, funcs) =>
182 IM.insert (funcs, #2 vi,
183 {kinds = ks',
184 defs = vis',
185 replacements = M.empty}))
186 funcs vis',
187 decls = #decls st,
188 nextName = nextName}
189
190 val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
191 let
192 val (e, st) = polyExp (e, st)
193 in
194 ((x, n, t, e, s), st)
195 end)
196 st vis'
197 in
198 (ENamed thisName,
199 {funcs = #funcs st,
164 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, 200 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
165 nextName = nextName}) 201 nextName = #nextName st})
166 end 202 end
167 end 203 end
168 end 204 end
169 | _ => (e, st) 205 | _ => (e, st)
206
207 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
170 208
171 fun decl (d, st : state) = 209 fun decl (d, st : state) =
172 case d of 210 case d of
173 DValRec (vis as ((x, n, t, e, s) :: rest)) => 211 DValRec (vis as ((x, n, t, e, s) :: rest)) =>
174 let 212 let
230 in 268 in
231 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then 269 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
232 (d, st) 270 (d, st)
233 else 271 else
234 (d, {funcs = foldl (fn (vi, funcs) => 272 (d, {funcs = foldl (fn (vi, funcs) =>
235 IM.insert (funcs, #2 vi, (cargs, vis))) 273 IM.insert (funcs, #2 vi, {kinds = cargs,
274 defs = vis,
275 replacements = M.empty}))
236 (#funcs st) vis, 276 (#funcs st) vis,
237 decls = #decls st, 277 decls = #decls st,
238 nextName = #nextName st}) 278 nextName = #nextName st})
239 end 279 end
240 end 280 end