From 143a68b2c43c4302abbbd39c28cac3f9c5f52f4a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 10 Apr 2024 16:46:24 +0200 Subject: Trust rustc regarding `Copy` bounds --- compiler/InterpreterExpressions.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 48a1cce6..444e5788 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) "Can't copy an assumed value other than Option" | TAdt (TAdtId _, _) as ty -> sanity_check __FILE__ __LINE__ - (allow_adt_copy || ty_is_primitively_copyable ty) + (allow_adt_copy || ty_is_copyable ty) meta | TAdt (TTuple, _) -> () (* Ok *) | TAdt @@ -158,7 +158,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) trait_refs = []; } ) -> exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable ty) + (ty_is_copyable ty) meta "The type is not primitively copyable" | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable"); let ctx, fields = @@ -195,7 +195,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) cassert __FILE__ __LINE__ - (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)) + (ty_is_copyable (Substitute.erase_regions sp.sv_ty)) meta "Not primitively copyable"; (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values @@ -529,7 +529,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) "The arguments given to the binop don't have the same type"; (* Equality/inequality check is primitive only for a subset of types *) exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable v1.ty) + (ty_is_copyable v1.ty) meta "Type is not primitively copyable"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) @@ -622,7 +622,7 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta; (* Equality/inequality check is primitive only for a subset of types *) exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable v1.ty) + (ty_is_copyable v1.ty) meta "The type is not primitively copyable"; TLiteral TBool) else -- cgit v1.2.3 From 8894c310cd995f2f1f2abb1ca5232f98aa046274 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 11 Apr 2024 19:05:12 +0200 Subject: Reformat the code --- compiler/InterpreterExpressions.ml | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 444e5788..5f849230 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) const_generics = []; trait_refs = []; } ) -> - exec_assert __FILE__ __LINE__ - (ty_is_copyable ty) - meta "The type is not primitively copyable" + exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta + "The type is not primitively copyable" | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable"); let ctx, fields = List.fold_left_map @@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "The arguments given to the binop don't have the same type"; (* Equality/inequality check is primitive only for a subset of types *) - exec_assert __FILE__ __LINE__ - (ty_is_copyable v1.ty) - meta "Type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "Type is not primitively copyable"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else @@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (* Equality operations *) sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta; (* Equality/inequality check is primitive only for a subset of types *) - exec_assert __FILE__ __LINE__ - (ty_is_copyable v1.ty) - meta "The type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "The type is not primitively copyable"; TLiteral TBool) else (* Other operations: input types are integers *) -- cgit v1.2.3