From 69bdeb0e79c7b33260111c6c6eae332d37d28d0e Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 15 Sep 2009 12:41:54 -0400
Subject: Escape character constants; lift indices properly in Reduce 'case'
 simplification

---
 src/reduce.sml | 123 ++++++++++++++++++++++++++++++---------------------------
 1 file changed, 65 insertions(+), 58 deletions(-)

(limited to 'src/reduce.sml')

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
-- 
cgit v1.2.3