Mercurial > urweb

comparison src/reduce.sml @ 509:140c68046598

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most exp rules for new Reduce
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 12:59:32 -0500
parents 04053089878a
children c644ec94866d
comparison
equal deleted inserted replaced
508:04053089878a 509:140c68046598
57 fun find (n', env, lift) = 57 fun find (n', env, lift) =
58 if n' = 0 then 58 if n' = 0 then
59 case env of 59 case env of
60 UnknownC :: _ => (CRel (n + lift), loc) 60 UnknownC :: _ => (CRel (n + lift), loc)
61 | KnownC c :: _ => con (Lift (lift, 0) :: env) c 61 | KnownC c :: _ => con (Lift (lift, 0) :: env) c
62 | Lift (lift', _) :: rest => find (0, rest, lift + lift')
62 | _ => raise Fail "Reduce.con: CRel [1]" 63 | _ => raise Fail "Reduce.con: CRel [1]"
63 else 64 else
64 case env of 65 case env of
65 UnknownC :: rest => find (n' - 1, rest, lift + 1) 66 UnknownC :: rest => find (n' - 1, rest, lift + 1)
66 | KnownC _ :: rest => find (n' - 1, rest, lift) 67 | KnownC _ :: rest => find (n' - 1, rest, lift)
67 | UnknownE :: rest => find (n' - 1, rest, lift) 68 | UnknownE :: rest => find (n' - 1, rest, lift)
68 | KnownE _ :: rest => find (n' - 1, rest, lift) 69 | KnownE _ :: rest => find (n' - 1, rest, lift)
69 | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift') 70 | Lift (lift', _) :: rest => find (n', rest, lift + lift')
70 | [] => raise Fail "Reduce.con: CRel [2]" 71 | [] => raise Fail "Reduce.con: CRel [2]"
71 in 72 in
72 find (n, env, 0) 73 find (n, env, 0)
73 end 74 end
74 | CNamed n => 75 | CNamed n =>
123 case #1 c of 124 case #1 c of
124 CTuple cs => List.nth (cs, n - 1) 125 CTuple cs => List.nth (cs, n - 1)
125 | _ => (CProj (c, n), loc) 126 | _ => (CProj (c, n), loc)
126 end 127 end
127 128
128 fun exp env e = e 129 fun patCon pc =
130 case pc of
131 PConVar _ => pc
132 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
133 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
134 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
135 kind = kind}
136
137
138 val k = (KType, ErrorMsg.dummySpan)
139 fun doPart e (this as (x, t), rest) =
140 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
141 this :: rest)
142
143 fun exp env (all as (e, loc)) =
144 case e of
145 EPrim _ => all
146 | ERel n =>
147 let
148 fun find (n', env, liftC, liftE) =
149 if n' = 0 then
150 case env of
151 UnknownE :: _ => (ERel (n + liftE), loc)
152 | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e
153 | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE')
154 | _ => raise Fail "Reduce.exp: ERel [1]"
155 else
156 case env of
157 UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE)
158 | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE)
159 | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1)
160 | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE)
161 | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE')
162 | [] => raise Fail "Reduce.exp: ERel [2]"
163 in
164 find (n, env, 0, 0)
165 end
166 | ENamed n =>
167 (case IM.find (namedE, n) of
168 NONE => all
169 | SOME e => e)
170 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
171 map (con env) cs, Option.map (exp env) eo), loc)
172 | EFfi _ => all
173 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
174
175 | EApp (e1, e2) =>
176 let
177 val e1 = exp env e1
178 val e2 = exp env e2
179 in
180 case #1 e1 of
181 EAbs (_, _, _, b) => exp (KnownE e2 :: env) b
182 | _ => (EApp (e1, e2), loc)
183 end
184
185 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
186
187 | ECApp (e, c) =>
188 let
189 val e = exp env e
190 val c = con env c
191 in
192 case #1 e of
193 ECAbs (_, _, b) => exp (KnownC c :: env) b
194 | _ => (ECApp (e, c), loc)
195 end
196
197 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
198
199 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
200 | EField (e, c, {field, rest}) =>
201 let
202 val e = exp env e
203 val c = con env c
204
205 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
206 in
207 case (#1 e, #1 c) of
208 (ERecord xcs, CName x) =>
209 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
210 NONE => default ()
211 | SOME (_, e, _) => e)
212 | _ => default ()
213 end
214
215 | EConcat (e1, c1, e2, c2) =>
216 let
217 val e1 = exp env e1
218 val e2 = exp env e2
219 in
220 case (#1 e1, #1 e2) of
221 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
222 | _ =>
223 let
224 val c1 = con env c1
225 val c2 = con env c2
226 in
227 case (#1 c1, #1 c2) of
228 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
229 let
230 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
231 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
232 in
233 exp env (ERecord (xes1 @ xes2), loc)
234 end
235 | _ => (EConcat (e1, c1, e2, c2), loc)
236 end
237 end
238
239 | ECut (e, c, {field, rest}) =>
240 let
241 val e = exp env e
242 val c = con env c
243
244 fun default () =
245 let
246 val rest = con env rest
247 in
248 case #1 rest of
249 CRecord (k, xcs) =>
250 let
251 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
252 in
253 exp env (ERecord xes, loc)
254 end
255 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
256 end
257 in
258 case (#1 e, #1 c) of
259 (ERecord xes, CName x) =>
260 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
261 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
262 | _ => raise Fail "Reduce: ECut") xes), loc)
263 else
264 default ()
265 | _ => default ()
266 end
267
268 | ECutMulti (e, c, {rest}) =>
269 let
270 val e = exp env e
271 val c = con env c
272
273 fun default () =
274 let
275 val rest = con env rest
276 in
277 case #1 rest of
278 CRecord (k, xcs) =>
279 let
280 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
281 in
282 exp env (ERecord xes, loc)
283 end
284 | _ => (ECutMulti (e, c, {rest = rest}), loc)
285 end
286 in
287 case (#1 e, #1 c) of
288 (ERecord xes, CRecord (_, xcs)) =>
289 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
290 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
291 (ERecord (List.filter (fn ((CName x', _), _, _) =>
292 List.all (fn ((CName x, _), _) => x' <> x
293 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
294 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
295 else
296 default ()
297 | _ => default ()
298 end
299
300 | EFold _ => all
301
302 | ECase (e, pes, {disc, result}) =>
303 let
304 fun patBinds (p, _) =
305 case p of
306 PWild => 0
307 | PVar _ => 1
308 | PPrim _ => 0
309 | PCon (_, _, _, NONE) => 0
310 | PCon (_, _, _, SOME p) => patBinds p
311 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
312
313 fun pat (all as (p, loc)) =
314 case p of
315 PWild => all
316 | PVar (x, t) => (PVar (x, con env t), loc)
317 | PPrim _ => all
318 | PCon (dk, pc, cs, po) =>
319 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
320 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
321 in
322 (ECase (exp env e,
323 map (fn (p, e) => (pat p,
324 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
325 pes, {disc = con env disc, result = con env result}), loc)
326 end
327
328 | EWrite e => (EWrite (exp env e), loc)
329 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
330
331 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
129 in 332 in
130 {con = con, exp = exp} 333 {con = con, exp = exp}
131 end 334 end
132 335
133 fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c 336 fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c
134 fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e 337 fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e
135 338
136 fun reduce file = 339 fun reduce file =
137 let 340 let
138 fun doDecl (d as (_, loc), st as (namedC, namedE)) = 341 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
139 case #1 d of 342 case #1 d of
140 DCon (x, n, k, c) => 343 DCon (x, n, k, c) =>
141 let 344 let
142 val c = con namedC c 345 val c = con namedC [] c
143 in 346 in
144 ((DCon (x, n, k, c), loc), 347 ((DCon (x, n, k, c), loc),
145 (IM.insert (namedC, n, c), namedE)) 348 (IM.insert (namedC, n, c), namedE))
146 end 349 end
147 | DDatatype (x, n, ps, cs) => 350 | DDatatype (x, n, ps, cs) =>
148 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc), 351 let
149 st) 352 val env = map (fn _ => UnknownC) ps
353 in
354 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc),
355 st)
356 end
150 | DVal (x, n, t, e, s) => 357 | DVal (x, n, t, e, s) =>
151 let 358 let
152 val t = con namedC t 359 val t = con namedC [] t
153 val e = exp (namedC, namedE) e 360 val e = exp (namedC, namedE) [] e
154 in 361 in
155 ((DVal (x, n, t, e, s), loc), 362 ((DVal (x, n, t, e, s), loc),
156 (namedC, IM.insert (namedE, n, e))) 363 (namedC, IM.insert (namedE, n, e)))
157 end 364 end
158 | DValRec vis => 365 | DValRec vis =>
159 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc), 366 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc),
160 st) 367 st)
161 | DExport _ => (d, st) 368 | DExport _ => (d, st)
162 | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st) 369 | DTable (s, n, c, s') => ((DTable (s, n, con namedC [] c, s'), loc), st)
163 | DSequence _ => (d, st) 370 | DSequence _ => (d, st)
164 | DDatabase _ => (d, st) 371 | DDatabase _ => (d, st)
165 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st) 372 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
166 373
167 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file 374 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
168 in 375 in
169 file 376 file
170 end 377 end