diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-01 10:55:38 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 10:55:38 -0400 |
| commit | 43116f69ce9330eb09d42a25d4afc746e7c3f3ef (patch) | |
| tree | e57ed0ff271cf35d5dbf88ecb90ce150a877e454 /src/elaborate.sml | |
| parent | cc2b6499cd2ea61f8882419cc5915c3428d5f5b7 (diff) | |
Initial disjointness prover
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 4323677d..0e9696b9 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -32,6 +32,7 @@ structure L = Source structure L' = Elab structure E = ElabEnv structure U = ElabUtil +structure D = Disjoint open Print open ElabPrint @@ -73,6 +74,8 @@ fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = in case (k1, k2) of (L'.KType, L'.KType) => () + | (L'.KUnit, L'.KUnit) => () + | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => (unifyKinds' d1 d2; unifyKinds' r1 r2) @@ -199,6 +202,7 @@ fun elabKind (k, loc) = | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (elabKind k), loc) + | L.KUnit => (L'.KUnit, loc) | L.KWild => kunif loc fun foldKind (dom, ran, loc)= @@ -330,6 +334,10 @@ fun elabCon env (c, loc) = val ku = kunif loc val k = (L'.KRecord ku, loc) in + case D.prove env D.empty (c1', c2', loc) of + [] => () + | _ => raise Fail "Can't prove disjointness"; + checkKind env c1' k1 k; checkKind env c2' k2 k; ((L'.CConcat (c1', c2'), loc), k) @@ -343,6 +351,8 @@ fun elabCon env (c, loc) = foldKind (dom, ran, loc)) end + | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc)) + | L.CWild k => let val k' = elabKind k @@ -478,6 +488,8 @@ fun kindof env (c, loc) = | L'.CConcat (c, _) => kindof env c | L'.CFold (dom, ran) => foldKind (dom, ran, loc) + | L'.CUnit => (L'.KUnit, loc) + | L'.CError => kerror | L'.CUnif (_, k, _, _) => k |