Mercurial > urweb

comparison src/expl_util.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 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