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