Mercurial > urweb

comparison src/elaborate.sml @ 1030:6bcc1020d5cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Decision
author Adam Chlipala <adamc@hcoop.net>
date Mon, 02 Nov 2009 15:48:06 -0500
parents 4de35df3d545
children 38411c2cd363
comparison
equal deleted inserted replaced
1029:53a22f46f377 1030:6bcc1020d5cd
1994 case E.projectStr env {str = str, sgn = sgn, field = m} of 1994 case E.projectStr env {str = str, sgn = sgn, field = m} of
1995 NONE => (strError env (UnboundStr (loc, m)); 1995 NONE => (strError env (UnboundStr (loc, m));
1996 (strerror, sgnerror)) 1996 (strerror, sgnerror))
1997 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1997 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1998 ((L'.StrVar n, loc), sgn) strs 1998 ((L'.StrVar n, loc), sgn) strs
1999 1999
2000 val cso = E.projectConstraints env {sgn = sgn, str = st} 2000 fun collect first (st, sgn) =
2001 case E.projectConstraints env {sgn = sgn, str = st} of
2002 NONE => (if first then
2003 strError env (UnboundStr (loc, str))
2004 else
2005 ();
2006 [])
2007 | SOME cs =>
2008 case #1 (hnormSgn env sgn) of
2009 L'.SgnConst sgis =>
2010 foldl (fn (sgi, cs) =>
2011 case #1 sgi of
2012 L'.SgiStr (x, _, _) =>
2013 (case E.projectStr env {sgn = sgn, str = st, field = x} of
2014 NONE => raise Fail "Elaborate: projectStr in collect"
2015 | SOME sgn' =>
2016 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'),
2017 cs))
2018 | _ => cs) cs sgis
2019 | _ => cs
2001 in 2020 in
2002 case cso of 2021 foldl (fn ((c1, c2), denv) =>
2003 NONE => (strError env (UnboundStr (loc, str)); 2022 D.assert env denv (c1, c2)) denv (collect true (st, sgn))
2004 denv)
2005 | SOME cs => foldl (fn ((c1, c2), denv) =>
2006 D.assert env denv (c1, c2)) denv cs
2007 end 2023 end
2008 2024
2009 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 2025 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
2010 case sgi of 2026 case sgi of
2011 L.SgiConAbs (x, k) => 2027 L.SgiConAbs (x, k) =>
3443 (case E.lookupStr env m of 3459 (case E.lookupStr env m of
3444 NONE => (strError env (UnboundStr (loc, m)); 3460 NONE => (strError env (UnboundStr (loc, m));
3445 ([], (env, denv, gs))) 3461 ([], (env, denv, gs)))
3446 | SOME (n, sgn) => 3462 | SOME (n, sgn) =>
3447 let 3463 let
3448 val (_, sgn) = foldl (fn (m, (str, sgn)) => 3464 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
3449 case E.projectStr env {str = str, sgn = sgn, field = m} of 3465 case E.projectStr env {str = str, sgn = sgn, field = m} of
3450 NONE => (strError env (UnboundStr (loc, m)); 3466 NONE => (strError env (UnboundStr (loc, m));
3451 (strerror, sgnerror)) 3467 (strerror, sgnerror))
3452 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 3468 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
3453 ((L'.StrVar n, loc), sgn) ms 3469 ((L'.StrVar n, loc), sgn) ms
3470
3471 val sgn = selfifyAt env {str = str, sgn = sgn}
3454 3472
3455 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} 3473 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
3456 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms} 3474 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms}
3457 in 3475 in
3458 (ds, (env', denv', gs)) 3476 (ds, (env', denv', gs))