diff src/core_env.sml @ 192:9bbf4d383381

Parametrized datatypes through corify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:59:06 -0400
parents d11754ffe252
children 8a70e2919e86
line wrap: on
line diff
--- a/src/core_env.sml	Fri Aug 08 10:28:32 2008 -0400
+++ b/src/core_env.sml	Fri Aug 08 10:59:06 2008 -0400
@@ -61,8 +61,8 @@
      relC : (string * kind) list,
      namedC : (string * kind * con option) IM.map,
 
-     datatypes : (string * (string * int * con option) list) IM.map,
-     constructors : (string * con option * int) IM.map,
+     datatypes : (string * string list * (string * int * con option) list) IM.map,
+     constructors : (string * string list * con option * int) IM.map,
 
      relE : (string * con) list,
      namedE : (string * con * exp option * string) IM.map
@@ -108,13 +108,13 @@
         NONE => raise UnboundNamed n
       | SOME x => x
 
-fun pushDatatype (env : env) x n xncs =
+fun pushDatatype (env : env) x n xs xncs =
     {relC = #relC env,
      namedC = #namedC env,
 
-     datatypes = IM.insert (#datatypes env, n, (x, xncs)),
+     datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)),
      constructors = foldl (fn ((x, n', to), constructors) =>
-                              IM.insert (constructors, n', (x, to, n)))
+                              IM.insert (constructors, n', (x, xs, to, n)))
                           (#constructors env) xncs,
      
      relE = #relE env,
@@ -162,9 +162,9 @@
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
-      | DDatatype (x, n, xncs) =>
+      | DDatatype (x, n, xs, xncs) =>
         let
-            val env = pushDatatype env x n xncs
+            val env = pushDatatype env x n xs xncs
             val env = pushCNamed env x n (KType, loc) NONE
         in
             foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""