Fix compiler{32,64}Prog for I/O modes

CakeML · Nov 5, 2018 · f1056b0 · f1056b0
1 parent 29b077c
commit f1056b0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml
@@ -248,7 +248,7 @@ val main_spec = Q.store_thm("main_spec",
     \\ CONV_TAC SWAP_EXISTS_CONV
     \\ qexists_tac`fs`
     \\ xsimpl)
-  \\ xlet_auto >- (xsimpl \\ fs[FD_stdin])
+  \\ xlet_auto >- (xsimpl \\ fs[FD_stdin, STD_streams_get_mode])
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
   \\ fs [full_compile_32_def]

diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml
@@ -267,7 +267,7 @@ val main_spec = Q.store_thm("main_spec",
     \\ CONV_TAC SWAP_EXISTS_CONV
     \\ qexists_tac`fs`
     \\ xsimpl)
-  \\ xlet_auto >- (xsimpl \\ fs[FD_stdin])
+  \\ xlet_auto >- (xsimpl \\ fs[FD_stdin, STD_streams_get_mode])
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
   \\ fs [full_compile_64_def]