Mercurial > urweb

comparison src/expl_env.sml @ 624:354800878b4d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kind polymorphism through Explify
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:32:56 -0500
parents d34834af4512
children 70cbdcf5989b
comparison
equal deleted inserted replaced
623:588b9d16b00a 624:354800878b4d
43 43
44 (* AST utility functions *) 44 (* AST utility functions *)
45 45
46 exception SynUnif 46 exception SynUnif
47 47
48 val liftKindInKind =
49 U.Kind.mapB {kind = fn bound => fn k =>
50 case k of
51 KRel xn =>
52 if xn < bound then
53 k
54 else
55 KRel (xn + 1)
56 | _ => k,
57 bind = fn (bound, _) => bound + 1}
58
59 val liftKindInCon =
60 U.Con.mapB {kind = fn bound => fn k =>
61 case k of
62 KRel xn =>
63 if xn < bound then
64 k
65 else
66 KRel (xn + 1)
67 | _ => k,
68 con = fn _ => fn c => c,
69 bind = fn (bound, U.Con.RelK _) => bound + 1
70 | (bound, _) => bound}
71
48 val liftConInCon = 72 val liftConInCon =
49 U.Con.mapB {kind = fn k => k, 73 U.Con.mapB {kind = fn _ => fn k => k,
50 con = fn bound => fn c => 74 con = fn bound => fn c =>
51 case c of 75 case c of
52 CRel xn => 76 CRel xn =>
53 if xn < bound then 77 if xn < bound then
54 c 78 c
55 else 79 else
56 CRel (xn + 1) 80 CRel (xn + 1)
57 (*| CUnif _ => raise SynUnif*) 81 (*| CUnif _ => raise SynUnif*)
58 | _ => c, 82 | _ => c,
59 bind = fn (bound, U.Con.Rel _) => bound + 1 83 bind = fn (bound, U.Con.RelC _) => bound + 1
60 | (bound, _) => bound} 84 | (bound, _) => bound}
61 85
62 val lift = liftConInCon 0 86 val lift = liftConInCon 0
63 87
64 88
72 NotBound 96 NotBound
73 | Rel of int * 'a 97 | Rel of int * 'a
74 | Named of int * 'a 98 | Named of int * 'a
75 99
76 type env = { 100 type env = {
77 renameC : kind var' SM.map, 101 relK : string list,
102
78 relC : (string * kind) list, 103 relC : (string * kind) list,
79 namedC : (string * kind * con option) IM.map, 104 namedC : (string * kind * con option) IM.map,
80 105
81 renameE : con var' SM.map,
82 relE : (string * con) list, 106 relE : (string * con) list,
83 namedE : (string * con) IM.map, 107 namedE : (string * con) IM.map,
84 108
85 renameSgn : (int * sgn) SM.map,
86 sgn : (string * sgn) IM.map, 109 sgn : (string * sgn) IM.map,
87 110
88 renameStr : (int * sgn) SM.map,
89 str : (string * sgn) IM.map 111 str : (string * sgn) IM.map
90 } 112 }
91 113
92 val namedCounter = ref 0 114 val namedCounter = ref 0
93 115
94 val empty = { 116 val empty = {
95 renameC = SM.empty, 117 relK = [],
118
96 relC = [], 119 relC = [],
97 namedC = IM.empty, 120 namedC = IM.empty,
98 121
99 renameE = SM.empty,
100 relE = [], 122 relE = [],
101 namedE = IM.empty, 123 namedE = IM.empty,
102 124
103 renameSgn = SM.empty,
104 sgn = IM.empty, 125 sgn = IM.empty,
105 126
106 renameStr = SM.empty,
107 str = IM.empty 127 str = IM.empty
108 } 128 }
109 129
130 fun pushKRel (env : env) x =
131 {relK = x :: #relK env,
132
133 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
134 namedC = #namedC env,
135
136 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
137 namedE = #namedE env,
138
139 sgn = #sgn env,
140
141 str = #str env
142 }
143
144 fun lookupKRel (env : env) n =
145 (List.nth (#relK env, n))
146 handle Subscript => raise UnboundRel n
147
110 fun pushCRel (env : env) x k = 148 fun pushCRel (env : env) x k =
111 let 149 {relK = #relK env,
112 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 150
113 | x => x) (#renameC env) 151 relC = (x, k) :: #relC env,
114 in 152 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
115 {renameC = SM.insert (renameC, x, Rel' (0, k)), 153
116 relC = (x, k) :: #relC env, 154 relE = map (fn (x, c) => (x, lift c)) (#relE env),
117 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 155 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
118 156
119 renameE = #renameE env, 157 sgn = #sgn env,
120 relE = map (fn (x, c) => (x, lift c)) (#relE env), 158
121 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), 159 str = #str env
122 160 }
123 renameSgn = #renameSgn env,
124 sgn = #sgn env,
125
126 renameStr = #renameStr env,
127 str = #str env
128 }
129 end
130 161
131 fun lookupCRel (env : env) n = 162 fun lookupCRel (env : env) n =
132 (List.nth (#relC env, n)) 163 (List.nth (#relC env, n))
133 handle Subscript => raise UnboundRel n 164 handle Subscript => raise UnboundRel n
134 165
135 fun pushCNamed (env : env) x n k co = 166 fun pushCNamed (env : env) x n k co =
136 {renameC = SM.insert (#renameC env, x, Named' (n, k)), 167 {relK = #relK env,
168
137 relC = #relC env, 169 relC = #relC env,
138 namedC = IM.insert (#namedC env, n, (x, k, co)), 170 namedC = IM.insert (#namedC env, n, (x, k, co)),
139 171
140 renameE = #renameE env,
141 relE = #relE env, 172 relE = #relE env,
142 namedE = #namedE env, 173 namedE = #namedE env,
143 174
144 renameSgn = #renameSgn env,
145 sgn = #sgn env, 175 sgn = #sgn env,
146 176
147 renameStr = #renameStr env,
148 str = #str env} 177 str = #str env}
149 178
150 fun lookupCNamed (env : env) n = 179 fun lookupCNamed (env : env) n =
151 case IM.find (#namedC env, n) of 180 case IM.find (#namedC env, n) of
152 NONE => raise UnboundNamed n 181 NONE => raise UnboundNamed n
153 | SOME x => x 182 | SOME x => x
154 183
155 fun pushERel (env : env) x t = 184 fun pushERel (env : env) x t =
156 let 185 {relK = #relK env,
157 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 186
158 | x => x) (#renameE env) 187 relC = #relC env,
159 in 188 namedC = #namedC env,
160 {renameC = #renameC env, 189
161 relC = #relC env, 190 relE = (x, t) :: #relE env,
162 namedC = #namedC env, 191 namedE = #namedE env,
163 192
164 renameE = SM.insert (renameE, x, Rel' (0, t)), 193 sgn = #sgn env,
165 relE = (x, t) :: #relE env, 194
166 namedE = #namedE env, 195 str = #str env}
167
168 renameSgn = #renameSgn env,
169 sgn = #sgn env,
170
171 renameStr = #renameStr env,
172 str = #str env}
173 end
174 196
175 fun lookupERel (env : env) n = 197 fun lookupERel (env : env) n =
176 (List.nth (#relE env, n)) 198 (List.nth (#relE env, n))
177 handle Subscript => raise UnboundRel n 199 handle Subscript => raise UnboundRel n
178 200
179 fun pushENamed (env : env) x n t = 201 fun pushENamed (env : env) x n t =
180 {renameC = #renameC env, 202 {relK = #relK env,
181 relC = #relC env, 203
182 namedC = #namedC env, 204 relC = #relC env,
183 205 namedC = #namedC env,
184 renameE = SM.insert (#renameE env, x, Named' (n, t)), 206
185 relE = #relE env, 207 relE = #relE env,
186 namedE = IM.insert (#namedE env, n, (x, t)), 208 namedE = IM.insert (#namedE env, n, (x, t)),
187 209
188 renameSgn = #renameSgn env,
189 sgn = #sgn env, 210 sgn = #sgn env,
190 211
191 renameStr = #renameStr env,
192 str = #str env} 212 str = #str env}
193 213
194 fun lookupENamed (env : env) n = 214 fun lookupENamed (env : env) n =
195 case IM.find (#namedE env, n) of 215 case IM.find (#namedE env, n) of
196 NONE => raise UnboundNamed n 216 NONE => raise UnboundNamed n
197 | SOME x => x 217 | SOME x => x
198 218
199 fun pushSgnNamed (env : env) x n sgis = 219 fun pushSgnNamed (env : env) x n sgis =
200 {renameC = #renameC env, 220 {relK = #relK env,
201 relC = #relC env, 221
202 namedC = #namedC env, 222 relC = #relC env,
203 223 namedC = #namedC env,
204 renameE = #renameE env, 224
205 relE = #relE env, 225 relE = #relE env,
206 namedE = #namedE env, 226 namedE = #namedE env,
207 227
208 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
209 sgn = IM.insert (#sgn env, n, (x, sgis)), 228 sgn = IM.insert (#sgn env, n, (x, sgis)),
210 229
211 renameStr = #renameStr env,
212 str = #str env} 230 str = #str env}
213 231
214 fun lookupSgnNamed (env : env) n = 232 fun lookupSgnNamed (env : env) n =
215 case IM.find (#sgn env, n) of 233 case IM.find (#sgn env, n) of
216 NONE => raise UnboundNamed n 234 NONE => raise UnboundNamed n
217 | SOME x => x 235 | SOME x => x
218 236
219 fun pushStrNamed (env : env) x n sgis = 237 fun pushStrNamed (env : env) x n sgis =
220 {renameC = #renameC env, 238 {relK = #relK env,
221 relC = #relC env, 239
222 namedC = #namedC env, 240 relC = #relC env,
223 241 namedC = #namedC env,
224 renameE = #renameE env, 242
225 relE = #relE env, 243 relE = #relE env,
226 namedE = #namedE env, 244 namedE = #namedE env,
227 245
228 renameSgn = #renameSgn env, 246 sgn = #sgn env,
229 sgn = #sgn env, 247
230
231 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
232 str = IM.insert (#str env, n, (x, sgis))} 248 str = IM.insert (#str env, n, (x, sgis))}
233 249
234 fun lookupStrNamed (env : env) n = 250 fun lookupStrNamed (env : env) n =
235 case IM.find (#str env, n) of 251 case IM.find (#str env, n) of
236 NONE => raise UnboundNamed n 252 NONE => raise UnboundNamed n