Mercurial > urweb
comparison src/expl_util.sml @ 624:354800878b4d
Kind polymorphism through Explify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 16:32:56 -0500 |
parents | 588b9d16b00a |
children | 0e554bfd6d6a |
comparison
equal
deleted
inserted
replaced
623:588b9d16b00a | 624:354800878b4d |
---|---|
31 | 31 |
32 structure S = Search | 32 structure S = Search |
33 | 33 |
34 structure Kind = struct | 34 structure Kind = struct |
35 | 35 |
36 fun mapfold f = | 36 fun mapfoldB {kind, bind} = |
37 let | 37 let |
38 fun mfk k acc = | 38 fun mfk ctx k acc = |
39 S.bindP (mfk' k acc, f) | 39 S.bindP (mfk' ctx k acc, kind ctx) |
40 | 40 |
41 and mfk' (kAll as (k, loc)) = | 41 and mfk' ctx (kAll as (k, loc)) = |
42 case k of | 42 case k of |
43 KType => S.return2 kAll | 43 KType => S.return2 kAll |
44 | 44 |
45 | KArrow (k1, k2) => | 45 | KArrow (k1, k2) => |
46 S.bind2 (mfk k1, | 46 S.bind2 (mfk ctx k1, |
47 fn k1' => | 47 fn k1' => |
48 S.map2 (mfk k2, | 48 S.map2 (mfk ctx k2, |
49 fn k2' => | 49 fn k2' => |
50 (KArrow (k1', k2'), loc))) | 50 (KArrow (k1', k2'), loc))) |
51 | 51 |
52 | KName => S.return2 kAll | 52 | KName => S.return2 kAll |
53 | 53 |
54 | KRecord k => | 54 | KRecord k => |
55 S.map2 (mfk k, | 55 S.map2 (mfk ctx k, |
56 fn k' => | 56 fn k' => |
57 (KRecord k', loc)) | 57 (KRecord k', loc)) |
58 | 58 |
59 | KUnit => S.return2 kAll | 59 | KUnit => S.return2 kAll |
60 | 60 |
61 | KTuple ks => | 61 | KTuple ks => |
62 S.map2 (ListUtil.mapfold mfk ks, | 62 S.map2 (ListUtil.mapfold (mfk ctx) ks, |
63 fn ks' => | 63 fn ks' => |
64 (KTuple ks', loc)) | 64 (KTuple ks', loc)) |
65 | |
66 | KRel _ => S.return2 kAll | |
67 | KFun (x, k) => | |
68 S.map2 (mfk (bind (ctx, x)) k, | |
69 fn k' => | |
70 (KFun (x, k'), loc)) | |
65 in | 71 in |
66 mfk | 72 mfk |
67 end | 73 end |
74 | |
75 fun mapfold fk = | |
76 mapfoldB {kind = fn () => fk, | |
77 bind = fn ((), _) => ()} () | |
78 | |
79 fun mapB {kind, bind} ctx k = | |
80 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), | |
81 bind = bind} ctx k () of | |
82 S.Continue (k, ()) => k | |
83 | S.Return _ => raise Fail "ExplUtil.Kind.mapB: Impossible" | |
68 | 84 |
69 fun exists f k = | 85 fun exists f k = |
70 case mapfold (fn k => fn () => | 86 case mapfold (fn k => fn () => |
71 if f k then | 87 if f k then |
72 S.Return () | 88 S.Return () |
78 end | 94 end |
79 | 95 |
80 structure Con = struct | 96 structure Con = struct |
81 | 97 |
82 datatype binder = | 98 datatype binder = |
83 Rel of string * Expl.kind | 99 RelK of string |
84 | Named of string * Expl.kind | 100 | RelC of string * Expl.kind |
101 | NamedC of string * Expl.kind | |
85 | 102 |
86 fun mapfoldB {kind = fk, con = fc, bind} = | 103 fun mapfoldB {kind = fk, con = fc, bind} = |
87 let | 104 let |
88 val mfk = Kind.mapfold fk | 105 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} |
89 | 106 |
90 fun mfc ctx c acc = | 107 fun mfc ctx c acc = |
91 S.bindP (mfc' ctx c acc, fc ctx) | 108 S.bindP (mfc' ctx c acc, fc ctx) |
92 | 109 |
93 and mfc' ctx (cAll as (c, loc)) = | 110 and mfc' ctx (cAll as (c, loc)) = |
97 fn c1' => | 114 fn c1' => |
98 S.map2 (mfc ctx c2, | 115 S.map2 (mfc ctx c2, |
99 fn c2' => | 116 fn c2' => |
100 (TFun (c1', c2'), loc))) | 117 (TFun (c1', c2'), loc))) |
101 | TCFun (x, k, c) => | 118 | TCFun (x, k, c) => |
102 S.bind2 (mfk k, | 119 S.bind2 (mfk ctx k, |
103 fn k' => | 120 fn k' => |
104 S.map2 (mfc (bind (ctx, Rel (x, k))) c, | 121 S.map2 (mfc (bind (ctx, RelC (x, k))) c, |
105 fn c' => | 122 fn c' => |
106 (TCFun (x, k', c'), loc))) | 123 (TCFun (x, k', c'), loc))) |
107 | TRecord c => | 124 | TRecord c => |
108 S.map2 (mfc ctx c, | 125 S.map2 (mfc ctx c, |
109 fn c' => | 126 fn c' => |
117 fn c1' => | 134 fn c1' => |
118 S.map2 (mfc ctx c2, | 135 S.map2 (mfc ctx c2, |
119 fn c2' => | 136 fn c2' => |
120 (CApp (c1', c2'), loc))) | 137 (CApp (c1', c2'), loc))) |
121 | CAbs (x, k, c) => | 138 | CAbs (x, k, c) => |
122 S.bind2 (mfk k, | 139 S.bind2 (mfk ctx k, |
123 fn k' => | 140 fn k' => |
124 S.map2 (mfc (bind (ctx, Rel (x, k))) c, | 141 S.map2 (mfc (bind (ctx, RelC (x, k))) c, |
125 fn c' => | 142 fn c' => |
126 (CAbs (x, k', c'), loc))) | 143 (CAbs (x, k', c'), loc))) |
127 | 144 |
128 | CName _ => S.return2 cAll | 145 | CName _ => S.return2 cAll |
129 | 146 |
130 | CRecord (k, xcs) => | 147 | CRecord (k, xcs) => |
131 S.bind2 (mfk k, | 148 S.bind2 (mfk ctx k, |
132 fn k' => | 149 fn k' => |
133 S.map2 (ListUtil.mapfold (fn (x, c) => | 150 S.map2 (ListUtil.mapfold (fn (x, c) => |
134 S.bind2 (mfc ctx x, | 151 S.bind2 (mfc ctx x, |
135 fn x' => | 152 fn x' => |
136 S.map2 (mfc ctx c, | 153 S.map2 (mfc ctx c, |
144 fn c1' => | 161 fn c1' => |
145 S.map2 (mfc ctx c2, | 162 S.map2 (mfc ctx c2, |
146 fn c2' => | 163 fn c2' => |
147 (CConcat (c1', c2'), loc))) | 164 (CConcat (c1', c2'), loc))) |
148 | CMap (k1, k2) => | 165 | CMap (k1, k2) => |
149 S.bind2 (mfk k1, | 166 S.bind2 (mfk ctx k1, |
150 fn k1' => | 167 fn k1' => |
151 S.map2 (mfk k2, | 168 S.map2 (mfk ctx k2, |
152 fn k2' => | 169 fn k2' => |
153 (CMap (k1', k2'), loc))) | 170 (CMap (k1', k2'), loc))) |
154 | 171 |
155 | CUnit => S.return2 cAll | 172 | CUnit => S.return2 cAll |
156 | 173 |
161 | 178 |
162 | CProj (c, n) => | 179 | CProj (c, n) => |
163 S.map2 (mfc ctx c, | 180 S.map2 (mfc ctx c, |
164 fn c' => | 181 fn c' => |
165 (CProj (c', n), loc)) | 182 (CProj (c', n), loc)) |
183 | |
184 | CKAbs (x, c) => | |
185 S.map2 (mfc (bind (ctx, RelK x)) c, | |
186 fn c' => | |
187 (CKAbs (x, c'), loc)) | |
188 | CKApp (c, k) => | |
189 S.bind2 (mfc ctx c, | |
190 fn c' => | |
191 S.map2 (mfk ctx k, | |
192 fn k' => | |
193 (CKApp (c', k'), loc))) | |
194 | TKFun (x, c) => | |
195 S.map2 (mfc (bind (ctx, RelK x)) c, | |
196 fn c' => | |
197 (TKFun (x, c'), loc)) | |
166 in | 198 in |
167 mfc | 199 mfc |
168 end | 200 end |
169 | 201 |
170 fun mapfold {kind = fk, con = fc} = | 202 fun mapfold {kind = fk, con = fc} = |
171 mapfoldB {kind = fk, | 203 mapfoldB {kind = fn () => fk, |
172 con = fn () => fc, | 204 con = fn () => fc, |
173 bind = fn ((), _) => ()} () | 205 bind = fn ((), _) => ()} () |
174 | 206 |
175 fun mapB {kind, con, bind} ctx c = | 207 fun mapB {kind, con, bind} ctx c = |
176 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), | 208 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), |
177 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), | 209 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), |
178 bind = bind} ctx c () of | 210 bind = bind} ctx c () of |
179 S.Continue (c, ()) => c | 211 S.Continue (c, ()) => c |
180 | S.Return _ => raise Fail "ExplUtil.Con.mapB: Impossible" | 212 | S.Return _ => raise Fail "ExplUtil.Con.mapB: Impossible" |
181 | 213 |
202 end | 234 end |
203 | 235 |
204 structure Exp = struct | 236 structure Exp = struct |
205 | 237 |
206 datatype binder = | 238 datatype binder = |
207 RelC of string * Expl.kind | 239 RelK of string |
240 | RelC of string * Expl.kind | |
208 | NamedC of string * Expl.kind | 241 | NamedC of string * Expl.kind |
209 | RelE of string * Expl.con | 242 | RelE of string * Expl.con |
210 | NamedE of string * Expl.con | 243 | NamedE of string * Expl.con |
211 | 244 |
212 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | 245 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = |
213 let | 246 let |
214 val mfk = Kind.mapfold fk | 247 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} |
215 | 248 |
216 fun bind' (ctx, b) = | 249 fun bind' (ctx, b) = |
217 let | 250 let |
218 val b' = case b of | 251 val b' = case b of |
219 Con.Rel x => RelC x | 252 Con.RelK x => RelK x |
220 | Con.Named x => NamedC x | 253 | Con.RelC x => RelC x |
254 | Con.NamedC x => NamedC x | |
221 in | 255 in |
222 bind (ctx, b') | 256 bind (ctx, b') |
223 end | 257 end |
224 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} | 258 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} |
225 | 259 |
252 fn e' => | 286 fn e' => |
253 S.map2 (mfc ctx c, | 287 S.map2 (mfc ctx c, |
254 fn c' => | 288 fn c' => |
255 (ECApp (e', c'), loc))) | 289 (ECApp (e', c'), loc))) |
256 | ECAbs (x, k, e) => | 290 | ECAbs (x, k, e) => |
257 S.bind2 (mfk k, | 291 S.bind2 (mfk ctx k, |
258 fn k' => | 292 fn k' => |
259 S.map2 (mfe (bind (ctx, RelC (x, k))) e, | 293 S.map2 (mfe (bind (ctx, RelC (x, k))) e, |
260 fn e' => | 294 fn e' => |
261 (ECAbs (x, k', e'), loc))) | 295 (ECAbs (x, k', e'), loc))) |
262 | 296 |
336 S.bind2 (mfe ctx e1, | 370 S.bind2 (mfe ctx e1, |
337 fn e1' => | 371 fn e1' => |
338 S.map2 (mfe (bind (ctx, RelE (x, t))) e2, | 372 S.map2 (mfe (bind (ctx, RelE (x, t))) e2, |
339 fn e2' => | 373 fn e2' => |
340 (ELet (x, t', e1', e2'), loc)))) | 374 (ELet (x, t', e1', e2'), loc)))) |
375 | |
376 | EKAbs (x, e) => | |
377 S.map2 (mfe (bind (ctx, RelK x)) e, | |
378 fn e' => | |
379 (EKAbs (x, e'), loc)) | |
380 | EKApp (e, k) => | |
381 S.bind2 (mfe ctx e, | |
382 fn e' => | |
383 S.map2 (mfk ctx k, | |
384 fn k' => | |
385 (EKApp (e', k'), loc))) | |
341 in | 386 in |
342 mfe | 387 mfe |
343 end | 388 end |
344 | 389 |
345 fun mapfold {kind = fk, con = fc, exp = fe} = | 390 fun mapfold {kind = fk, con = fc, exp = fe} = |
346 mapfoldB {kind = fk, | 391 mapfoldB {kind = fn () => fk, |
347 con = fn () => fc, | 392 con = fn () => fc, |
348 exp = fn () => fe, | 393 exp = fn () => fe, |
349 bind = fn ((), _) => ()} () | 394 bind = fn ((), _) => ()} () |
350 | 395 |
351 fun exists {kind, con, exp} k = | 396 fun exists {kind, con, exp} k = |
370 end | 415 end |
371 | 416 |
372 structure Sgn = struct | 417 structure Sgn = struct |
373 | 418 |
374 datatype binder = | 419 datatype binder = |
375 RelC of string * Expl.kind | 420 RelK of string |
421 | RelC of string * Expl.kind | |
376 | NamedC of string * Expl.kind | 422 | NamedC of string * Expl.kind |
377 | Str of string * Expl.sgn | 423 | Str of string * Expl.sgn |
378 | Sgn of string * Expl.sgn | 424 | Sgn of string * Expl.sgn |
379 | 425 |
380 fun mapfoldB {kind, con, sgn_item, sgn, bind} = | 426 fun mapfoldB {kind, con, sgn_item, sgn, bind} = |
381 let | 427 let |
382 fun bind' (ctx, b) = | 428 fun bind' (ctx, b) = |
383 let | 429 let |
384 val b' = case b of | 430 val b' = case b of |
385 Con.Rel x => RelC x | 431 Con.RelK x => RelK x |
386 | Con.Named x => NamedC x | 432 | Con.RelC x => RelC x |
433 | Con.NamedC x => NamedC x | |
387 in | 434 in |
388 bind (ctx, b') | 435 bind (ctx, b') |
389 end | 436 end |
390 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} | 437 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} |
391 | 438 |
392 val kind = Kind.mapfold kind | 439 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)} |
393 | 440 |
394 fun sgi ctx si acc = | 441 fun sgi ctx si acc = |
395 S.bindP (sgi' ctx si acc, sgn_item ctx) | 442 S.bindP (sgi' ctx si acc, sgn_item ctx) |
396 | 443 |
397 and sgi' ctx (siAll as (si, loc)) = | 444 and sgi' ctx (siAll as (si, loc)) = |
398 case si of | 445 case si of |
399 SgiConAbs (x, n, k) => | 446 SgiConAbs (x, n, k) => |
400 S.map2 (kind k, | 447 S.map2 (kind ctx k, |
401 fn k' => | 448 fn k' => |
402 (SgiConAbs (x, n, k'), loc)) | 449 (SgiConAbs (x, n, k'), loc)) |
403 | SgiCon (x, n, k, c) => | 450 | SgiCon (x, n, k, c) => |
404 S.bind2 (kind k, | 451 S.bind2 (kind ctx k, |
405 fn k' => | 452 fn k' => |
406 S.map2 (con ctx c, | 453 S.map2 (con ctx c, |
407 fn c' => | 454 fn c' => |
408 (SgiCon (x, n, k', c'), loc))) | 455 (SgiCon (x, n, k', c'), loc))) |
409 | SgiDatatype (x, n, xs, xncs) => | 456 | SgiDatatype (x, n, xs, xncs) => |
480 in | 527 in |
481 sg | 528 sg |
482 end | 529 end |
483 | 530 |
484 fun mapfold {kind, con, sgn_item, sgn} = | 531 fun mapfold {kind, con, sgn_item, sgn} = |
485 mapfoldB {kind = kind, | 532 mapfoldB {kind = fn () => kind, |
486 con = fn () => con, | 533 con = fn () => con, |
487 sgn_item = fn () => sgn_item, | 534 sgn_item = fn () => sgn_item, |
488 sgn = fn () => sgn, | 535 sgn = fn () => sgn, |
489 bind = fn ((), _) => ()} () | 536 bind = fn ((), _) => ()} () |
490 | 537 |