diff options
| -rw-r--r-- | src/bytecode_util.ml | 7 | ||||
| -rw-r--r-- | src/c_backend.ml | 16 | ||||
| -rw-r--r-- | test/c/option_nest.expect | 1 | ||||
| -rw-r--r-- | test/c/option_nest.sail | 18 |
4 files changed, 33 insertions, 9 deletions
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index fa41e1e1..4320e945 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -626,6 +626,11 @@ let cdef_map_instr f = function | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp) | CDEF_type tdef -> CDEF_type tdef +let ctype_def_map_ctyp f = function + | CTD_enum (id, ids) -> CTD_enum (id, ids) + | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors) + | CTD_variant (id, ctors) -> CTD_variant (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors) + (** Map over each ctyp in a cdef using map_instr_ctyp *) let cdef_map_ctyp f = function | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, f ctyp, List.map (map_instr_ctyp f) instrs) @@ -634,7 +639,7 @@ let cdef_map_ctyp f = function | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs) | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr_ctyp f) instrs) | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, List.map f ctyps, f ctyp) - | CDEF_type tdef -> CDEF_type tdef (* FIXME *) + | CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef) (* Map over all sequences of instructions contained within an instruction *) let rec map_instrs f (I_aux (instr, aux)) = diff --git a/src/c_backend.ml b/src/c_backend.ml index d79a2957..62310f60 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1781,7 +1781,7 @@ let flatten_instrs = | cdef -> cdef -let rec specialize_variants ctx = +let rec specialize_variants ctx prior = let unifications = ref (Bindings.empty) in @@ -1859,8 +1859,8 @@ let rec specialize_variants ctx = } in let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in - let cdefs, ctx = specialize_variants ctx cdefs in - CDEF_type (CTD_variant (var_id, new_ctors)) :: cdefs, ctx + let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in + specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs | cdef :: cdefs -> let remove_poly (I_aux (instr, aux)) = @@ -1870,10 +1870,9 @@ let rec specialize_variants ctx = | instr -> I_aux (instr, aux) in let cdef = cdef_map_instr remove_poly cdef in - let cdefs, ctx = specialize_variants ctx cdefs in - cdef :: cdefs, ctx + specialize_variants ctx (cdef :: prior) cdefs - | [] -> [], ctx + | [] -> List.rev prior, ctx (** Once we specialize variants, there may be additional type dependencies which could be in the wrong order. As such we need to @@ -2834,9 +2833,10 @@ let codegen_ctg ctx = function any auxillary type definitions that are required. *) let codegen_def ctx def = let ctyps = cdef_ctyps ctx def in - (* We should have erased only polymorphism introduced by variants at this point! *) + (* We should have erased any polymorphism introduced by variants at this point! *) if List.exists is_polymorphic ctyps then let polymorphic_ctyps = List.filter is_polymorphic ctyps in + prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); c_error (Printf.sprintf "Found polymorphic types:\n%s\nwhile generating definition." (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps)) else @@ -2966,7 +2966,7 @@ let compile_ast ctx (Defs defs) = let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in - let cdefs, ctx = specialize_variants ctx cdefs in + let cdefs, ctx = specialize_variants ctx [] cdefs in let cdefs = sort_ctype_defs cdefs in let cdefs = optimize ctx cdefs in (* diff --git a/test/c/option_nest.expect b/test/c/option_nest.expect new file mode 100644 index 00000000..9daeafb9 --- /dev/null +++ b/test/c/option_nest.expect @@ -0,0 +1 @@ +test diff --git a/test/c/option_nest.sail b/test/c/option_nest.sail new file mode 100644 index 00000000..995bf074 --- /dev/null +++ b/test/c/option_nest.sail @@ -0,0 +1,18 @@ + +union test ('a : Type) = { + Just : 'a, + Nothing : unit +} + +union option ('a : Type) = { + None : unit, + Some : 'a +} + +val "print_endline" : string -> unit + +function main() : unit -> unit = { + let _ : test(option(int)) = Just(None()); + let Just(Some(x)) = Just(Some("test")); + print_endline(x) +}
\ No newline at end of file |