Mercurial > urweb
comparison src/elaborate.sml @ 78:a6d45c6819c9
Implicit structure members
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 29 Jun 2008 11:05:38 -0400 |
parents | 522f4bd3955e |
children | 37847b504cc6 |
comparison
equal
deleted
inserted
replaced
77:a1026ae076ea | 78:a6d45c6819c9 |
---|---|
1567 end | 1567 end |
1568 | 1568 |
1569 | L.DStr (x, sgno, str) => | 1569 | L.DStr (x, sgno, str) => |
1570 let | 1570 let |
1571 val formal = Option.map (elabSgn env) sgno | 1571 val formal = Option.map (elabSgn env) sgno |
1572 val (str', actual) = elabStr env str | 1572 |
1573 | 1573 val (str', sgn') = |
1574 val sgn' = case formal of | 1574 case formal of |
1575 NONE => selfifyAt env {str = str', sgn = actual} | 1575 NONE => |
1576 | SOME formal => | 1576 let |
1577 (subSgn env actual formal; | 1577 val (str', actual) = elabStr env str |
1578 formal) | 1578 in |
1579 (str', selfifyAt env {str = str', sgn = actual}) | |
1580 end | |
1581 | SOME formal => | |
1582 let | |
1583 val str = | |
1584 case #1 (hnormSgn env formal) of | |
1585 L'.SgnConst sgis => | |
1586 (case #1 str of | |
1587 L.StrConst ds => | |
1588 let | |
1589 val needed = foldl (fn ((sgi, _), needed) => | |
1590 case sgi of | |
1591 L'.SgiConAbs (x, _, _) => SS.add (needed, x) | |
1592 | _ => needed) | |
1593 SS.empty sgis | |
1594 | |
1595 val needed = foldl (fn ((d, _), needed) => | |
1596 case d of | |
1597 L.DCon (x, _, _) => (SS.delete (needed, x) | |
1598 handle NotFound => needed) | |
1599 | L.DOpen _ => SS.empty | |
1600 | _ => needed) | |
1601 needed ds | |
1602 in | |
1603 case SS.listItems needed of | |
1604 [] => str | |
1605 | xs => | |
1606 let | |
1607 val kwild = (L.KWild, #2 str) | |
1608 val cwild = (L.CWild kwild, #2 str) | |
1609 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs | |
1610 in | |
1611 (L.StrConst (ds @ ds'), #2 str) | |
1612 end | |
1613 end | |
1614 | _ => str) | |
1615 | _ => str | |
1616 | |
1617 val (str', actual) = elabStr env str | |
1618 in | |
1619 subSgn env actual formal; | |
1620 (str', formal) | |
1621 end | |
1579 | 1622 |
1580 val (env', n) = E.pushStrNamed env x sgn' | 1623 val (env', n) = E.pushStrNamed env x sgn' |
1581 in | 1624 in |
1582 case #1 (hnormSgn env sgn') of | 1625 case #1 (hnormSgn env sgn') of |
1583 L'.SgnFun _ => | 1626 L'.SgnFun _ => |