Mercurial > urweb

comparison src/reduce.sml @ 1272:56bd4a4f6e66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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