Mercurial > urweb

comparison src/elaborate.sml @ 719:5c099b1308ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hello compiles with CSS
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 11:08:00 -0400
parents f152f215a02c
children acb8537f58f0
comparison
equal deleted inserted replaced
718:f152f215a02c 719:5c099b1308ae
3282 fun doPage (makeRes, ran) = 3282 fun doPage (makeRes, ran) =
3283 case hnormCon env ran of 3283 case hnormCon env ran of
3284 (L'.CApp (tf, arg), _) => 3284 (L'.CApp (tf, arg), _) =>
3285 (case (hnormCon env tf, hnormCon env arg) of 3285 (case (hnormCon env tf, hnormCon env arg) of
3286 ((L'.CModProj (basis, [], "transaction"), _), 3286 ((L'.CModProj (basis, [], "transaction"), _),
3287 (L'.CApp (tf, arg3), _)) => 3287 (L'.CApp (tf, arg4), _)) =>
3288 (case (basis = !basis_r, 3288 (case (basis = !basis_r,
3289 hnormCon env tf, hnormCon env arg3) of 3289 hnormCon env tf, hnormCon env arg4) of
3290 (true, 3290 (true,
3291 (L'.CApp (tf, arg2), _), 3291 (L'.CApp (tf, arg3), _),
3292 ((L'.CRecord (_, []), _))) => 3292 ((L'.CRecord (_, []), _))) =>
3293 (case (hnormCon env tf) of 3293 (case hnormCon env tf of
3294 (L'.CApp (tf, arg1), _) => 3294 (L'.CApp (tf, arg2), _) =>
3295 (case (hnormCon env tf, 3295 (case hnormCon env tf of
3296 hnormCon env arg1, 3296 (L'.CApp (tf, arg1), _) =>
3297 hnormCon env arg2) of 3297 (case (hnormCon env tf,
3298 (tf, arg1, 3298 hnormCon env arg1,
3299 (L'.CRecord (_, []), _)) => 3299 hnormCon env arg2,
3300 let 3300 hnormCon env arg3,
3301 val t = (L'.CApp (tf, arg1), loc) 3301 hnormCon env arg4) of
3302 val t = (L'.CApp (t, arg2), loc) 3302 (tf,
3303 val t = (L'.CApp (t, arg3), loc) 3303 arg1,
3304 val t = (L'.CApp ( 3304 (L'.CRecord (_, []), _),
3305 (L'.CModProj 3305 arg2,
3306 (basis, [], "transaction"), loc), 3306 arg4) =>
3307 let
3308 val t = (L'.CApp (tf, arg1), loc)
3309 val t = (L'.CApp (t, arg2), loc)
3310 val t = (L'.CApp (t, arg3), loc)
3311 val t = (L'.CApp (t, arg4), loc)
3312
3313 val t = (L'.CApp (
3314 (L'.CModProj
3315 (basis, [], "transaction"), loc),
3307 t), loc) 3316 t), loc)
3308 in 3317 in
3309 (L'.SgiVal (x, n, makeRes t), loc) 3318 (L'.SgiVal (x, n, makeRes t), loc)
3310 end 3319 end
3320 | _ => all)
3311 | _ => all) 3321 | _ => all)
3312 | _ => all) 3322 | _ => all)
3313 | _ => all) 3323 | _ => all)
3314 | _ => all) 3324 | _ => all)
3315 | _ => all 3325 | _ => all
3620 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) 3630 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
3621 val () = case gs of 3631 val () = case gs of
3622 [] => () 3632 [] => ()
3623 | _ => raise Fail "Unresolved disjointness constraints in top.urs" 3633 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
3624 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) 3634 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
3635
3636 val () = subSgn env' topSgn' topSgn
3637
3638 val () = app (fn (env, k, s1, s2) =>
3639 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
3640 handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in Top final record unification";
3641 cunifyError env err))
3642 (!delayedUnifs)
3643 val () = delayedUnifs := []
3644
3625 val () = case gs of 3645 val () = case gs of
3626 [] => () 3646 [] => ()
3627 | _ => app (fn Disjoint (loc, env, denv, c1, c2) => 3647 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
3628 (case D.prove env denv (c1, c2, loc) of 3648 (case D.prove env denv (c1, c2, loc) of
3629 [] => () 3649 [] => ()
3630 | _ => 3650 | _ =>
3631 (prefaces "Unresolved constraint in top.ur" 3651 (prefaces "Unresolved constraint in top.ur"
3632 [("loc", PD.string (ErrorMsg.spanToString loc)), 3652 [("loc", PD.string (ErrorMsg.spanToString loc)),
3633 ("c1", p_con env c1), 3653 ("c1", p_con env c1),
3634 ("c2", p_con env c2)]; 3654 ("c2", p_con env c2),
3655 ("topStr", p_str env topStr)];
3635 raise Fail "Unresolved constraint in top.ur")) 3656 raise Fail "Unresolved constraint in top.ur"))
3636 | TypeClass (env, c, r, loc) => 3657 | TypeClass (env, c, r, loc) =>
3637 let 3658 let
3638 val c = normClassKey env c 3659 val c = normClassKey env c
3639 in 3660 in
3640 case E.resolveClass env c of 3661 case E.resolveClass env c of
3641 SOME e => r := SOME e 3662 SOME e => r := SOME e
3642 | NONE => expError env (Unresolvable (loc, c)) 3663 | NONE => expError env (Unresolvable (loc, c))
3643 end) gs 3664 end) gs
3644
3645 val () = subSgn env' topSgn' topSgn
3646 3665
3647 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3666 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3648 val () = top_r := top_n 3667 val () = top_r := top_n
3649 3668
3650 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 3669 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}