diff src/cjr_env.sml @ 166:a991431b77eb

Start of unurlify for datatypes
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 14:28:44 -0400
parents e52dfb1e6b19
children 25b169416ea8
line wrap: on
line diff
--- a/src/cjr_env.sml	Tue Jul 29 13:50:53 2008 -0400
+++ b/src/cjr_env.sml	Tue Jul 29 14:28:44 2008 -0400
@@ -38,7 +38,7 @@
 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 @@
 }
 
 val empty = {
-    namedT = IM.empty,
+    datatypes = IM.empty,
 
     numRelE = 0,
     relE = [],
@@ -57,8 +57,8 @@
     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 @@
 
      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 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 @@
       | 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 @@
     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