Mercurial > urweb

comparison src/elaborate.sml @ 720:acb8537f58f0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Stop tracking CSS classes in XML types
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 12:31:54 -0400
parents 5c099b1308ae
children 9864b64b1700
comparison
equal deleted inserted replaced
719:5c099b1308ae 720:acb8537f58f0
2400 (L'.CConcat (pc, cc), loc)), loc)), loc)] 2400 (L'.CConcat (pc, cc), loc)), loc)), loc)]
2401 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2401 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2402 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2402 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2403 | L'.DDatabase _ => [] 2403 | L'.DDatabase _ => []
2404 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2404 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2405 | L'.DStyle (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (styleOf (), c), loc)), loc)] 2405 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
2406 2406
2407 and subSgn env sgn1 (sgn2 as (_, loc2)) = 2407 and subSgn env sgn1 (sgn2 as (_, loc2)) =
2408 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), 2408 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2409 ("sgn2", p_sgn env sgn2)];*) 2409 ("sgn2", p_sgn env sgn2)];*)
2410 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 2410 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
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, arg4), _)) => 3287 (L'.CApp (tf, arg3), _)) =>
3288 (case (basis = !basis_r, 3288 (case (basis = !basis_r,
3289 hnormCon env tf, hnormCon env arg4) of 3289 hnormCon env tf, hnormCon env arg3) of
3290 (true, 3290 (true,
3291 (L'.CApp (tf, arg3), _), 3291 (L'.CApp (tf, arg2), _),
3292 ((L'.CRecord (_, []), _))) => 3292 ((L'.CRecord (_, []), _))) =>
3293 (case hnormCon env tf of 3293 (case (hnormCon env tf) of
3294 (L'.CApp (tf, arg2), _) => 3294 (L'.CApp (tf, arg1), _) =>
3295 (case hnormCon env tf of 3295 (case (hnormCon env tf,
3296 (L'.CApp (tf, arg1), _) => 3296 hnormCon env arg1,
3297 (case (hnormCon env tf, 3297 hnormCon env arg2) of
3298 hnormCon env arg1, 3298 (tf, arg1,
3299 hnormCon env arg2, 3299 (L'.CRecord (_, []), _)) =>
3300 hnormCon env arg3, 3300 let
3301 hnormCon env arg4) of 3301 val t = (L'.CApp (tf, arg1), loc)
3302 (tf, 3302 val t = (L'.CApp (t, arg2), loc)
3303 arg1, 3303 val t = (L'.CApp (t, arg3), loc)
3304 (L'.CRecord (_, []), _), 3304 val t = (L'.CApp (
3305 arg2, 3305 (L'.CModProj
3306 arg4) => 3306 (basis, [], "transaction"), loc),
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),
3316 t), loc) 3307 t), loc)
3317 in 3308 in
3318 (L'.SgiVal (x, n, makeRes t), loc) 3309 (L'.SgiVal (x, n, makeRes t), loc)
3319 end 3310 end
3320 | _ => all)
3321 | _ => all) 3311 | _ => all)
3322 | _ => all) 3312 | _ => all)
3323 | _ => all) 3313 | _ => all)
3324 | _ => all) 3314 | _ => all)
3325 | _ => all 3315 | _ => all
3400 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) 3390 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc)
3401 in 3391 in
3402 checkKind env c' k (L'.KType, loc); 3392 checkKind env c' k (L'.KType, loc);
3403 ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3393 ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
3404 end 3394 end
3405 | L.DStyle (x, c) => 3395 | L.DStyle x =>
3406 let 3396 let
3407 val (c', k, gs') = elabCon (env, denv) c 3397 val (env, n) = E.pushENamed env x (styleOf ())
3408 val (env, n) = E.pushENamed env x (L'.CApp (styleOf (), c'), loc)
3409 in 3398 in
3410 checkKind env c' k (L'.KRecord (L'.KUnit, loc), loc); 3399 ([(L'.DStyle (!basis_r, x, n), loc)], (env, denv, gs))
3411 ([(L'.DStyle (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
3412 end 3400 end
3413 3401
3414 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) 3402 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
3415 in 3403 in
3416 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), 3404 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
3630 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) 3618 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
3631 val () = case gs of 3619 val () = case gs of
3632 [] => () 3620 [] => ()
3633 | _ => raise Fail "Unresolved disjointness constraints in top.urs" 3621 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
3634 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) 3622 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
3645 val () = case gs of 3623 val () = case gs of
3646 [] => () 3624 [] => ()
3647 | _ => app (fn Disjoint (loc, env, denv, c1, c2) => 3625 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
3648 (case D.prove env denv (c1, c2, loc) of 3626 (case D.prove env denv (c1, c2, loc) of
3649 [] => () 3627 [] => ()
3650 | _ => 3628 | _ =>
3651 (prefaces "Unresolved constraint in top.ur" 3629 (prefaces "Unresolved constraint in top.ur"
3652 [("loc", PD.string (ErrorMsg.spanToString loc)), 3630 [("loc", PD.string (ErrorMsg.spanToString loc)),
3653 ("c1", p_con env c1), 3631 ("c1", p_con env c1),
3654 ("c2", p_con env c2), 3632 ("c2", p_con env c2)];
3655 ("topStr", p_str env topStr)];
3656 raise Fail "Unresolved constraint in top.ur")) 3633 raise Fail "Unresolved constraint in top.ur"))
3657 | TypeClass (env, c, r, loc) => 3634 | TypeClass (env, c, r, loc) =>
3658 let 3635 let
3659 val c = normClassKey env c 3636 val c = normClassKey env c
3660 in 3637 in
3661 case E.resolveClass env c of 3638 case E.resolveClass env c of
3662 SOME e => r := SOME e 3639 SOME e => r := SOME e
3663 | NONE => expError env (Unresolvable (loc, c)) 3640 | NONE => expError env (Unresolvable (loc, c))
3664 end) gs 3641 end) gs
3642
3643 val () = subSgn env' topSgn' topSgn
3665 3644
3666 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3645 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3667 val () = top_r := top_n 3646 val () = top_r := top_n
3668 3647
3669 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 3648 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}