Mercurial > urweb

comparison src/elaborate.sml @ 218:a3413288cce1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Signature ascription for type classes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 16:57:21 -0400
parents 56db662ebcfd
children 2b665e822e9a
comparison
equal deleted inserted replaced
217:56db662ebcfd 218:a3413288cce1
1911 | L.SgiVal (x, c) => 1911 | L.SgiVal (x, c) =>
1912 let 1912 let
1913 val (c', ck, gs') = elabCon (env, denv) c 1913 val (c', ck, gs') = elabCon (env, denv) c
1914 1914
1915 val (env', n) = E.pushENamed env x c' 1915 val (env', n) = E.pushENamed env x c'
1916 val (c', gs'') = normClassConstraint (env, denv) c'
1916 in 1917 in
1917 (unifyKinds ck ktype 1918 (unifyKinds ck ktype
1918 handle KUnify ue => strError env (NotType (ck, ue))); 1919 handle KUnify ue => strError env (NotType (ck, ue)));
1919 1920
1920 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 1921 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs))
1921 end 1922 end
1922 1923
1923 | L.SgiStr (x, sgn) => 1924 | L.SgiStr (x, sgn) =>
1924 let 1925 let
1925 val (sgn', gs') = elabSgn (env, denv) sgn 1926 val (sgn', gs') = elabSgn (env, denv) sgn
2135 | L'.SgnConst sgis => 2136 | L'.SgnConst sgis =>
2136 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 2137 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
2137 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 2138 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
2138 | (L'.SgiDatatype (x, n, xs, xncs), loc) => 2139 | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
2139 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) 2140 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
2141 | (L'.SgiClassAbs (x, n), loc) =>
2142 (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc)
2140 | (L'.SgiStr (x, n, sgn), loc) => 2143 | (L'.SgiStr (x, n, sgn), loc) =>
2141 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 2144 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
2142 | x => x) sgis), #2 sgn) 2145 | x => x) sgis), #2 sgn)
2143 | L'.SgnFun _ => sgn 2146 | L'.SgnFun _ => sgn
2144 | L'.SgnWhere _ => sgn 2147 | L'.SgnWhere _ => sgn
2337 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2340 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2338 in 2341 in
2339 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) 2342 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
2340 end 2343 end
2341 | L'.SgiClassAbs (x', n1) => found (x', n1, 2344 | L'.SgiClassAbs (x', n1) => found (x', n1,
2342 (L'.KArrow ((L'.KType, loc), 2345 (L'.KArrow ((L'.KType, loc),
2343 (L'.KType, loc)), loc), 2346 (L'.KType, loc)), loc),
2344 NONE) 2347 NONE)
2345 | L'.SgiClass (x', n1, c) => found (x', n1, 2348 | L'.SgiClass (x', n1, c) => found (x', n1,
2346 (L'.KArrow ((L'.KType, loc), 2349 (L'.KArrow ((L'.KType, loc),
2347 (L'.KType, loc)), loc), 2350 (L'.KType, loc)), loc),
2348 SOME c) 2351 SOME c)
2349 | _ => NONE 2352 | _ => NONE
2590 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2593 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2591 2594
2592 fun found (x', n1, c1) = 2595 fun found (x', n1, c1) =
2593 if x = x' then 2596 if x = x' then
2594 let 2597 let
2595 fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv) 2598 fun good () =
2599 let
2600 val env = E.pushCNamedAs env x n2 k (SOME c2)
2601 val env = if n1 = n2 then
2602 env
2603 else
2604 E.pushCNamedAs env x n1 k (SOME c1)
2605 in
2606 SOME (env, denv)
2607 end
2596 in 2608 in
2597 (case unifyCons (env, denv) c1 c2 of 2609 (case unifyCons (env, denv) c1 c2 of
2598 [] => good () 2610 [] => good ()
2599 | _ => NONE) 2611 | _ => NONE)
2600 handle CUnify (c1, c2, err) => 2612 handle CUnify (c1, c2, err) =>
2821 2833
2822 val needed = foldl (fn ((d, _), needed) => 2834 val needed = foldl (fn ((d, _), needed) =>
2823 case d of 2835 case d of
2824 L.DCon (x, _, _) => (SS.delete (needed, x) 2836 L.DCon (x, _, _) => (SS.delete (needed, x)
2825 handle NotFound => needed) 2837 handle NotFound => needed)
2838 | L.DClass (x, _) => (SS.delete (needed, x)
2839 handle NotFound => needed)
2826 | L.DOpen _ => SS.empty 2840 | L.DOpen _ => SS.empty
2827 | _ => needed) 2841 | _ => needed)
2828 needed ds 2842 needed ds
2829 in 2843 in
2830 case SS.listItems needed of 2844 case SS.listItems needed of