Mercurial > urweb
diff src/reduce_local.sml @ 1062:3bc726a822fb
Shake bug fix; pattern reduction in ReduceLocal
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 08 Dec 2009 11:45:19 -0500 |
parents | dfe34fad749d |
children | b2311dfb3158 |
line wrap: on
line diff
--- a/src/reduce_local.sml Tue Dec 08 10:46:50 2009 -0500 +++ b/src/reduce_local.sml Tue Dec 08 11:45:19 2009 -0500 @@ -33,6 +33,12 @@ structure IM = IntBinaryMap +fun multiLiftExpInExp n e = + if n = 0 then + e + else + multiLiftExpInExp (n - 1) (CoreEnv.liftExpInExp 0 e) + datatype env_item = Unknown | Known of exp @@ -44,6 +50,76 @@ val deKnown = List.filter (fn Known _ => false | _ => true) +datatype result = Yes of env | No | Maybe + +fun match (env, p : pat, e : exp) = + let + val baseline = length env + + fun match (env, p, e) = + case (#1 p, #1 e) of + (PWild, _) => Yes env + | (PVar (x, t), _) => Yes (Known (multiLiftExpInExp (length env - baseline) e) :: env) + + | (PPrim p, EPrim p') => + if Prim.equal (p, p') then + Yes env + else + No + + | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => + if n1 = n2 then + Yes env + else + No + + | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) => + if n1 = n2 then + match (env, p, e) + else + No + + | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE), + ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) => + if m1 = m2 andalso con1 = con2 then + Yes env + else + No + + | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep), + ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => + if m1 = m2 andalso con1 = con2 then + match (env, p, e) + else + No + + | (PRecord xps, ERecord xes) => + if List.exists (fn ((CName _, _), _, _) => false + | _ => true) xes then + Maybe + else + let + fun consider (xps, env) = + case xps of + [] => Yes env + | (x, p, _) :: rest => + case List.find (fn ((CName x', _), _, _) => x' = x + | _ => false) xes of + NONE => No + | SOME (_, e, _) => + case match (env, p, e) of + No => No + | Maybe => Maybe + | Yes env => consider (rest, env) + in + consider (xps, env) + end + + | _ => Maybe + in + match (env, p, e) + end + fun exp env (all as (e, loc)) = case e of EPrim _ => all @@ -127,11 +203,24 @@ | PCon (_, _, _, NONE) => 0 | PCon (_, _, _, SOME p) => patBinds p | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts + + fun push () = + (ECase (exp env e, + map (fn (p, e) => (p, + exp (List.tabulate (patBinds p, + fn _ => Unknown) @ env) e)) + pes, others), loc) + + fun search pes = + case pes of + [] => push () + | (p, body) :: pes => + case match (env, p, e) of + No => search pes + | Maybe => push () + | Yes env' => exp env' body in - (ECase (exp env e, - map (fn (p, e) => (p, - exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e)) - pes, others), loc) + search pes end | EWrite e => (EWrite (exp env e), loc)