Mercurial > urweb

comparison src/core_env.sml @ 192:9bbf4d383381

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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