From e8f8f3e65c9cb541712cec3c38de80f78d8fdedb Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 5 Nov 2018 18:37:40 +0000
Subject: Ensure function quantifier is in scope when generating C return type

This goes partway to resolving issue #23, as it now generates C code,
but it seems like there is still an issue with the generated C.
---
 src/c_backend.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 6dca1f8a..4e1bde7e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -566,12 +566,15 @@ let cdef_ctyps ctx = function
   | CDEF_reg_dec (_, ctyp, instrs) -> ctyp :: List.concat (List.map instr_ctyps instrs)
   | CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps
   | CDEF_fundef (id, _, _, instrs) ->
-     let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
+     let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
        | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
-     let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in
+     let arg_ctyps, ret_ctyp =
+       List.map (ctyp_of_typ ctx) arg_typs,
+       ctyp_of_typ { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } ret_typ
+     in
      ret_ctyp :: arg_ctyps @ List.concat (List.map instr_ctyps instrs)
 
   | CDEF_startup (id, instrs) | CDEF_finish (id, instrs) -> List.concat (List.map instr_ctyps instrs)
-- 
cgit v1.2.3