comparison src/cjr_print.sml @ 779:7394368a5cad

cookieSec demo
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 May 2009 15:38:49 -0400
parents c125df6fabfc
children ef6de4075dc1
comparison
equal deleted inserted replaced
778:7b47fc964a0f 779:7394368a5cad
2419 val (pds, env) = ListUtil.foldlMap (fn (d, env) => 2419 val (pds, env) = ListUtil.foldlMap (fn (d, env) =>
2420 (p_decl env d, 2420 (p_decl env d,
2421 E.declBinds env d)) 2421 E.declBinds env d))
2422 env ds 2422 env ds
2423 2423
2424 fun flatFields (t : typ) = 2424 fun flatFields always (t : typ) =
2425 case #1 t of 2425 case #1 t of
2426 TRecord i => 2426 TRecord i =>
2427 let 2427 let
2428 val xts = E.lookupStruct env i 2428 val xts = E.lookupStruct env i
2429 in 2429 in
2430 SOME (map #1 xts :: List.concat (List.mapPartial (flatFields o #2) xts)) 2430 SOME ((always @ map #1 xts) :: List.concat (List.mapPartial (flatFields [] o #2) xts))
2431 end 2431 end
2432 | TList (_, i) => 2432 | TList (_, i) =>
2433 let 2433 let
2434 val ts = E.lookupStruct env i 2434 val ts = E.lookupStruct env i
2435 in 2435 in
2436 case ts of 2436 case ts of
2437 [("1", t'), ("2", _)] => flatFields t' 2437 [("1", t'), ("2", _)] => flatFields [] t'
2438 | _ => raise Fail "CjrPrint: Bad struct for TList" 2438 | _ => raise Fail "CjrPrint: Bad struct for TList"
2439 end 2439 end
2440 | _ => NONE 2440 | _ => NONE
2441 2441
2442 val fields = foldl (fn ((ek, _, _, ts, _, _), fields) => 2442 val fields = foldl (fn ((ek, _, _, ts, _, _), fields) =>
2446 | Action eff => 2446 | Action eff =>
2447 case List.nth (ts, length ts - 2) of 2447 case List.nth (ts, length ts - 2) of
2448 (TRecord i, loc) => 2448 (TRecord i, loc) =>
2449 let 2449 let
2450 val xts = E.lookupStruct env i 2450 val xts = E.lookupStruct env i
2451 val xts = case eff of 2451 val extra = case eff of
2452 ReadCookieWrite => 2452 ReadCookieWrite => [sigName xts]
2453 (sigName xts, (TRecord 0, ErrorMsg.dummySpan)) :: xts 2453 | _ => []
2454 | _ => xts
2455 in 2454 in
2456 case flatFields (TRecord i, loc) of 2455 case flatFields extra (TRecord i, loc) of
2457 NONE => raise Fail "CjrPrint: flatFields impossible" 2456 NONE => raise Fail "CjrPrint: flatFields impossible"
2458 | SOME fields' => List.revAppend (fields', fields) 2457 | SOME fields' => List.revAppend (fields', fields)
2459 end 2458 end
2460 | _ => raise Fail "CjrPrint: Last argument of action isn't record") 2459 | _ => raise Fail "CjrPrint: Last argument of action isn't record")
2461 [] ps 2460 [] ps