Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
191:aa54250f58ac | 192:9bbf4d383381 |
---|---|
59 | 59 |
60 type env = { | 60 type env = { |
61 relC : (string * kind) list, | 61 relC : (string * kind) list, |
62 namedC : (string * kind * con option) IM.map, | 62 namedC : (string * kind * con option) IM.map, |
63 | 63 |
64 datatypes : (string * (string * int * con option) list) IM.map, | 64 datatypes : (string * string list * (string * int * con option) list) IM.map, |
65 constructors : (string * con option * int) IM.map, | 65 constructors : (string * string list * con option * int) IM.map, |
66 | 66 |
67 relE : (string * con) list, | 67 relE : (string * con) list, |
68 namedE : (string * con * exp option * string) IM.map | 68 namedE : (string * con * exp option * string) IM.map |
69 } | 69 } |
70 | 70 |
106 fun lookupCNamed (env : env) n = | 106 fun lookupCNamed (env : env) n = |
107 case IM.find (#namedC env, n) of | 107 case IM.find (#namedC env, n) of |
108 NONE => raise UnboundNamed n | 108 NONE => raise UnboundNamed n |
109 | SOME x => x | 109 | SOME x => x |
110 | 110 |
111 fun pushDatatype (env : env) x n xncs = | 111 fun pushDatatype (env : env) x n xs xncs = |
112 {relC = #relC env, | 112 {relC = #relC env, |
113 namedC = #namedC env, | 113 namedC = #namedC env, |
114 | 114 |
115 datatypes = IM.insert (#datatypes env, n, (x, xncs)), | 115 datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), |
116 constructors = foldl (fn ((x, n', to), constructors) => | 116 constructors = foldl (fn ((x, n', to), constructors) => |
117 IM.insert (constructors, n', (x, to, n))) | 117 IM.insert (constructors, n', (x, xs, to, n))) |
118 (#constructors env) xncs, | 118 (#constructors env) xncs, |
119 | 119 |
120 relE = #relE env, | 120 relE = #relE env, |
121 namedE = #namedE env} | 121 namedE = #namedE env} |
122 | 122 |
160 | SOME x => x | 160 | SOME x => x |
161 | 161 |
162 fun declBinds env (d, loc) = | 162 fun declBinds env (d, loc) = |
163 case d of | 163 case d of |
164 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) | 164 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) |
165 | DDatatype (x, n, xncs) => | 165 | DDatatype (x, n, xs, xncs) => |
166 let | 166 let |
167 val env = pushDatatype env x n xncs | 167 val env = pushDatatype env x n xs xncs |
168 val env = pushCNamed env x n (KType, loc) NONE | 168 val env = pushCNamed env x n (KType, loc) NONE |
169 in | 169 in |
170 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE "" | 170 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE "" |
171 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "") | 171 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "") |
172 env xncs | 172 env xncs |