Reverse FFI names in export libs more systematically

As pointed out by Yong Kiam, 71569a0 was not enough (and is reverted here).
CakeML · Feb 20, 2017 · e92bf33 · e92bf33
1 parent 71569a0
commit e92bf33
Show file tree

Hide file tree

Showing 9 changed files with 11 additions and 11 deletions.
diff --git a/characteristic/examples/compilation/echoCompileScript.sml b/characteristic/examples/compilation/echoCompileScript.sml
@@ -37,7 +37,7 @@ fun to_bytes alg conf prog =
   end
 
 val extract_bytes = pairSyntax.dest_pair o optionSyntax.dest_some o rconc
-val extract_ffi_names = rev o map stringSyntax.fromHOLstring o fst o listSyntax.dest_list
+val extract_ffi_names = map stringSyntax.fromHOLstring o fst o listSyntax.dest_list
 
 fun write_asm [] = ()
   | write_asm ((name,(bytes,ffi_names))::xs) =

diff --git a/compiler/bootstrap/evaluation/x64BootstrapScript.sml b/compiler/bootstrap/evaluation/x64BootstrapScript.sml
@@ -925,7 +925,7 @@ val () = Lib.say"Writing output: "
 
 val () = time (
   x64_exportLib.write_cake_S stack_mb heap_mb
-    (List.rev (List.map stringSyntax.fromHOLstring (#1 (listSyntax.dest_list ffi_names_tm))))
+    (map stringSyntax.fromHOLstring (#1 (listSyntax.dest_list ffi_names_tm)))
     bytes_tm ) filename
 
 val _ = export_theory();
diff --git a/compiler/eval/benchmarks/benchmarkScript.sml b/compiler/eval/benchmarks/benchmarkScript.sml
@@ -1012,7 +1012,7 @@ val names = ["foo","qsortimp","nqueens","foldl","reverse","fib","btree","queue",
 
 val extract_bytes = pairSyntax.dest_pair o optionSyntax.dest_some o rconc
 
-val extract_ffi_names = rev o map stringSyntax.fromHOLstring o fst o listSyntax.dest_list
+val extract_ffi_names = map stringSyntax.fromHOLstring o fst o listSyntax.dest_list
 
 fun write_asm [] = ()
   | write_asm ((name,(bytes,ffi_names))::xs) =

diff --git a/compiler/eval/targets/arm8_exportLib.sml b/compiler/eval/targets/arm8_exportLib.sml
@@ -94,7 +94,7 @@ fun byte_list_to_asm_lines bytes = let
   in bytes_to_strings xs end;
 
 fun cake_lines stack_mb heap_mb ffi_names bytes_tm =
-  cake_boilerplate_lines stack_mb heap_mb ffi_names @
+  cake_boilerplate_lines stack_mb heap_mb (List.rev ffi_names) @
   byte_list_to_asm_lines bytes_tm;
 
 fun write_cake_S stack_mb heap_mb ffi_names bytes_tm filename = let

diff --git a/compiler/eval/targets/arm_exportLib.sml b/compiler/eval/targets/arm_exportLib.sml
@@ -102,7 +102,7 @@ fun cake_lines stack_mb heap_mb ffi_names bytes_tm =
   byte_list_to_asm_lines bytes_tm;
 
 fun write_cake_S stack_mb heap_mb ffi_names bytes_tm filename = let
-  val lines = cake_lines stack_mb heap_mb ffi_names bytes_tm
+  val lines = cake_lines stack_mb heap_mb (List.rev ffi_names) bytes_tm
   val f = TextIO.openOut filename
   fun each g [] = ()
     | each g (x::xs) = (g x; each g xs)

diff --git a/compiler/eval/targets/export_x64Script.sml b/compiler/eval/targets/export_x64Script.sml
@@ -105,7 +105,7 @@ val ffi_code =
        "";
        "     .p2align 3";
        ""] ++
-     ffi_asm ffi_names ++
+     ffi_asm (REVERSE ffi_names) ++
      MAP (\n. n ++ "\n")
       ["cake_clear:";
        "     callq   cdecl(exit)";

diff --git a/compiler/eval/targets/mips_exportLib.sml b/compiler/eval/targets/mips_exportLib.sml
@@ -72,7 +72,7 @@ fun cake_boilerplate_lines stack_mb heap_mb ffi_names = let
 
 fun cake_tail_lines ffi_names = let
   fun ffi_asm [] = []
-    | ffi_asm (ffi::ffis) = 
+    | ffi_asm (ffi::ffis) =
        ("cake_back_ffi" ^ ffi ^ ":") ::
        (*"     pushq   %rax"::*)
        "     dla $t9, cdecl(ffi" ^ ffi ^ ")"::
@@ -124,7 +124,7 @@ fun cake_lines stack_mb heap_mb ffi_names bytes_tm =
   cake_tail_lines ffi_names;
 
 fun write_cake_S stack_mb heap_mb ffi_names bytes_tm filename = let
-  val lines = cake_lines stack_mb heap_mb ffi_names bytes_tm
+  val lines = cake_lines stack_mb heap_mb (List.rev ffi_names) bytes_tm
   val f = TextIO.openOut filename
   fun each g [] = ()
     | each g (x::xs) = (g x; each g xs)

diff --git a/compiler/eval/targets/riscv_exportLib.sml b/compiler/eval/targets/riscv_exportLib.sml
@@ -8,7 +8,7 @@ fun cake_boilerplate_lines stack_mb heap_mb ffi_names = let
   val stack_line = "    .space  " ^ Int.toString stack_mb ^
                    " * 1024 * 1024   # stack size in bytes"
   fun ffi_asm [] = []
-    | ffi_asm (ffi::ffis) = 
+    | ffi_asm (ffi::ffis) =
        ("cake_ffi" ^ ffi ^ ":") ::
        "     j     cdecl(ffi" ^ ffi ^ ")"::
        "     .p2align 3"::
@@ -95,7 +95,7 @@ fun cake_lines stack_mb heap_mb ffi_names bytes_tm =
   byte_list_to_asm_lines bytes_tm;
 
 fun write_cake_S stack_mb heap_mb ffi_names bytes_tm filename = let
-  val lines = cake_lines stack_mb heap_mb ffi_names bytes_tm
+  val lines = cake_lines stack_mb heap_mb (List.rev ffi_names) bytes_tm
   val f = TextIO.openOut filename
   fun each g [] = ()
     | each g (x::xs) = (g x; each g xs)

diff --git a/compiler/eval/targets/x64_exportLib.sml b/compiler/eval/targets/x64_exportLib.sml
@@ -106,7 +106,7 @@ fun cake_lines stack_mb heap_mb ffi_names bytes_tm =
   byte_list_to_asm_lines bytes_tm;
 
 fun write_cake_S stack_mb heap_mb ffi_names bytes_tm filename = let
-  val lines = cake_lines stack_mb heap_mb ffi_names bytes_tm
+  val lines = cake_lines stack_mb heap_mb (List.rev ffi_names) bytes_tm
   val f = TextIO.openOut filename
   fun each g [] = ()
     | each g (x::xs) = (g x; each g xs)