Start working on a solution for correctly monomorphising polymorphic variant types

3 files changed, 95 insertions, 17 deletions

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index b11b70d0..c3e61956 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -164,6 +164,7 @@ let rec string_of_fragment ?zencode:(zencode=true) = function
   | F_have_exception -> "have_exception"
   | F_current_exception -> "(*current_exception)"
   | F_raw raw -> raw
+  | F_poly f -> "POLY(" ^ string_of_fragment ~zencode:zencode f ^ ")"
 and string_of_fragment' ?zencode:(zencode=true) f =
   match f with
   | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")"
@@ -171,7 +172,7 @@ and string_of_fragment' ?zencode:(zencode=true) f =
 
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
-let rec string_of_ctyp = function
+and string_of_ctyp = function
   | CT_int -> "mpz_t"
   | CT_bits true -> "bv_t(dec)"
   | CT_bits false -> "bv_t(inc)"
@@ -189,6 +190,15 @@ let rec string_of_ctyp = function
   | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")"
   | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")"
   | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")"
+  | CT_poly -> "*"
+
+let rec is_polymorphic = function
+  | CT_int | CT_int64 | CT_bits _ | CT_bits64 _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
+  | CT_tup ctyps -> List.exists is_polymorphic ctyps
+  | CT_enum _ -> false
+  | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
+  | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
+  | CT_poly -> true
 
 let pp_id id =
   string (string_of_id id)
@@ -475,3 +485,41 @@ let make_dot id graph =
   output_string out_chan "}\n";
   Util.opt_colors := true;
   close_out out_chan
+
+(** Map over each instruction within an instruction, bottom-up *)
+let rec map_instr f (I_aux (instr, aux)) =
+  let instr = match instr with
+    | I_decl _ | I_init _ | I_reset _ | I_reinit _
+      | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+      | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr
+    | I_if (cval, instrs1, instrs2, ctyp) ->
+       I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp)
+    | I_block instrs ->
+       I_block (List.map (map_instr f) instrs)
+    | I_try_block instrs ->
+       I_try_block (List.map (map_instr f) instrs)
+  in
+  f (I_aux (instr, aux))
+
+(** Map over each instruction in a cdef using map_instr *)
+let cdef_map_instr f = function
+  | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, List.map (map_instr f) instrs)
+  | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr f) instrs)
+  | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr f) instrs)
+  | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr f) instrs)
+  | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr f) instrs)
+  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+  | CDEF_type tdef -> CDEF_type tdef
+
+(* Map over all sequences of instructions contained within an instruction *)
+let rec map_instrs f (I_aux (instr, aux)) =
+  let instr = match instr with
+    | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr
+    | I_if (cval, instrs1, instrs2, ctyp) ->
+       I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp)
+    | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
+    | I_block instrs -> I_block (f (List.map (map_instrs f) instrs))
+    | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs))
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr
+  in
+  I_aux (instr, aux)
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 433e3d85..e5ce1ff9 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -210,6 +210,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_exist (_, _, typ) -> ctyp_of_typ ctx typ
 
+  | Typ_var kid -> CT_poly (* c_error ~loc:l ("Polymorphic type encountered " ^ string_of_kid kid) *)
+
   | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
 
 let rec is_stack_ctyp ctyp = match ctyp with
@@ -219,6 +221,7 @@ let rec is_stack_ctyp ctyp = match ctyp with
   | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (*FIXME*)
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
   | CT_ref ctyp -> true
+  | CT_poly -> true
 
 let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ)
 
@@ -538,18 +541,6 @@ let clexp_ctyp = function
   | CL_have_exception -> CT_bool
   | CL_current_exception ctyp -> ctyp
 
-let rec map_instrs f (I_aux (instr, aux)) =
-  let instr = match instr with
-    | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr
-    | I_if (cval, instrs1, instrs2, ctyp) ->
-       I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp)
-    | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
-    | I_block instrs -> I_block (f (List.map (map_instrs f) instrs))
-    | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr
-  in
-  I_aux (instr, aux)
-
 let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
 
 let rec instr_ctyps (I_aux (instr, aux)) =
@@ -821,10 +812,12 @@ let compile_funcall l ctx id args typ =
 
   let setup_arg ctyp aval =
     let arg_setup, cval, arg_cleanup = compile_aval ctx aval in
