Mercurial > urweb

comparison src/elaborate.sml @ 100:f0f59e918cac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
page declaration, up through monoize
author Adam Chlipala <adamc@hcoop.net>
date Thu, 10 Jul 2008 10:11:35 -0400
parents 94afff1ff7f6
children 813e5a52063d
comparison
equal deleted inserted replaced
99:5182f0c80d2e 100:f0f59e918cac
1591 denv 1591 denv
1592 end 1592 end
1593 1593
1594 fun sgiOfDecl (d, loc) = 1594 fun sgiOfDecl (d, loc) =
1595 case d of 1595 case d of
1596 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc) 1596 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
1597 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc) 1597 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
1598 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc) 1598 | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc)
1599 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc) 1599 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
1600 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) 1600 | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc)
1601 | L'.DConstraint cs => (L'.SgiConstraint cs, loc) 1601 | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc)
1602 | L'.DPage _ => NONE
1602 1603
1603 fun sgiBindsD (env, denv) (sgi, _) = 1604 fun sgiBindsD (env, denv) (sgi, _) =
1604 case sgi of 1605 case sgi of
1605 L'.SgiConstraint (c1, c2) => 1606 L'.SgiConstraint (c1, c2) =>
1606 (case D.assert env denv (c1, c2) of 1607 (case D.assert env denv (c1, c2) of
1926 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} 1927 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
1927 in 1928 in
1928 ([], (env, denv, [])) 1929 ([], (env, denv, []))
1929 end 1930 end
1930 1931
1932 | L.DPage e =>
1933 let
1934 val basis =
1935 case E.lookupStr env "Basis" of
1936 NONE => raise Fail "elabExp: Unbound Basis"
1937 | SOME (n, _) => n
1938
1939 val (e', t, gs1) = elabExp (env, denv) e
1940
1941 val k = (L'.KRecord (L'.KType, loc), loc)
1942 val vs = cunif (loc, k)
1943
1944 val c = (L'.TFun ((L'.TRecord vs, loc),
1945 (L'.CApp ((L'.CModProj (basis, [], "xml"), loc),
1946 (L'.CRecord ((L'.KUnit, loc),
1947 [((L'.CName "Html", loc),
1948 (L'.CUnit, loc))]), loc)), loc)), loc)
1949
1950 val gs2 = checkCon (env, denv) e' t c
1951 in
1952 ([(L'.DPage (vs, e'), loc)], (env, denv, gs1 @ gs2))
1953 end
1954
1931 and elabStr (env, denv) (str, loc) = 1955 and elabStr (env, denv) (str, loc) =
1932 case str of 1956 case str of
1933 L.StrConst ds => 1957 L.StrConst ds =>
1934 let 1958 let
1935 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds 1959 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
1936 val sgis = map sgiOfDecl ds' 1960 val sgis = List.mapPartial sgiOfDecl ds'
1937 1961
1938 val (sgis, _, _, _, _) = 1962 val (sgis, _, _, _, _) =
1939 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => 1963 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
1940 case sgi of 1964 case sgi of
1941 L'.SgiConAbs (x, n, k) => 1965 L'.SgiConAbs (x, n, k) =>