Factor some operations into ElabOps

4 files changed, 184 insertions, 105 deletions

diff --git a/src/elab_ops.sig b/src/elab_ops.sig
new file mode 100644
index 00000000..62af9638
--- /dev/null
+++ b/src/elab_ops.sig
@@ -0,0 +1,36 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature ELAB_OPS = sig
+
+    val liftConInCon : int -> Elab.con -> Elab.con
+    val subConInCon : int * Elab.con -> Elab.con -> Elab.con
+    val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
+
+    val hnormCon : ElabEnv.env -> Elab.con -> Elab.con
+
+end
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
new file mode 100644
index 00000000..7331d371
--- /dev/null
+++ b/src/elab_ops.sml
@@ -0,0 +1,143 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ElabOps :> ELAB_OPS = struct
+
+open Elab
+
+structure E = ElabEnv
+structure U = ElabUtil
+
+val liftConInCon = E.liftConInCon
+
+val subConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn (xn, rep) => fn c =>
+                                  case c of
+                                      CRel xn' =>
+                                      (case Int.compare (xn', xn) of
+                                           EQUAL => #1 rep
+                                         | GREATER => CRel (xn' - 1)
+                                         | LESS => c)
+                                    (*| CUnif _ => raise SynUnif*)
+                                    | _ => c,
+                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+                        | (ctx, _) => ctx}
+
+fun subStrInSgn (m1, m2) =
+    U.Sgn.map {kind = fn k => k,
+               con = fn c as CModProj (m1', ms, x) =>
+                        if m1 = m1' then
+                            CModProj (m2, ms, x)
+                        else
+                            c
+                      | c => c,
+               sgn_item = fn sgi => sgi,
+               sgn = fn sgn => sgn}
+
+
+fun hnormCon env (cAll as (c, loc)) =
+    case c of
+        CUnif (_, _, _, ref (SOME c)) => hnormCon env c
+
+      | CNamed xn =>
+        (case E.lookupCNamed env xn of
+             (_, _, SOME c') => hnormCon env c'
+           | _ => cAll)
+
+      | CModProj (n, ms, x) =>
+        let
+            val (_, sgn) = E.lookupStrNamed env n
+            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                       case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                           NONE => raise Fail "hnormCon: Unknown substructure"
+                                         | SOME sgn => ((StrProj (str, m), loc), sgn))
+                             ((StrVar n, loc), sgn) ms
+        in
+            case E.projectCon env {sgn = sgn, str = str, field = x} of
+                NONE => raise Fail "kindof: Unknown con in structure"
+              | SOME (_, NONE) => cAll
+              | SOME (_, SOME c) => hnormCon env c
+        end
+
+      | CApp (c1, c2) =>
+        (case #1 (hnormCon env c1) of
+             CAbs (x, k, cb) =>
+             let
+                 val sc = (hnormCon env (subConInCon (0, c2) cb))
+                     handle SynUnif => cAll
+                 (*val env' = E.pushCRel env x k*)
+             in
+                 (*eprefaces "Subst" [("x", Print.PD.string x),
+                                    ("cb", p_con env' cb),
+                                    ("c2", p_con env c2),
+                                    ("sc", p_con env sc)];*)
+                 sc
+             end
+           | CApp (c', i) =>
+             (case #1 (hnormCon env c') of
+                  CApp (c', f) =>
+                  (case #1 (hnormCon env c') of
+                       CFold ks =>
+                       (case #1 (hnormCon env c2) of
+                            CRecord (_, []) => hnormCon env i
+                          | CRecord (k, (x, c) :: rest) =>
+                            hnormCon env
+                                     (CApp ((CApp ((CApp (f, x), loc), c), loc),
+                                               (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
+                                                         (CRecord (k, rest), loc)), loc)), loc)
+                          | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+                            let
+                                val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+
+                                (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
+                                                   (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
+                                                             rest''), loc)), loc)*)
+                            in
+                                (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
+                                hnormCon env
+                                         (CApp ((CApp ((CApp (f, x), loc), c), loc),
+                                                   (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
+                                                             rest''), loc)), loc)
+                            end
+                          | _ => cAll)
+                     | _ => cAll)
+                | _ => cAll)
+           | _ => cAll)
+
+      | CConcat (c1, c2) =>
+        (case (hnormCon env c1, hnormCon env c2) of
+             ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
+             (CRecord (k, xcs1 @ xcs2), loc)
+           | ((CRecord (_, []), _), c2') => c2'
+           | ((CConcat (c11, c12), loc), c2') =>
+             hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
+           | _ => cAll)
+
+      | _ => cAll
+
+end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ceca9b4f..4323677d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -416,32 +416,8 @@ fun cunifyError env err =
         eprefaces "Can't unify record constructors" []
 
 exception SynUnif = E.SynUnif
-val liftConInCon = E.liftConInCon
-
-val subConInCon =
-    U.Con.mapB {kind = fn k => k,
-                con = fn (xn, rep) => fn c =>
-                                  case c of
-                                      L'.CRel xn' =>
-                                      (case Int.compare (xn', xn) of
-                                           EQUAL => #1 rep
-                                         | GREATER => L'.CRel (xn' - 1)
-                                         | LESS => c)
-                                    (*| L'.CUnif _ => raise SynUnif*)
-                                    | _ => c,
-                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
-                        | (ctx, _) => ctx}
-
-fun subStrInSgn (m1, m2) =
-    U.Sgn.map {kind = fn k => k,
-               con = fn c as L'.CModProj (m1', ms, x) =>
-                        if m1 = m1' then
-                            L'.CModProj (m2, ms, x)
-                        else
-                            c
-                      | c => c,
-               sgn_item = fn sgi => sgi,
-               sgn = fn sgn => sgn}
+
+open ElabOps
 
 type record_summary = {
      fields : (L'.con * L'.con) list,
@@ -631,85 +607,6 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
         pairOffUnifs (unifs1, unifs2)
     end
 
-and hnormCon env (cAll as (c, loc)) =
-    case c of
-        L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c
-
-      | L'.CNamed xn =>
-        (case E.lookupCNamed env xn of
-             (_, _, SOME c') => hnormCon env c'
-           | _ => cAll)
-
-      | L'.CModProj (n, ms, x) =>
-        let
-            val (_, sgn) = E.lookupStrNamed env n
-            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
-                                       case E.projectStr env {sgn = sgn, str = str, field = m} of
-                                           NONE => raise Fail "hnormCon: Unknown substructure"
-                                         | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
-                             ((L'.StrVar n, loc), sgn) ms
-        in
-            case E.projectCon env {sgn = sgn, str = str, field = x} of
-                NONE => raise Fail "kindof: Unknown con in structure"
-              | SOME (_, NONE) => cAll
-              | SOME (_, SOME c) => hnormCon env c
-        end
-
-      | L'.CApp (c1, c2) =>
-        (case #1 (hnormCon env c1) of
-             L'.CAbs (x, k, cb) =>
-             let
-                 val sc = (hnormCon env (subConInCon (0, c2) cb))
-                     handle SynUnif => cAll
-                 (*val env' = E.pushCRel env x k*)
-             in
-                 (*eprefaces "Subst" [("x", Print.PD.string x),
-                                    ("cb", p_con env' cb),
-                                    ("c2", p_con env c2),
-                                    ("sc", p_con env sc)];*)
-                 sc
-             end
-           | L'.CApp (c', i) =>
-             (case #1 (hnormCon env c') of
-                  L'.CApp (c', f) =>
-                  (case #1 (hnormCon env c') of
-                       L'.CFold ks =>
-                       (case #1 (hnormCon env c2) of
-                            L'.CRecord (_, []) => hnormCon env i
-                          | L'.CRecord (k, (x, c) :: rest) =>
-                            hnormCon env
-                                     (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
-                                               (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
-                                                         (L'.CRecord (k, rest), loc)), loc)), loc)
-                          | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') =>
-                            let
-                                val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc)
-
-                                (*val ccc = (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
-                                                   (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
-                                                             rest''), loc)), loc)*)
-                            in
-                                (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
-                                hnormCon env
-                                         (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
-                                                   (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
-                                                             rest''), loc)), loc)
-                            end
-                          | _ => cAll)
-                     | _ => cAll)
-                | _ => cAll)
-           | _ => cAll)
-
-      | L'.CConcat (c1, c2) =>
-        (case (hnormCon env c1, hnormCon env c2) of
-             ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
-             (L'.CRecord (k, xcs1 @ xcs2), loc)
-           | ((L'.CRecord (_, []), _), c2') => c2'
-           | ((L'.CConcat (c11, c12), loc), c2') =>
-             hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc)
-           | _ => cAll)
-
-      | _ => cAll
 
 and unifyCons' env c1 c2 =
     unifyCons'' env (hnormCon env c1) (hnormCon env c2)
diff --git a/src/sources b/src/sources
index 5bfb0221..03b8f344 100644
--- a/src/sources
+++ b/src/sources
@@ -32,6 +32,9 @@ elab_env.sml
 elab_print.sig
 elab_print.sml
 
+elab_ops.sig
+elab_ops.sml
+
 elaborate.sig
 elaborate.sml