michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/type_context): revise get_assignment

Browse source 
It is safer to return optional.
This commit is contained in:
Leonardo de Moura 2015-10-31 23:01:19 -07:00
parent 3bc5084bf6
commit 18d9272f22
3 changed files with 29 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/blast/blast.cpp
View file

@ -70,12 +70,18 @@ class blastenv {
return blast::is_mref(e); return blast::is_mref(e);
} }
virtual level const * get_assignment(level const & u) const { virtual optional<level> get_assignment(level const & u) const {
return m_benv.m_curr_state.get_uref_assignment(u); if (auto v = m_benv.m_curr_state.get_uref_assignment(u))
return some_level(*v);
else
return none_level();
} }
virtual expr const * get_assignment(expr const & m) const { virtual optional<expr> get_assignment(expr const & m) const {
return m_benv.m_curr_state.get_mref_assignment(m); if (auto v = m_benv.m_curr_state.get_mref_assignment(m))
return some_expr(*v);
else
return none_expr();
} }
virtual void update_assignment(level const & u, level const & v) { virtual void update_assignment(level const & u, level const & v) {

16
src/library/type_context.cpp
View file

@ -400,7 +400,7 @@ expr type_context::subst_mvar(expr const & e) {
buffer<expr> args; buffer<expr> args;
expr const & m = get_app_rev_args(e, args); expr const & m = get_app_rev_args(e, args);
lean_assert(is_mvar(m)); lean_assert(is_mvar(m));
expr const * v = get_assignment(m); optional<expr> v = get_assignment(m);
lean_assert(v); lean_assert(v);
return apply_beta(*v, args.size(), args.data()); return apply_beta(*v, args.size(), args.data());
} }
@ -1705,12 +1705,18 @@ unsigned default_type_context::mvar_idx(expr const & m) const {
return mlocal_name(m).get_numeral(); return mlocal_name(m).get_numeral();
} }
level const * default_type_context::get_assignment(level const & u) const { optional<level> default_type_context::get_assignment(level const & u) const {
return m_assignment.m_uassignment.find(uvar_idx(u)); if (auto v = m_assignment.m_uassignment.find(uvar_idx(u)))
return some_level(*v);
else
return none_level();
} }
expr const * default_type_context::get_assignment(expr const & m) const { optional<expr> default_type_context::get_assignment(expr const & m) const {
return m_assignment.m_eassignment.find(mvar_idx(m)); if (auto v = m_assignment.m_eassignment.find(mvar_idx(m)))
return some_expr(*v);
else
return none_expr();
} }
void default_type_context::update_assignment(level const & u, level const & v) { void default_type_context::update_assignment(level const & u, level const & v) {

16
src/library/type_context.h
View file

@ -243,14 +243,14 @@ public:
virtual bool is_mvar(expr const & e) const = 0; virtual bool is_mvar(expr const & e) const = 0;
/** \brief Return the assignment for universe unification variable /** \brief Return the assignment for universe unification variable
\c u, and nullptr if it is not assigned. \c u, and none if it is not assigned.
\pre is_uvar(u) */ \pre is_uvar(u) */
virtual level const * get_assignment(level const & u) const = 0; virtual optional<level> get_assignment(level const & u) const = 0;
/** \brief Return the assignment for unification variable /** \brief Return the assignment for unification variable
\c m, and nullptr if it is not assigned. \c m, and none if it is not assigned.
\pre is_mvar(u) */ \pre is_mvar(u) */
virtual expr const * get_assignment(expr const & m) const = 0; virtual optional<expr> get_assignment(expr const & m) const = 0;
/** \brief Update the assignment for \c u. /** \brief Update the assignment for \c u.
\pre is_uvar(u) */ \pre is_uvar(u) */
@ -297,8 +297,8 @@ public:
assign unassigned metavariables in the given terms. */ assign unassigned metavariables in the given terms. */
virtual bool on_is_def_eq_failure(expr &, expr &); virtual bool on_is_def_eq_failure(expr &, expr &);
bool is_assigned(level const & u) const { return get_assignment(u) != nullptr; } bool is_assigned(level const & u) const { return static_cast<bool>(get_assignment(u)); }
bool is_assigned(expr const & m) const { return get_assignment(m) != nullptr; } bool is_assigned(expr const & m) const { return static_cast<bool>(get_assignment(m)); }
bool has_assigned_uvar(level const & l) const; bool has_assigned_uvar(level const & l) const;
bool has_assigned_uvar(levels const & ls) const; bool has_assigned_uvar(levels const & ls) const;
@ -409,8 +409,8 @@ public:
virtual bool is_tmp_local(expr const & e) const; virtual bool is_tmp_local(expr const & e) const;
virtual bool is_uvar(level const & l) const; virtual bool is_uvar(level const & l) const;
virtual bool is_mvar(expr const & e) const; virtual bool is_mvar(expr const & e) const;
virtual level const * get_assignment(level const & u) const; virtual optional<level> get_assignment(level const & u) const;
virtual expr const * get_assignment(expr const & m) const; virtual optional<expr> get_assignment(expr const & m) const;
virtual void update_assignment(level const & u, level const & v); virtual void update_assignment(level const & u, level const & v);
virtual void update_assignment(expr const & m, expr const & v); virtual void update_assignment(expr const & m, expr const & v);
virtual level mk_uvar(); virtual level mk_uvar();