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)];*)