Mercurial > urweb
changeset 942:280f81731426
Escape character constants; lift indices properly in Reduce 'case' simplification
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 15 Sep 2009 12:41:54 -0400 |
| parents | b8d7a47b8e0c |
| children | e2194a6793ae |
| files | src/prim.sml src/reduce.sml |
| diffstat | 2 files changed, 61 insertions(+), 54 deletions(-) [+] |
line wrap: on
line diff
--- a/src/prim.sml Tue Sep 15 12:23:42 2009 -0400 +++ b/src/prim.sml Tue Sep 15 12:41:54 2009 -0400 @@ -41,7 +41,7 @@ Int n => string (Int64.toString n) | Float n => string (Real64.toString n) | String s => box [string "\"", string (String.toString s), string "\""] - | Char ch => box [string "#\"", string (String.str ch), string "\""] + | Char ch => box [string "#\"", string (String.toString (String.str ch)), string "\""] fun int2s n = if Int64.compare (n, Int64.fromInt 0) = LESS then @@ -73,7 +73,7 @@ Int n => string (int2s n) | Float n => string (float2s n) | String s => box [string "\"", string (String.toString s), string "\""] - | Char ch => box [string "'", string (str ch), string "'"] + | Char ch => box [string "'", string (String.toString (str ch)), string "'"] fun equal x = case x of
--- a/src/reduce.sml Tue Sep 15 12:23:42 2009 -0400 +++ b/src/reduce.sml Tue Sep 15 12:41:54 2009 -0400 @@ -104,65 +104,72 @@ 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) + let + val baseline = length env - | (PPrim p, EPrim p') => - if Prim.equal (p, p') then - Yes env - else - No + 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) - | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => - if n1 = n2 then - Yes env - else - No + | (PPrim p, EPrim p') => + if Prim.equal (p, p') 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 (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => + if n1 = n2 then + Yes env + 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 (_, 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, ...}, _, SOME ep), - ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => - if m1 = m2 andalso con1 = con2 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 - | (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 + | (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 - | _ => Maybe + | (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