diff src/cjr_env.sml @ 181:31dfab1d4050

Cjrize ECon
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 11:17:33 -0400
parents 25b169416ea8
children d11754ffe252
line wrap: on
line diff
--- a/src/cjr_env.sml	Sun Aug 03 11:03:35 2008 -0400
+++ b/src/cjr_env.sml	Sun Aug 03 11:17:33 2008 -0400
@@ -39,6 +39,7 @@
 
 type env = {
      datatypes : (string * (string * int * typ option) list) IM.map,
+     constructors : (string * typ option * int) IM.map,
 
      numRelE : int,
      relE : (string * typ) list,
@@ -49,6 +50,7 @@
 
 val empty = {
     datatypes = IM.empty,
+    constructors = IM.empty,
 
     numRelE = 0,
     relE = [],
@@ -59,6 +61,9 @@
 
 fun pushDatatype (env : env) x n xncs =
     {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
+     constructors = foldl (fn ((x, n, to), constructors) =>
+                              IM.insert (constructors, n, (x, to, n)))
+                          (#constructors env) xncs,
 
      numRelE = #numRelE env,
      relE = #relE env,
@@ -71,8 +76,14 @@
         NONE => raise UnboundNamed n
       | SOME x => x
 
+fun lookupConstructor (env : env) n =
+    case IM.find (#constructors env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
 fun pushERel (env : env) x t =
     {datatypes = #datatypes env,
+     constructors = #constructors env,
 
      numRelE = #numRelE env + 1,
      relE = (x, t) :: #relE env,
@@ -90,6 +101,7 @@
 
 fun pushENamed (env : env) x n t =
     {datatypes = #datatypes env,
+     constructors = #constructors env,
 
      numRelE = #numRelE env,
      relE = #relE env,
@@ -104,6 +116,7 @@
 
 fun pushStruct (env : env) n xts =
     {datatypes = #datatypes env,
+     constructors = #constructors env,
 
      numRelE = #numRelE env,
      relE = #relE env,