Mercurial > urweb
changeset 160:870e8abbe3b9
Datatype import signature-matches abstract datatype
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 24 Jul 2008 16:48:47 -0400 |
| parents | 1e382d10e832 |
| children | a5ae7b3e37a4 |
| files | src/elaborate.sml tests/datatypeMod.lac |
| diffstat | 2 files changed, 51 insertions(+), 36 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jul 24 16:41:12 2008 -0400 +++ b/src/elaborate.sml Thu Jul 24 16:48:47 2008 -0400 @@ -1751,44 +1751,57 @@ | L'.SgiDatatype (x, n2, xncs2) => seek (fn sgi1All as (sgi1, _) => - case sgi1 of - L'.SgiDatatype (x', n1, xncs1) => - let - fun mismatched ue = - (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); - SOME (env, denv)) + let + fun found (n1, xncs1) = + let + fun mismatched ue = + (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); + SOME (env, denv)) - fun good () = - let - val env = E.sgiBinds env sgi2All - val env = if n1 = n2 then - env - else - E.pushCNamedAs env x n1 (L'.KType, loc) - (SOME (L'.CNamed n1, loc)) - in - SOME (env, denv) - end + fun good () = + let + val env = E.sgiBinds env sgi2All + val env = if n1 = n2 then + env + else + E.pushCNamedAs env x n1 (L'.KType, loc) + (SOME (L'.CNamed n1, loc)) + in + SOME (env, denv) + end - fun xncBad ((x1, _, t1), (x2, _, t2)) = - String.compare (x1, x2) <> EQUAL - orelse case (t1, t2) of - (NONE, NONE) => false - | (SOME t1, SOME t2) => - not (List.null (unifyCons (env, denv) t1 t2)) - | _ => true - in - (if x = x' then - if length xncs1 <> length xncs2 - orelse ListPair.exists xncBad (xncs1, xncs2) then - mismatched NONE - else - good () - else - NONE) - handle CUnify ue => mismatched (SOME ue) - end - | _ => NONE) + fun xncBad ((x1, _, t1), (x2, _, t2)) = + String.compare (x1, x2) <> EQUAL + orelse case (t1, t2) of + (NONE, NONE) => false + | (SOME t1, SOME t2) => + not (List.null (unifyCons (env, denv) t1 t2)) + | _ => true + in + (if length xncs1 <> length xncs2 + orelse ListPair.exists xncBad (xncs1, xncs2) then + mismatched NONE + else + good ()) + handle CUnify ue => mismatched (SOME ue) + end + in + case sgi1 of + L'.SgiDatatype (x', n1, xncs1) => + if x' = x then + found (n1, xncs1) + else + NONE + | L'.SgiDatatypeImp (x', n1, m1, ms, s) => + let + val (str, sgn) = E.chaseMpath env (m1, ms) + in + case E.projectDatatype env {str = str, sgn = sgn, field = s} of + NONE => NONE + | SOME xncs1 => found (n1, xncs1) + end + | _ => NONE + end) | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) => seek (fn sgi1All as (sgi1, _) =>