From 6855e4766fa8d07e2f3e3cd468de6c58fed0c903 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 29 Jul 2008 14:28:44 -0400
Subject: Start of unurlify for datatypes

---
 src/cjr_env.sml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'src/cjr_env.sml')

diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index 0d34b98f..88d7972f 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -38,7 +38,7 @@ exception UnboundF of int
 exception UnboundStruct of int
 
 type env = {
-     namedT : (string * typ option) IM.map,
+     datatypes : (string * (string * int * typ option) list) IM.map,
 
      numRelE : int,
      relE : (string * typ) list,
@@ -48,7 +48,7 @@ type env = {
 }
 
 val empty = {
-    namedT = IM.empty,
+    datatypes = IM.empty,
 
     numRelE = 0,
     relE = [],
@@ -57,8 +57,8 @@ val empty = {
     structs = IM.empty
 }
 
-fun pushTNamed (env : env) x n co =
-    {namedT = IM.insert (#namedT env, n, (x, co)),
+fun pushDatatype (env : env) x n xncs =
+    {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
 
      numRelE = #numRelE env,
      relE = #relE env,
@@ -66,13 +66,13 @@ fun pushTNamed (env : env) x n co =
 
      structs = #structs env}
 
-fun lookupTNamed (env : env) n =
-    case IM.find (#namedT env, n) of
+fun lookupDatatype (env : env) n =
+    case IM.find (#datatypes env, n) of
         NONE => raise UnboundNamed n
       | SOME x => x
 
 fun pushERel (env : env) x t =
-    {namedT = #namedT env,
+    {datatypes = #datatypes env,
 
      numRelE = #numRelE env + 1,
      relE = (x, t) :: #relE env,
@@ -89,7 +89,7 @@ fun countERels (env : env) = #numRelE env
 fun listERels (env : env) = #relE env
 
 fun pushENamed (env : env) x n t =
-    {namedT = #namedT env,
+    {datatypes = #datatypes env,
 
      numRelE = #numRelE env,
      relE = #relE env,
@@ -103,7 +103,7 @@ fun lookupENamed (env : env) n =
       | SOME x => x
 
 fun pushStruct (env : env) n xts =
-    {namedT = #namedT env,
+    {datatypes = #datatypes env,
 
      numRelE = #numRelE env,
      relE = #relE env,
@@ -120,10 +120,10 @@ fun declBinds env (d, loc) =
     case d of
         DDatatype (x, n, xncs) =>
         let
-            val env = pushTNamed env x n NONE
+            val env = pushDatatype env x n xncs
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TNamed n, loc)), loc))
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype n, loc)
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype n, loc)), loc))
             env xncs
         end
       | DStruct (n, xts) => pushStruct env n xts
-- 
cgit v1.2.3