diff 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
line wrap: on
line diff
--- a/src/cjr_print.sml	Sun May 03 15:13:00 2009 -0400
+++ b/src/cjr_print.sml	Sun May 03 15:38:49 2009 -0400
@@ -2421,20 +2421,20 @@
                                                 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 @@
                                        (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