diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-24 16:48:47 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 16:48:47 -0400 |
| commit | f9f2ae472f9c0ef861df8d087529b26b734bf191 (patch) | |
| tree | c3685cb2585037a804b6a8ab92d71c257d18418c /src | |
| parent | 7e8a4397825d3ee1addd7326104759294deff832 (diff) | |
Datatype import signature-matches abstract datatype
Diffstat (limited to 'src')
| -rw-r--r-- | src/elaborate.sml | 85 |
1 files changed, 49 insertions, 36 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index d5bae866..1753313f 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1751,44 +1751,57 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = | 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, _) => |