Mercurial > urweb
comparison src/elaborate.sml @ 1883:5125b1df6045
Save disjointness environments across top-level declarations
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 17 Oct 2013 09:22:38 -0400 |
parents | d6b0ee53dc93 |
children | b7cd3c7c7edd |
comparison
equal
deleted
inserted
replaced
1882:77cde56d41b6 | 1883:5125b1df6045 |
---|---|
4000 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; | 4000 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; |
4001 (str', formal, enD gs1 @ gs2) | 4001 (str', formal, enD gs1 @ gs2) |
4002 end | 4002 end |
4003 | 4003 |
4004 val (env', n) = E.pushStrNamed env x sgn' | 4004 val (env', n) = E.pushStrNamed env x sgn' |
4005 | |
4005 val denv' = | 4006 val denv' = |
4006 case #1 str' of | 4007 case #1 str' of |
4007 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} | 4008 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} |
4008 | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} | 4009 | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} |
4009 | _ => denv | 4010 | _ => denv |
4579 | 4580 |
4580 val () = top_r := top_n | 4581 val () = top_r := top_n |
4581 | 4582 |
4582 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} | 4583 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} |
4583 | 4584 |
4584 fun elabDecl' (d, (env, gs)) = | 4585 fun elabDecl' x = |
4585 let | 4586 (resetKunif (); |
4586 val () = resetKunif () | 4587 resetCunif (); |
4587 val () = resetCunif () | 4588 elabDecl x) |
4588 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs)) | 4589 |
4589 in | 4590 val (file, (env'', _, gs)) = ListUtil.foldlMapConcat elabDecl' (env', D.empty, []) file |
4590 (ds, (env', gs)) | |
4591 end | |
4592 | |
4593 val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file | |
4594 | 4591 |
4595 fun oneSummaryRound () = | 4592 fun oneSummaryRound () = |
4596 if ErrorMsg.anyErrors () then | 4593 if ErrorMsg.anyErrors () then |
4597 () | 4594 () |
4598 else | 4595 else |