Mercurial > urweb
comparison src/reduce.sml @ 1272:56bd4a4f6e66
Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 03 Jun 2010 13:04:37 -0400 |
parents | beb67ff4c8a0 |
children | 3b22c3c67f35 |
comparison
equal
deleted
inserted
replaced
1271:503d4ec93494 | 1272:56bd4a4f6e66 |
---|---|
63 bind = fn (n, b) => | 63 bind = fn (n, b) => |
64 case b of | 64 case b of |
65 CoreUtil.Exp.RelE _ => n + 1 | 65 CoreUtil.Exp.RelE _ => n + 1 |
66 | _ => n} | 66 | _ => n} |
67 | 67 |
68 val cdangling = | |
69 CoreUtil.Exp.existsB {kind = fn _ => false, | |
70 con = fn (n, c) => | |
71 case c of | |
72 CRel n' => n' >= n | |
73 | _ => false, | |
74 exp = fn _ => false, | |
75 bind = fn (n, b) => | |
76 case b of | |
77 CoreUtil.Exp.RelC _ => n + 1 | |
78 | _ => n} | |
79 | |
68 datatype env_item = | 80 datatype env_item = |
69 UnknownK | 81 UnknownK |
70 | KnownK of kind | 82 | KnownK of kind |
71 | 83 |
72 | UnknownC | 84 | UnknownC |
82 | (_, n) => n) 0 | 94 | (_, n) => n) 0 |
83 | 95 |
84 val edepth' = foldl (fn (UnknownE, n) => n + 1 | 96 val edepth' = foldl (fn (UnknownE, n) => n + 1 |
85 | (KnownE _, n) => n + 1 | 97 | (KnownE _, n) => n + 1 |
86 | (Lift (_, _, n'), n) => n + n' | 98 | (Lift (_, _, n'), n) => n + n' |
99 | (_, n) => n) 0 | |
100 | |
101 val cdepth = foldl (fn (UnknownC, n) => n + 1 | |
102 | (KnownC _, n) => n + 1 | |
103 | (_, n) => n) 0 | |
104 | |
105 val cdepth' = foldl (fn (UnknownC, n) => n + 1 | |
106 | (KnownC _, n) => n + 1 | |
107 | (Lift (_, n', _), n) => n + n' | |
87 | (_, n) => n) 0 | 108 | (_, n) => n) 0 |
88 | 109 |
89 type env = env_item list | 110 type env = env_item list |
90 | 111 |
91 fun ei2s ei = | 112 fun ei2s ei = |
340 ("env", Print.PD.string (e2s env))]*) | 361 ("env", Print.PD.string (e2s env))]*) |
341 (*val () = if dangling (edepth env) all then | 362 (*val () = if dangling (edepth env) all then |
342 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), | 363 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), |
343 ("env", Print.PD.string (e2s env))]; | 364 ("env", Print.PD.string (e2s env))]; |
344 raise Fail "!") | 365 raise Fail "!") |
366 else | |
367 ()*) | |
368 (*val () = if cdangling (cdepth env) all then | |
369 Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all), | |
370 ("env", Print.PD.string (e2s env))] | |
345 else | 371 else |
346 ()*) | 372 ()*) |
347 | 373 |
348 val r = case e of | 374 val r = case e of |
349 EPrim _ => all | 375 EPrim _ => all |
634 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), | 660 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), |
635 ("r", CorePrint.p_exp CoreEnv.empty r)]; | 661 ("r", CorePrint.p_exp CoreEnv.empty r)]; |
636 raise Fail "!!") | 662 raise Fail "!!") |
637 else | 663 else |
638 ();*) | 664 ();*) |
665 (*if cdangling (cdepth' (deKnown env)) r then | |
666 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), | |
667 ("r", CorePrint.p_exp CoreEnv.empty r)]; | |
668 raise Fail "!!") | |
669 else | |
670 ();*) | |
639 r | 671 r |
640 end | 672 end |
641 in | 673 in |
642 {kind = kind, con = con, exp = exp} | 674 {kind = kind, con = con, exp = exp} |
643 end | 675 end |