# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1212939168 14400
# Node ID 6049e2193bf29944c3b8fbb9e7ae7391c22f5a2e
# Parent  d89477f07c1ee006530dd8c43179c72fc8e7e55d
Lifting cons in ElabEnv

diff -r d89477f07c1e -r 6049e2193bf2 src/elab_env.sig
--- a/src/elab_env.sig	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elab_env.sig	Sun Jun 08 11:32:48 2008 -0400
@@ -27,6 +27,9 @@
 
 signature ELAB_ENV = sig
 
+    exception SynUnif
+    val liftConInCon : int -> Elab.con -> Elab.con
+
     type env
 
     val empty : env
@@ -57,4 +60,6 @@
                                                  
     val lookupE : env -> string -> Elab.con var
 
+    val declBinds : env -> Elab.decl -> env
+
 end
diff -r d89477f07c1e -r 6049e2193bf2 src/elab_env.sml
--- a/src/elab_env.sml	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elab_env.sml	Sun Jun 08 11:32:48 2008 -0400
@@ -29,6 +29,9 @@
 
 open Elab
 
+structure L' = Elab
+structure U = ElabUtil
+
 structure IM = IntBinaryMap
 structure SM = BinaryMapFn(struct
                            type ord_key = string
@@ -38,6 +41,30 @@
 exception UnboundRel of int
 exception UnboundNamed of int
 
+
+(* AST utility functions *)
+
+exception SynUnif
+
+val liftConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn bound => fn c =>
+                                     case c of
+                                         L'.CRel xn =>
+                                         if xn < bound then
+                                             c
+                                         else
+                                             L'.CRel (xn + 1)
+                                       | L'.CUnif _ => raise SynUnif
+                                       | _ => c,
+                bind = fn (bound, U.Con.Rel _) => bound + 1
+                        | (bound, _) => bound}
+
+val lift = liftConInCon 0
+
+
+(* Back to environments *)
+
 datatype 'a var' =
          Rel' of int * 'a
        | Named' of int * 'a
@@ -76,11 +103,11 @@
     in
         {renameC = SM.insert (renameC, x, Rel' (0, k)),
          relC = (x, k) :: #relC env,
-         namedC = #namedC env,
+         namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
 
          renameE = #renameE env,
-         relE = #relE env,
-         namedE = #namedE env}
+         relE = map (fn (x, c) => (x, lift c)) (#relE env),
+         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
     end
 
 fun lookupCRel (env : env) n =
@@ -161,4 +188,9 @@
       | SOME (Rel' x) => Rel x
       | SOME (Named' x) => Named x
 
+fun declBinds env (d, _) =
+    case d of
+        DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | DVal (x, n, t, _) => pushENamedAs env x n t
+
 end
diff -r d89477f07c1e -r 6049e2193bf2 src/elab_print.sml
--- a/src/elab_print.sml	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elab_print.sml	Sun Jun 08 11:32:48 2008 -0400
@@ -270,7 +270,7 @@
 fun p_file env file =
     let
         val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (ElabUtil.declBinds env d,
+                                             (E.declBinds env d,
                                               p_decl env d))
                              env file
     in
diff -r d89477f07c1e -r 6049e2193bf2 src/elab_util.sig
--- a/src/elab_util.sig	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elab_util.sig	Sun Jun 08 11:32:48 2008 -0400
@@ -75,6 +75,4 @@
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
 end
 
-val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env
-
 end
diff -r d89477f07c1e -r 6049e2193bf2 src/elab_util.sml
--- a/src/elab_util.sml	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elab_util.sml	Sun Jun 08 11:32:48 2008 -0400
@@ -286,11 +286,4 @@
 
 end
 
-structure E = ElabEnv
-
-fun declBinds env (d, _) =
-    case d of
-        DCon (x, n, k, c) => E.pushCNamedAs env x n k (SOME c)
-      | DVal (x, n, t, _) => E.pushENamedAs env x n t
-
 end
diff -r d89477f07c1e -r 6049e2193bf2 src/elaborate.sml
--- a/src/elaborate.sml	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/elaborate.sml	Sun Jun 08 11:32:48 2008 -0400
@@ -344,21 +344,8 @@
       | CRecordFailure =>
         eprefaces "Can't unify record constructors" []
 
-exception SynUnif
-
-val liftConInCon =
-    U.Con.mapB {kind = fn k => k,
-                con = fn bound => fn c =>
-                                     case c of
-                                         L'.CRel xn =>
-                                         if xn < bound then
-                                             c
-                                         else
-                                             L'.CRel (xn + 1)
-                                       | L'.CUnif _ => raise SynUnif
-                                       | _ => c,
-                bind = fn (bound, U.Con.Rel _) => bound + 1
-                        | (bound, _) => bound}
+exception SynUnif = E.SynUnif
+val liftConInCon = E.liftConInCon
 
 val subConInCon =
     U.Con.mapB {kind = fn k => k,
diff -r d89477f07c1e -r 6049e2193bf2 src/sources
--- a/src/sources	Fri Mar 28 17:34:57 2008 -0400
+++ b/src/sources	Sun Jun 08 11:32:48 2008 -0400
@@ -20,12 +20,12 @@
 
 elab.sml
 
+elab_util.sig
+elab_util.sml
+
 elab_env.sig
 elab_env.sml
 
-elab_util.sig
-elab_util.sml
-
 elab_print.sig
 elab_print.sml