summaryrefslogtreecommitdiff
path: root/src/cjr_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 15:38:49 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 15:38:49 -0400
commite57a588744ec72e443d69d2e47b4a9a199613745 (patch)
tree09387818d6f755a3b5eec66ad560cbe707f348dd /src/cjr_print.sml
parent92df298250032469bab59565aa4e23a86b4a6e9a (diff)
cookieSec demo
Diffstat (limited to 'src/cjr_print.sml')
-rw-r--r--src/cjr_print.sml15
1 files changed, 7 insertions, 8 deletions
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index cb92588d..4828996c 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2421,20 +2421,20 @@ fun p_file env (ds, ps) =
E.declBinds env d))
env ds
- fun flatFields (t : typ) =
+ fun flatFields always (t : typ) =
case #1 t of
TRecord i =>
let
val xts = E.lookupStruct env i
in
- SOME (map #1 xts :: List.concat (List.mapPartial (flatFields o #2) xts))
+ SOME ((always @ map #1 xts) :: List.concat (List.mapPartial (flatFields [] o #2) xts))
end
| TList (_, i) =>
let
val ts = E.lookupStruct env i
in
case ts of
- [("1", t'), ("2", _)] => flatFields t'
+ [("1", t'), ("2", _)] => flatFields [] t'
| _ => raise Fail "CjrPrint: Bad struct for TList"
end
| _ => NONE
@@ -2448,12 +2448,11 @@ fun p_file env (ds, ps) =
(TRecord i, loc) =>
let
val xts = E.lookupStruct env i
- val xts = case eff of
- ReadCookieWrite =>
- (sigName xts, (TRecord 0, ErrorMsg.dummySpan)) :: xts
- | _ => xts
+ val extra = case eff of
+ ReadCookieWrite => [sigName xts]
+ | _ => []
in
- case flatFields (TRecord i, loc) of
+ case flatFields extra (TRecord i, loc) of
NONE => raise Fail "CjrPrint: flatFields impossible"
| SOME fields' => List.revAppend (fields', fields)
end