From e8a03738642f88f75e9af1b993f3f27acaa506d9 Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Wed, 4 Oct 2023 14:25:15 +0100
Subject: [PATCH] Fix a bug where types weren't specialized in top level lets

---
 src/lib/jib_util.ml      |  3 ++-
 test/c/let_option.expect |  1 +
 test/c/let_option.sail   | 17 +++++++++++++++++
 3 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 test/c/let_option.expect
 create mode 100644 test/c/let_option.sail

diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml
index 89a022953..99dbffda6 100644
--- a/src/lib/jib_util.ml
+++ b/src/lib/jib_util.ml
@@ -900,7 +900,8 @@ let ctype_def_map_ctyp f = function
 (* Map over each ctyp in a cdef using map_instr_ctyp *)
 let cdef_map_ctyp f = function
   | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, f ctyp, List.map (map_instr_ctyp f) instrs)
-  | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr_ctyp f) instrs)
+  | CDEF_let (n, bindings, instrs) ->
+      CDEF_let (n, List.map (fun (id, ctyp) -> (id, f ctyp)) bindings, List.map (map_instr_ctyp f) instrs)
   | CDEF_fundef (id, heap_return, args, instrs) ->
       CDEF_fundef (id, heap_return, args, List.map (map_instr_ctyp f) instrs)
   | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs)
diff --git a/test/c/let_option.expect b/test/c/let_option.expect
new file mode 100644
index 000000000..b5c1cd24e
--- /dev/null
+++ b/test/c/let_option.expect
@@ -0,0 +1 @@
+x is None()
diff --git a/test/c/let_option.sail b/test/c/let_option.sail
new file mode 100644
index 000000000..5f7372e04
--- /dev/null
+++ b/test/c/let_option.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+overload operator ^ = {concat_str}
+
+let x : option(bits(32)) = None()
+let y : option(bits(128)) = None()
+
+function main() -> unit = {
+    match x {
+      Some(x) => print_endline("x is " ^ bits_str(x)),
+      _ => print_endline("x is None()"),
+    };
+}