Mercurial > urweb
comparison src/elaborate.sml @ 1199:c316ca3c9ec6
Pushing policies through
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 04 Apr 2010 12:29:34 -0400 |
parents | 61c3139eab12 |
children | 950d1e540df6 |
comparison
equal
deleted
inserted
replaced
1197:6d8e3dcb9713 | 1199:c316ca3c9ec6 |
---|---|
2593 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] | 2593 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] |
2594 | L'.DDatabase _ => [] | 2594 | L'.DDatabase _ => [] |
2595 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] | 2595 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] |
2596 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] | 2596 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] |
2597 | L'.DTask _ => [] | 2597 | L'.DTask _ => [] |
2598 | L'.DPolicy _ => [] | |
2598 | 2599 |
2599 and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = | 2600 and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = |
2600 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), | 2601 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), |
2601 ("sgn2", p_sgn env sgn2)];*) | 2602 ("sgn2", p_sgn env sgn2)];*) |
2602 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of | 2603 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of |
3726 (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc) | 3727 (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc) |
3727 in | 3728 in |
3728 checkCon env e1' t1 t1'; | 3729 checkCon env e1' t1 t1'; |
3729 checkCon env e2' t2 t2'; | 3730 checkCon env e2' t2 t2'; |
3730 ([(L'.DTask (e1', e2'), loc)], (env, denv, gs2 @ gs1 @ gs)) | 3731 ([(L'.DTask (e1', e2'), loc)], (env, denv, gs2 @ gs1 @ gs)) |
3732 end | |
3733 | L.DPolicy e1 => | |
3734 let | |
3735 val (e1', t1, gs1) = elabExp (env, denv) e1 | |
3736 | |
3737 val t1' = (L'.CModProj (!basis_r, [], "sql_policy"), loc) | |
3738 in | |
3739 checkCon env e1' t1 t1'; | |
3740 ([(L'.DPolicy e1', loc)], (env, denv, gs1 @ gs)) | |
3731 end | 3741 end |
3732 | 3742 |
3733 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) | 3743 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) |
3734 in | 3744 in |
3735 (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*) | 3745 (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*) |