Start of elaboration

1 files changed, 100 insertions, 0 deletions

diff --git a/src/elab_env.sml b/src/elab_env.sml
new file mode 100644
index 00000000..7b932aad
--- /dev/null
+++ b/src/elab_env.sml
@@ -0,0 +1,100 @@
+(* 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 ElabEnv :> ELAB_ENV = struct
+
+open Elab
+
+structure IM = IntBinaryMap
+structure SM = BinaryMapFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
+
+exception UnboundRel of int
+exception UnboundNamed of int
+
+datatype var' =
+         CRel' of int * kind
+       | CNamed' of int * kind
+
+datatype var =
+         CNotBound
+       | CRel of int * kind
+       | CNamed of int * kind
+
+type env = {
+     renameC : var' SM.map,
+     relC : (string * kind) list,
+     namedC : (string * kind) IM.map
+}
+
+val namedCounter = ref 0
+
+val empty = {
+    renameC = SM.empty,
+    relC = [],
+    namedC = IM.empty
+}
+
+fun pushCRel (env : env) x k =
+    let
+        val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k)
+                               | x => x) (#renameC env)
+    in
+        {renameC = SM.insert (renameC, x, CRel' (0, k)),
+         relC = (x, k) :: #relC env,
+         namedC = #namedC env}
+    end
+
+fun lookupCRel (env : env) n =
+    (List.nth (#relC env, n))
+    handle Subscript => raise UnboundRel n
+
+fun pushCNamed (env : env) x k =
+    let
+        val n = !namedCounter
+    in
+        namedCounter := n + 1;
+        ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
+          relC = #relC env,
+          namedC = IM.insert (#namedC env, n, (x, k))},
+         n)
+    end
+
+fun lookupCNamed (env : env) n =
+    case IM.find (#namedC env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun lookupC (env : env) x =
+    case SM.find (#renameC env, x) of
+        NONE => CNotBound
+      | SOME (CRel' x) => CRel x
+      | SOME (CNamed' x) => CNamed x
+
+end