Mercurial > urweb

comparison src/elaborate.sml @ 1797:bb942416bf1c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove 'class' declaration; now use 'con' instead
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Jul 2012 12:27:13 -0400
parents 1bbad32cb4a8
children 1aa9629e3a4c
comparison
equal deleted inserted replaced
1796:0de0daab5fbb 1797:bb942416bf1c
2980 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), 2980 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
2981 (L'.CConcat (pc, cc), loc)), loc)), loc)] 2981 (L'.CConcat (pc, cc), loc)), loc)), loc)]
2982 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2982 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2983 | L'.DView (tn, x, n, _, c) => 2983 | L'.DView (tn, x, n, _, c) =>
2984 [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)] 2984 [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)]
2985 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2986 | L'.DDatabase _ => [] 2985 | L'.DDatabase _ => []
2987 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2986 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2988 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] 2987 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
2989 | L'.DTask _ => [] 2988 | L'.DTask _ => []
2990 | L'.DPolicy _ => [] 2989 | L'.DPolicy _ => []
3360 NONE 3359 NONE
3361 in 3360 in
3362 case sgi1 of 3361 case sgi1 of
3363 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE) 3362 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
3364 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c) 3363 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
3364 | L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
3365 | L'.SgiCon (x', n1, k1, c) => found (x', n1, k1, SOME c)
3365 | _ => NONE 3366 | _ => NONE
3366 end) 3367 end)
3367 | L'.SgiClass (x, n2, k2, c2) => 3368 | L'.SgiClass (x, n2, k2, c2) =>
3368 seek (fn (env, sgi1All as (sgi1, loc)) => 3369 seek (fn (env, sgi1All as (sgi1, loc)) =>
3369 let 3370 let
3399 else 3400 else
3400 NONE 3401 NONE
3401 in 3402 in
3402 case sgi1 of 3403 case sgi1 of
3403 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) 3404 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
3405 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
3404 | _ => NONE 3406 | _ => NONE
3405 end) 3407 end)
3406 end 3408 end
3407 in 3409 in
3408 ignore (foldl folder env sgis2) 3410 ignore (foldl folder env sgis2)
3506 | _ => NONE 3508 | _ => NONE
3507 3509
3508 fun dname (d, _) = 3510 fun dname (d, _) =
3509 case d of 3511 case d of
3510 L.DCon (x, _, _) => SOME x 3512 L.DCon (x, _, _) => SOME x
3511 | L.DClass (x, _, _) => SOME x
3512 | _ => NONE 3513 | _ => NONE
3513 3514
3514 fun decompileKind (k, loc) = 3515 fun decompileKind (k, loc) =
3515 case k of 3516 case k of
3516 L'.KType => SOME (L.KType, loc) 3517 L'.KType => SOME (L.KType, loc)
3639 3640
3640 fun removeUsed (nd, ds) = 3641 fun removeUsed (nd, ds) =
3641 foldl (fn ((d, _), nd) => 3642 foldl (fn ((d, _), nd) =>
3642 case d of 3643 case d of
3643 L.DCon (x, _, _) => ndelCon (nd, x) 3644 L.DCon (x, _, _) => ndelCon (nd, x)
3644 | L.DClass (x, _, _) => ndelCon (nd, x)
3645 | L.DVal (x, _, _) => ndelVal (nd, x) 3645 | L.DVal (x, _, _) => ndelVal (nd, x)
3646 | L.DOpen _ => nempty 3646 | L.DOpen _ => nempty
3647 | L.DStr (x, _, _, (L.StrConst ds', _)) => 3647 | L.DStr (x, _, _, (L.StrConst ds', _)) =>
3648 (case SM.find (nmods nd, x) of 3648 (case SM.find (nmods nd, x) of
3649 NONE => nd 3649 NONE => nd
3664 L.DCon _ => true 3664 L.DCon _ => true
3665 | L.DDatatype _ => true 3665 | L.DDatatype _ => true
3666 | L.DDatatypeImp _ => true 3666 | L.DDatatypeImp _ => true
3667 | L.DStr _ => true 3667 | L.DStr _ => true
3668 | L.DConstraint _ => true 3668 | L.DConstraint _ => true
3669 | L.DClass _ => true
3670 | _ => false 3669 | _ => false
3671 in 3670 in
3672 if isCony then 3671 if isCony then
3673 (ds, acc) 3672 (ds, acc)
3674 else 3673 else
4180 val ct = (L'.CApp (ct, fs), loc) 4179 val ct = (L'.CApp (ct, fs), loc)
4181 in 4180 in
4182 checkCon env e' t ct; 4181 checkCon env e' t ct;
4183 ([(L'.DView (!basis_r, x, n, e', fs), loc)], 4182 ([(L'.DView (!basis_r, x, n, e', fs), loc)],
4184 (env', denv, gs' @ gs)) 4183 (env', denv, gs' @ gs))
4185 end
4186
4187 | L.DClass (x, k, c) =>
4188 let
4189 val k = elabKind env k
4190 val (c', ck, gs') = elabCon (env, denv) c
4191 val (env, n) = E.pushCNamed env x k (SOME c')
4192 val env = E.pushClass env n
4193 in
4194 checkKind env c' ck k;
4195 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
4196 end 4184 end
4197 4185
4198 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) 4186 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
4199 4187
4200 | L.DCookie (x, c) => 4188 | L.DCookie (x, c) =>