7772c16033
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms. If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions. If they are not, instead of throwing an error, we try again expanding the opaque terms. This seems to be the best of both worlds. The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
35 lines
1.2 KiB
C++
35 lines
1.2 KiB
C++
/*
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#pragma once
|
|
#include <memory>
|
|
#include "kernel/expr.h"
|
|
#include "kernel/environment.h"
|
|
#include "kernel/context.h"
|
|
|
|
namespace lean {
|
|
class environment;
|
|
class options;
|
|
class metavar_env;
|
|
/** \brief Functional object for normalizing expressions */
|
|
class normalizer {
|
|
class imp;
|
|
std::unique_ptr<imp> m_ptr;
|
|
public:
|
|
normalizer(ro_environment const & env);
|
|
normalizer(ro_environment const & env, unsigned max_depth);
|
|
normalizer(ro_environment const & env, options const & opts);
|
|
~normalizer();
|
|
|
|
expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque = false);
|
|
expr operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque = false);
|
|
expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false);
|
|
|
|
void clear();
|
|
};
|
|
/** \brief Normalize \c e using the environment \c env and context \c ctx */
|
|
expr normalize(expr const & e, ro_environment const & env, context const & ctx = context(), bool unfold_opaque = false);
|
|
}
|