Mercurial > urweb

comparison src/elaborate.sml @ 1864:1aa9629e3a4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
author Adam Chlipala <adam@chlipala.net>
date Mon, 19 Aug 2013 12:25:32 -0400
parents bb942416bf1c
children 5144e03ef603
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
1 (* Copyright (c) 2008-2012, Adam Chlipala 1 (* Copyright (c) 2008-2013, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
2638 2638
2639 | L.SgiStr (x, sgn) => 2639 | L.SgiStr (x, sgn) =>
2640 let 2640 let
2641 val (sgn', gs') = elabSgn (env, denv) sgn 2641 val (sgn', gs') = elabSgn (env, denv) sgn
2642 val (env', n) = E.pushStrNamed env x sgn' 2642 val (env', n) = E.pushStrNamed env x sgn'
2643 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
2643 in 2644 in
2644 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) 2645 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs))
2645 end 2646 end
2646 2647
2647 | L.SgiSgn (x, sgn) => 2648 | L.SgiSgn (x, sgn) =>
2648 let 2649 let
2649 val (sgn', gs') = elabSgn (env, denv) sgn 2650 val (sgn', gs') = elabSgn (env, denv) sgn
2796 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []} 2797 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
2797 val (ran', gs2) = elabSgn (env', denv') ran 2798 val (ran', gs2) = elabSgn (env', denv') ran
2798 in 2799 in
2799 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2) 2800 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
2800 end 2801 end
2801 | L.SgnWhere (sgn, x, c) => 2802 | L.SgnWhere (sgn, ms, x, c) =>
2802 let 2803 let
2803 val (sgn', ds1) = elabSgn (env, denv) sgn 2804 val (sgn', ds1) = elabSgn (env, denv) sgn
2804 val (c', ck, ds2) = elabCon (env, denv) c 2805 val (c', ck, ds2) = elabCon (env, denv) c
2805 in 2806
2806 case #1 (hnormSgn env sgn') of 2807 fun checkPath (ms, sgn') =
2807 L'.SgnError => (sgnerror, []) 2808 case #1 (hnormSgn env sgn') of
2808 | L'.SgnConst sgis => 2809 L'.SgnConst sgis =>
2809 if List.exists (fn (L'.SgiConAbs (x', _, k), _) => 2810 List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
2810 x' = x andalso 2811 List.null ms andalso x' = x andalso
2811 (unifyKinds env k ck 2812 (unifyKinds env k ck
2812 handle KUnify x => sgnError env (WhereWrongKind x); 2813 handle KUnify x => sgnError env (WhereWrongKind x);
2813 true) 2814 true)
2814 | _ => false) sgis then 2815 | (L'.SgiStr (x', _, sgn''), _) =>
2815 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2) 2816 (case ms of
2816 else 2817 [] => false
2817 (sgnError env (UnWhereable (sgn', x)); 2818 | m :: ms' =>
2818 (sgnerror, [])) 2819 m = x' andalso
2819 | _ => (sgnError env (UnWhereable (sgn', x)); 2820 checkPath (ms', sgn''))
2820 (sgnerror, [])) 2821 | _ => false) sgis
2822 | _ => false
2823 in
2824 if checkPath (ms, sgn') then
2825 ((L'.SgnWhere (sgn', ms, x, c'), loc), ds1 @ ds2)
2826 else
2827 (sgnError env (UnWhereable (sgn', x));
2828 (sgnerror, []))
2821 end 2829 end
2822 | L.SgnProj (m, ms, x) => 2830 | L.SgnProj (m, ms, x) =>
2823 (case E.lookupStr env m of 2831 (case E.lookupStr env m of
2824 NONE => (strError env (UnboundStr (loc, m)); 2832 NONE => (strError env (UnboundStr (loc, m));
2825 (sgnerror, [])) 2833 (sgnerror, []))
3592 | L'.CApp (f, x) => 3600 | L'.CApp (f, x) =>
3593 (case (decompileCon env f, decompileCon env x) of 3601 (case (decompileCon env f, decompileCon env x) of
3594 (SOME f, SOME x) => SOME (L.CApp (f, x), loc) 3602 (SOME f, SOME x) => SOME (L.CApp (f, x), loc)
3595 | _ => NONE) 3603 | _ => NONE)
3596 3604
3605 | L'.CTuple cs =>
3606 let
3607 val cs' = foldr (fn (c, cs') =>
3608 case cs' of
3609 NONE => NONE
3610 | SOME cs' =>
3611 case decompileCon env c of
3612 NONE => NONE
3613 | SOME c' => SOME (c' :: cs'))
3614 (SOME []) cs
3615 in
3616 case cs' of
3617 NONE => NONE
3618 | SOME cs' => SOME (L.CTuple cs', loc)
3619 end
3620
3621 | L'.CMap _ => SOME (L.CMap, loc)
3622
3597 | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE) 3623 | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE)
3598 3624
3599 fun buildNeeded env sgis = 3625 fun buildNeeded env sgis =
3600 #1 (foldl (fn ((sgi, loc), (nd, env')) => 3626 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
3601 (case sgi of 3627 (case sgi of