diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/c_backend.ml | 50 | ||||
| -rw-r--r-- | src/specialize.ml | 18 |
2 files changed, 65 insertions, 3 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 88b01d87..a875405d 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1374,6 +1374,44 @@ let rec codegen_conversion l clexp cval = | CT_ref ctyp_to, ctyp_from -> codegen_conversion l (CL_addr clexp) cval + | CT_vector (_, ctyp_elem_to), CT_vector (_, ctyp_elem_from) -> + let i = ngensym () in + let from = ngensym () in + let into = ngensym () in + ksprintf string " KILL(%s)(%s);" (sgen_ctyp_name ctyp_to) (sgen_clexp clexp) ^^ hardline + ^^ ksprintf string " internal_vector_init_%s(%s, %s.len);" (sgen_ctyp_name ctyp_to) (sgen_clexp clexp) (sgen_cval cval) ^^ hardline + ^^ ksprintf string " for (int %s = 0; %s < %s.len; %s++) {" (sgen_name i) (sgen_name i) (sgen_cval cval) (sgen_name i) ^^ hardline + ^^ (if is_stack_ctyp ctyp_elem_from then + ksprintf string " %s %s = %s.data[%s];" (sgen_ctyp ctyp_elem_from) (sgen_name from) (sgen_cval cval) (sgen_name i) + else + ksprintf string " %s %s;" (sgen_ctyp ctyp_elem_from) (sgen_name from) ^^ hardline + ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp_elem_from) (sgen_name from) ^^ hardline + ^^ ksprintf string " COPY(%s)(&%s, %s.data[%s]);" (sgen_ctyp_name ctyp_elem_from) (sgen_name from) (sgen_cval cval) (sgen_name i) + ) + ^^ hardline + ^^ ksprintf string " %s %s;" (sgen_ctyp ctyp_elem_to) (sgen_name into) + ^^ (if is_stack_ctyp ctyp_elem_to then + empty + else + hardline ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp_elem_to) (sgen_name into) + ) + ^^ nest 2 (hardline + ^^ codegen_conversion l (CL_id (into, ctyp_elem_to)) (V_id (from, ctyp_elem_from))) + ^^ hardline + ^^ (if is_stack_ctyp ctyp_elem_to then + ksprintf string " %s.data[%s] = %s;" (sgen_clexp_pure clexp) (sgen_name i) (sgen_name into) + else + ksprintf string " COPY(%s)(&((%s)->data[%s]), %s);" (sgen_ctyp_name ctyp_elem_to) (sgen_clexp clexp) (sgen_name i) (sgen_name into) + ^^ hardline ^^ ksprintf string " KILL(%s)(&%s);" (sgen_ctyp_name ctyp_elem_to) (sgen_name into) + ) + ^^ (if is_stack_ctyp ctyp_elem_from then + empty + else + hardline ^^ ksprintf string " KILL(%s)(&%s);" (sgen_ctyp_name ctyp_elem_from) (sgen_name from) + ) + ^^ hardline + ^^ string " }" + (* If we have to convert between tuple types, convert the fields individually. *) | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from -> let len = List.length ctyps_to in @@ -2019,6 +2057,17 @@ let codegen_vector ctx (direction, ctyp) = ^^ string " }\n" ^^ string "}" in + let vector_equal = + let open Printf in + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ string " if (op1.len != op2.len) return false;\n" + ^^ string " bool result = true;" + ^^ string " for (int i = 0; i < op1.len; i++) {\n" + ^^ ksprintf string " result &= EQUAL(%s)(op1.data[i], op2.data[i]);" (sgen_ctyp_name ctyp) + ^^ string " }\n" + ^^ ksprintf string " return result;\n" + ^^ string "}" + in begin generated := IdSet.add id !generated; vector_typedef ^^ twice hardline @@ -2028,6 +2077,7 @@ let codegen_vector ctx (direction, ctyp) = ^^ vector_access ^^ twice hardline ^^ vector_set ^^ twice hardline ^^ vector_update ^^ twice hardline + ^^ vector_equal ^^ twice hardline ^^ internal_vector_update ^^ twice hardline ^^ internal_vector_init ^^ twice hardline end diff --git a/src/specialize.ml b/src/specialize.ml index bbf74f46..cfd80cce 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -381,15 +381,27 @@ let specialize_id_valspec spec instantiations id ast = let spec_ids = ref IdSet.empty in let specialize_instance instantiation = - let safe_instantiation, reverse = safe_instantiation instantiation in - (* Replace the polymorphic type variables in the type with their concrete instantiation. *) - let typ = remove_implicit (Type_check.subst_unifiers reverse (Type_check.subst_unifiers safe_instantiation typ)) in + let uninstantiated = quant_kopts typq |> List.map kopt_kid |> List.filter (fun v -> not (KBindings.mem v instantiation)) |> KidSet.of_list in (* Collect any new type variables introduced by the instantiation *) let collect_kids kidsets = KidSet.elements (List.fold_left KidSet.union KidSet.empty kidsets) in let typ_frees = KBindings.bindings instantiation |> List.map snd |> List.map typ_arg_frees |> collect_kids in let int_frees = KBindings.bindings instantiation |> List.map snd |> List.map typ_arg_int_frees |> collect_kids in + let typq, typ = + List.fold_left (fun (typq, typ) free -> + if KidSet.mem free uninstantiated then + let fresh_v = prepend_kid "o#" free in + typquant_subst_kid free fresh_v typq, subst_kid typ_subst free fresh_v typ + else + typq, typ + ) (typq, typ) (typ_frees @ int_frees) + in + + let safe_instantiation, reverse = safe_instantiation instantiation in + (* Replace the polymorphic type variables in the type with their concrete instantiation. *) + let typ = remove_implicit (Type_check.subst_unifiers reverse (Type_check.subst_unifiers safe_instantiation typ)) in + (* Remove type variables from the type quantifier. *) let kopts, constraints = quant_split typq in let constraints = instantiate_constraints safe_instantiation constraints in |