Mercurial > urweb

comparison src/elaborate.sml @ 160:870e8abbe3b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
159:1e382d10e832 160:870e8abbe3b9
1749 NONE 1749 NONE
1750 | _ => NONE) 1750 | _ => NONE)
1751 1751
1752 | L'.SgiDatatype (x, n2, xncs2) => 1752 | L'.SgiDatatype (x, n2, xncs2) =>
1753 seek (fn sgi1All as (sgi1, _) => 1753 seek (fn sgi1All as (sgi1, _) =>
1754 case sgi1 of 1754 let
1755 L'.SgiDatatype (x', n1, xncs1) => 1755 fun found (n1, xncs1) =
1756 let 1756 let
1757 fun mismatched ue = 1757 fun mismatched ue =
1758 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); 1758 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
1759 SOME (env, denv)) 1759 SOME (env, denv))
1760 1760
1761 fun good () = 1761 fun good () =
1762 let 1762 let
1763 val env = E.sgiBinds env sgi2All 1763 val env = E.sgiBinds env sgi2All
1764 val env = if n1 = n2 then 1764 val env = if n1 = n2 then
1765 env 1765 env
1766 else 1766 else
1767 E.pushCNamedAs env x n1 (L'.KType, loc) 1767 E.pushCNamedAs env x n1 (L'.KType, loc)
1768 (SOME (L'.CNamed n1, loc)) 1768 (SOME (L'.CNamed n1, loc))
1769 in 1769 in
1770 SOME (env, denv) 1770 SOME (env, denv)
1771 end 1771 end
1772 1772
1773 fun xncBad ((x1, _, t1), (x2, _, t2)) = 1773 fun xncBad ((x1, _, t1), (x2, _, t2)) =
1774 String.compare (x1, x2) <> EQUAL 1774 String.compare (x1, x2) <> EQUAL
1775 orelse case (t1, t2) of 1775 orelse case (t1, t2) of
1776 (NONE, NONE) => false 1776 (NONE, NONE) => false
1777 | (SOME t1, SOME t2) => 1777 | (SOME t1, SOME t2) =>
1778 not (List.null (unifyCons (env, denv) t1 t2)) 1778 not (List.null (unifyCons (env, denv) t1 t2))
1779 | _ => true 1779 | _ => true
1780 in 1780 in
1781 (if x = x' then 1781 (if length xncs1 <> length xncs2
1782 if length xncs1 <> length xncs2 1782 orelse ListPair.exists xncBad (xncs1, xncs2) then
1783 orelse ListPair.exists xncBad (xncs1, xncs2) then 1783 mismatched NONE
1784 mismatched NONE 1784 else
1785 else 1785 good ())
1786 good () 1786 handle CUnify ue => mismatched (SOME ue)
1787 else 1787 end
1788 NONE) 1788 in
1789 handle CUnify ue => mismatched (SOME ue) 1789 case sgi1 of
1790 end 1790 L'.SgiDatatype (x', n1, xncs1) =>
1791 | _ => NONE) 1791 if x' = x then
1792 found (n1, xncs1)
1793 else
1794 NONE
1795 | L'.SgiDatatypeImp (x', n1, m1, ms, s) =>
1796 let
1797 val (str, sgn) = E.chaseMpath env (m1, ms)
1798 in
1799 case E.projectDatatype env {str = str, sgn = sgn, field = s} of
1800 NONE => NONE
1801 | SOME xncs1 => found (n1, xncs1)
1802 end
1803 | _ => NONE
1804 end)
1792 1805
1793 | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) => 1806 | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) =>
1794 seek (fn sgi1All as (sgi1, _) => 1807 seek (fn sgi1All as (sgi1, _) =>
1795 case sgi1 of 1808 case sgi1 of
1796 L'.SgiDatatypeImp (x', n1, m12, ms2, s2) => 1809 L'.SgiDatatypeImp (x', n1, m12, ms2, s2) =>