diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-09-15 12:41:54 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-15 12:41:54 -0400 |
| commit | 69bdeb0e79c7b33260111c6c6eae332d37d28d0e (patch) | |
| tree | d6603b8c61d4657448e07ca3389d291a44242adc /src/reduce.sml | |
| parent | 508ac0708d67027aa9d14138d24f4aa427a70c03 (diff) | |
Escape character constants; lift indices properly in Reduce 'case' simplification
Diffstat (limited to 'src/reduce.sml')
| -rw-r--r-- | src/reduce.sml | 123 |
1 files changed, 65 insertions, 58 deletions
diff --git a/src/reduce.sml b/src/reduce.sml index 54977432..bcd502cc 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -104,65 +104,72 @@ val deKnown = ListUtil.mapConcat (fn KnownC _ => [] datatype result = Yes of env | No | Maybe fun match (env, p : pat, e : exp) = - case (#1 p, #1 e) of - (PWild, _) => Yes env - | (PVar (x, t), _) => Yes (KnownE 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 + let + val baseline = length env + + fun match (env, p, e) = + case (#1 p, #1 e) of + (PWild, _) => Yes env + | (PVar (x, t), _) => Yes (KnownE (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 - | _ => Maybe + | (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 kindConAndExp (namedC, namedE) = let |