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 _ =>