From 2d04ecc7041fff2ec0bc1017c3138d418a1955ad Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 8 Sep 2019 13:42:47 +0200 Subject: [PATCH] refactor(util/object_ref): move and adjust `cnstr_get_ref_t` --- src/library/compiler/ir_interpreter.cpp | 7 ------- src/util/object_ref.h | 7 +++++++ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 5a87547028..567402ab28 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -47,13 +47,6 @@ namespace ir { typedef object_ref lit_val; typedef object_ref ctor_info; -// TODO(Sebastian): move -template -inline T const & cnstr_get_ref_t(object_ref const & o, unsigned i) { - static_assert(sizeof(T) == sizeof(object_ref), "unexpected object wrapper size"); - return *reinterpret_cast(&cnstr_get_ref(o.raw(), i)); -} - bool arg_is_irrelevant(arg const & a) { return is_scalar(a.raw()); } var_id const & arg_var_id(arg const & a) { lean_assert(!arg_is_irrelevant(a)); return cnstr_get_ref_t(a, 0); } diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 7016690159..b470e70d5d 100644 --- a/src/util/object_ref.h +++ b/src/util/object_ref.h @@ -137,6 +137,13 @@ inline object_ref const & cnstr_get_ref(object_ref const & ref, unsigned i) { return cnstr_get_ref(ref.raw(), i); } +template +inline T const & cnstr_get_ref_t(object_ref const & o, unsigned i) { + static_assert(sizeof(T) == sizeof(object_ref), "unexpected object wrapper size"); + return static_cast(cnstr_get_ref(o.raw(), i)); +} + + /* Given `T` which is a subclass of object_ref that wraps a Lean value of type `Ty`, convert a value `o` of `Option Ty` into `optional` */ template optional to_optional(obj_arg o) {