diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_compile.ml | 37 | ||||
| -rw-r--r-- | src/parser.mly | 2 |
2 files changed, 25 insertions, 14 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index f977193a..a59f6c80 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -254,23 +254,32 @@ let rec compile_aval l ctx = function (F_id gs, ctyp), [iclear ctyp gs] - | AV_vector ([], _) -> - raise (Reporting.err_general l "Encountered empty vector literal") + | AV_vector ([], typ) -> + let vector_ctyp = ctyp_of_typ ctx typ in + begin match ctyp_of_typ ctx typ with + | CT_fbits (0, _) -> + [], (F_lit (V_bits []), vector_ctyp), [] + | _ -> + let gs = ngensym () in + [idecl vector_ctyp gs; + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int Big_int.zero), CT_fint 64)]], + (F_id gs, vector_ctyp), + [iclear vector_ctyp gs] + end (* Convert a small bitvector to a uint64_t literal. *) | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> - begin - let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in - let len = List.length avals in - match destruct_vector ctx.tc_env typ with - | Some (_, Ord_aux (Ord_inc, _), _) -> - [], (bitstring, CT_fbits (len, false)), [] - | Some (_, Ord_aux (Ord_dec, _), _) -> - [], (bitstring, CT_fbits (len, true)), [] - | Some _ -> - raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") - | None -> - raise (Reporting.err_general l "Encountered vector literal without vector type") + let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let len = List.length avals in + begin match destruct_vector ctx.tc_env typ with + | Some (_, Ord_aux (Ord_inc, _), _) -> + [], (bitstring, CT_fbits (len, false)), [] + | Some (_, Ord_aux (Ord_dec, _), _) -> + [], (bitstring, CT_fbits (len, true)), [] + | Some _ -> + raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") + | None -> + raise (Reporting.err_general l "Encountered vector literal without vector type") end (* Convert a bitvector literal that is larger than 64-bits to a diff --git a/src/parser.mly b/src/parser.mly index 5e448a05..8c4475c4 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1064,6 +1064,8 @@ atomic_exp: { mk_exp (E_record $3) $startpos $endpos } | Lcurly exp With fexp_exp_list Rcurly { mk_exp (E_record_update ($2, $4)) $startpos $endpos } + | Lsquare Rsquare + { mk_exp (E_vector []) $startpos $endpos } | Lsquare exp_list Rsquare { mk_exp (E_vector $2) $startpos $endpos } | Lsquare exp With atomic_exp Eq exp Rsquare |