-    setup := List.rev arg_setup @ [icomment (string_of_ctyp (cval_ctyp cval))] @ !setup;
+    setup := List.rev arg_setup @ [icomment (string_of_ctyp ctyp ^ " <- " ^ string_of_ctyp (cval_ctyp cval))] @ !setup;
     cleanup := arg_cleanup @ !cleanup;
     let have_ctyp = cval_ctyp cval in
-    if ctyp_equal ctyp have_ctyp then
+    if is_polymorphic ctyp then
+      (F_poly (fst cval), have_ctyp)
+    else if ctyp_equal ctyp have_ctyp then
       cval
     else
       let gs = gensym () in
@@ -873,7 +866,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
      let id_ctyp = ctyp_of_typ ctx typ in
      c_debug (lazy ("Adding local " ^ string_of_id pid ^ " : " ^ string_of_ctyp id_ctyp));
      let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
-     [idecl ctyp pid; icopy (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx
+     [idecl id_ctyp pid; icopy (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx
 
   | AP_tup apats, (frag, ctyp) ->
      begin
@@ -1799,6 +1792,36 @@ let flatten_instrs ctx =
 
   | cdef -> [cdef]
 
+let rec specialize_variants ctx =
+  let specialize_constructor ctx ctor_id ctyp =
+    let ctyps = match ctyp with
+    | CT_tup ctyps -> ctyps
+    | ctyp -> [ctyp]
+    in
+    function
+    | I_aux (I_funcall (clexp, extern, id, cvals), aux) as instr when Id.compare id ctor_id = 0 ->
+       assert (List.length ctyps = List.length cvals);
+       List.iter2 (fun cval ctyp -> print_endline (Pretty_print_sail.to_string (pp_cval cval) ^ " -> " ^ string_of_ctyp ctyp)) cvals ctyps;
+       instr
+    | instr -> instr
+  in
+
+  function
+  | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
+     let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
+     List.iter (fun (id, ctyp) -> prerr_endline (Printf.sprintf "%s : %s" (string_of_id id) (string_of_ctyp ctyp))) polymorphic_ctors;
+     let cdefs =
+       List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
+                      cdefs
+                      polymorphic_ctors
+     in
+     cdef :: specialize_variants ctx cdefs
+
+  | cdef :: cdefs ->
+     cdef :: specialize_variants ctx cdefs
+
+  | [] -> []
+
               (*
 (* When this optimization fires we know we have bytecode of the form
 
@@ -1867,6 +1890,7 @@ let optimize ctx cdefs =
   let nothing cdefs = cdefs in
   cdefs
   |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing)
+  |> specialize_variants ctx
 (* |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) *)
 
 (**************************************************************************)
@@ -1896,6 +1920,7 @@ let rec sgen_ctyp = function
   | CT_string -> "sail_string"
   | CT_real -> "real"
   | CT_ref ctyp -> sgen_ctyp ctyp ^ "*"
+  | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
 
 let rec sgen_ctyp_name = function
   | CT_unit -> "unit"
@@ -1914,6 +1939,7 @@ let rec sgen_ctyp_name = function
   | CT_string -> "sail_string"
   | CT_real -> "real"
   | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
+  | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
 
 let sgen_cval_param (frag, ctyp) =
   match ctyp with
@@ -2120,7 +2146,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      separate_map hardline (fun str -> string ("  " ^ str)) (List.rev prev)
      ^^ hardline
      ^^ string (Printf.sprintf "  return %s;" ret)
-        
+
   | I_comment str ->
      string ("  /* " ^ str ^ " */")
 
diff --git a/src/specialize.ml b/src/specialize.ml
index 148b511c..578b139a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -494,6 +494,7 @@ let specialize_variants ((Defs defs) as ast) env =
          let specialize_tu (Tu_aux (Tu_ty_id (typ, id), annot)) =
            ctors := id :: !ctors;
            let is = instantiations_of id ast in
+           List.iter (fun i -> print_endline (string_of_instantiation i)) is;
            let is = List.sort_uniq (fun i1 i2 -> String.compare (string_of_instantiation i1) (string_of_instantiation i2)) is in
            List.map (fun i ->
                let i = fix_instantiation i in
@@ -525,7 +526,10 @@ let specialize_variants ((Defs defs) as ast) env =
 let rec specialize ast env =
   let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in
   if IdSet.is_empty ids then
+    ast, env
+           (*
     specialize_variants ast env
+            *)
   else
     let ast, env = specialize_ids ids ast in
     specialize ast env