Mercurial > urweb

comparison src/elaborate.sml @ 834:74e9e7642f08

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Do 'open constraints' automatically; fix sourceless <cselect> monoize bug; Monad library module
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Jun 2009 11:50:53 -0400
parents 9a1026e2b3f5
children ccf22c2c77b2
comparison
equal deleted inserted replaced
833:9a1026e2b3f5 834:74e9e7642f08
3353 subSgn env (selfifyAt env {str = str', sgn = actual}) formal; 3353 subSgn env (selfifyAt env {str = str', sgn = actual}) formal;
3354 (str', formal, enD gs1 @ gs2) 3354 (str', formal, enD gs1 @ gs2)
3355 end 3355 end
3356 3356
3357 val (env', n) = E.pushStrNamed env x sgn' 3357 val (env', n) = E.pushStrNamed env x sgn'
3358 val denv' =
3359 case #1 str' of
3360 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
3361 | _ => denv
3358 in 3362 in
3359 case #1 (hnormSgn env sgn') of 3363 case #1 (hnormSgn env sgn') of
3360 L'.SgnFun _ => 3364 L'.SgnFun _ =>
3361 (case #1 str' of 3365 (case #1 str' of
3362 L'.StrFun _ => () 3366 L'.StrFun _ => ()
3363 | _ => strError env (FunctorRebind loc)) 3367 | _ => strError env (FunctorRebind loc))
3364 | _ => (); 3368 | _ => ();
3365 3369
3366 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) 3370 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs))
3367 end 3371 end
3368 3372
3369 | L.DFfiStr (x, sgn) => 3373 | L.DFfiStr (x, sgn) =>
3370 let 3374 let
3371 val (sgn', gs') = elabSgn (env, denv) sgn 3375 val (sgn', gs') = elabSgn (env, denv) sgn
3719 end 3723 end
3720 | L.StrFun (m, dom, ranO, str) => 3724 | L.StrFun (m, dom, ranO, str) =>
3721 let 3725 let
3722 val (dom', gs1) = elabSgn (env, denv) dom 3726 val (dom', gs1) = elabSgn (env, denv) dom
3723 val (env', n) = E.pushStrNamed env m dom' 3727 val (env', n) = E.pushStrNamed env m dom'
3724 val (str', actual, gs2) = elabStr (env', denv) str 3728 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
3729 val (str', actual, gs2) = elabStr (env', denv') str
3725 3730
3726 val (formal, gs3) = 3731 val (formal, gs3) =
3727 case ranO of 3732 case ranO of
3728 NONE => (actual, []) 3733 NONE => (actual, [])
3729 | SOME ran => 3734 | SOME ran =>
3730 let 3735 let
3731 val (ran', gs) = elabSgn (env', denv) ran 3736 val (ran', gs) = elabSgn (env', denv') ran
3732 in 3737 in
3733 subSgn env' actual ran'; 3738 subSgn env' actual ran';
3734 (ran', gs) 3739 (ran', gs)
3735 end 3740 end
3736 in 3741 in