Mercurial > urweb

comparison src/elaborate.sml @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 60d97de1bbe8
children 0a1baddd8ab2
comparison
equal deleted inserted replaced
81:60d97de1bbe8 82:b4f2a258e52c
30 structure P = Prim 30 structure P = Prim
31 structure L = Source 31 structure L = Source
32 structure L' = Elab 32 structure L' = Elab
33 structure E = ElabEnv 33 structure E = ElabEnv
34 structure U = ElabUtil 34 structure U = ElabUtil
35 structure D = Disjoint
35 36
36 open Print 37 open Print
37 open ElabPrint 38 open ElabPrint
38 39
39 structure SS = BinarySetFn(struct 40 structure SS = BinarySetFn(struct
71 let 72 let
72 fun err f = raise KUnify' (f (k1All, k2All)) 73 fun err f = raise KUnify' (f (k1All, k2All))
73 in 74 in
74 case (k1, k2) of 75 case (k1, k2) of
75 (L'.KType, L'.KType) => () 76 (L'.KType, L'.KType) => ()
77 | (L'.KUnit, L'.KUnit) => ()
78
76 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => 79 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
77 (unifyKinds' d1 d2; 80 (unifyKinds' d1 d2;
78 unifyKinds' r1 r2) 81 unifyKinds' r1 r2)
79 | (L'.KName, L'.KName) => () 82 | (L'.KName, L'.KName) => ()
80 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 83 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
197 case k of 200 case k of
198 L.KType => (L'.KType, loc) 201 L.KType => (L'.KType, loc)
199 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 202 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
200 | L.KName => (L'.KName, loc) 203 | L.KName => (L'.KName, loc)
201 | L.KRecord k => (L'.KRecord (elabKind k), loc) 204 | L.KRecord k => (L'.KRecord (elabKind k), loc)
205 | L.KUnit => (L'.KUnit, loc)
202 | L.KWild => kunif loc 206 | L.KWild => kunif loc
203 207
204 fun foldKind (dom, ran, loc)= 208 fun foldKind (dom, ran, loc)=
205 (L'.KArrow ((L'.KArrow ((L'.KName, loc), 209 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
206 (L'.KArrow (dom, 210 (L'.KArrow (dom,
328 val (c1', k1) = elabCon env c1 332 val (c1', k1) = elabCon env c1
329 val (c2', k2) = elabCon env c2 333 val (c2', k2) = elabCon env c2
330 val ku = kunif loc 334 val ku = kunif loc
331 val k = (L'.KRecord ku, loc) 335 val k = (L'.KRecord ku, loc)
332 in 336 in
337 case D.prove env D.empty (c1', c2', loc) of
338 [] => ()
339 | _ => raise Fail "Can't prove disjointness";
340
333 checkKind env c1' k1 k; 341 checkKind env c1' k1 k;
334 checkKind env c2' k2 k; 342 checkKind env c2' k2 k;
335 ((L'.CConcat (c1', c2'), loc), k) 343 ((L'.CConcat (c1', c2'), loc), k)
336 end 344 end
337 | L.CFold => 345 | L.CFold =>
340 val ran = kunif loc 348 val ran = kunif loc
341 in 349 in
342 ((L'.CFold (dom, ran), loc), 350 ((L'.CFold (dom, ran), loc),
343 foldKind (dom, ran, loc)) 351 foldKind (dom, ran, loc))
344 end 352 end
353
354 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc))
345 355
346 | L.CWild k => 356 | L.CWild k =>
347 let 357 let
348 val k' = elabKind k 358 val k' = elabKind k
349 in 359 in
475 | L'.CName _ => kname 485 | L'.CName _ => kname
476 486
477 | L'.CRecord (k, _) => (L'.KRecord k, loc) 487 | L'.CRecord (k, _) => (L'.KRecord k, loc)
478 | L'.CConcat (c, _) => kindof env c 488 | L'.CConcat (c, _) => kindof env c
479 | L'.CFold (dom, ran) => foldKind (dom, ran, loc) 489 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
490
491 | L'.CUnit => (L'.KUnit, loc)
480 492
481 | L'.CError => kerror 493 | L'.CError => kerror
482 | L'.CUnif (_, k, _, _) => k 494 | L'.CUnif (_, k, _, _) => k
483 495
484 fun unifyRecordCons env (c1, c2) = 496 fun unifyRecordCons env (c1, c2) =