max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel/local_ctx): use new representation defined at localcontext.lean

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-06 10:47:50 -07:00
parent 2343260ca5
commit bad3f8e77e
2 changed files with 18 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/local_ctx.cpp
View file

@ -24,15 +24,12 @@ bool is_local_decl_ref(expr const & e) { // TODO(Leo): delete
local_decl::local_decl():object_ref(*g_dummy_decl) {}
local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v):
object_ref(mk_cnstr(0, n, un, t, v, sizeof(unsigned) + sizeof(unsigned char))) {
cnstr_set_scalar<unsigned>(raw(), sizeof(object*)*4, idx);
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned), 0);
object_ref(mk_cnstr(1, nat(idx), n, un, t, v)) {
}
local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi):
object_ref(mk_cnstr(0, n, un, t, object_ref(box(0)), sizeof(unsigned) + sizeof(unsigned char))) {
cnstr_set_scalar<unsigned>(raw(), sizeof(object*)*4, idx);
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned), static_cast<unsigned char>(bi));
object_ref(mk_cnstr(0, nat(idx), n, un, t, sizeof(unsigned char))) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4, static_cast<unsigned char>(bi));
}
local_decl::local_decl(local_decl const & d, expr const & t, expr const & v):

23
src/kernel/local_ctx.h
View file

@ -11,6 +11,11 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
/*
inductive LocalDecl
| cdecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo)
| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
*/
class local_decl : public object_ref {
friend class local_ctx;
friend class local_context;
@ -26,16 +31,18 @@ public:
local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; }
friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 0)); }
name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 2)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 3)); }
optional<expr> get_value() const {
/* Remark: if we decide to expose `local_decl` in Lean, we will need to use Lean `option` type. */
if (is_scalar(cnstr_get(raw(), 3))) return none_expr();
else return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 3)));
if (cnstr_tag(raw()) == 0) return none_expr();
return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 4)));
}
binder_info get_info() const {
if (cnstr_tag(raw()) == 0) return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4));
else return binder_info();
}
unsigned get_idx() const { return cnstr_get_scalar<unsigned>(raw(), sizeof(object*)*4); }
binder_info get_info() const { return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned))); }
expr mk_ref() const;
};