c4c548dc5d
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.
The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:
try-for (T1 ORELSE T2) 5
It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
78 lines
2.3 KiB
C++
78 lines
2.3 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 <utility>
|
|
#include "kernel/environment.h"
|
|
#include "kernel/formatter.h"
|
|
|
|
namespace lean {
|
|
class frontend;
|
|
/**
|
|
\brief Expression elaborator for the Lean default frontend, it is responsible for "filling" holes
|
|
in terms left by the user. This is the main module resposible for computing
|
|
the value of implicit arguments. It is based on the general purpose elaborator defined at
|
|
library/elaborator/elaborator.h
|
|
*/
|
|
class frontend_elaborator {
|
|
class imp;
|
|
std::shared_ptr<imp> m_ptr;
|
|
static void print(imp * ptr);
|
|
public:
|
|
explicit frontend_elaborator(frontend const & fe);
|
|
~frontend_elaborator();
|
|
|
|
/**
|
|
\brief Elaborate the given expression.
|
|
*/
|
|
expr operator()(expr const & e);
|
|
/**
|
|
\brief Elaborate the given type and expression. The typeof(e) == t.
|
|
This information is used by the elaborator. The result is a new
|
|
elaborated type and expression.
|
|
*/
|
|
std::pair<expr, expr> operator()(name const & n, expr const & t, expr const & e);
|
|
|
|
/**
|
|
\brief If \c e is an expression instantiated by the elaborator, then it
|
|
returns the expression (the one with "holes") used to generate \c e.
|
|
Otherwise, it just returns \c e.
|
|
*/
|
|
expr const & get_original(expr const & e) const;
|
|
|
|
void clear();
|
|
|
|
environment const & get_environment() const;
|
|
};
|
|
|
|
/**
|
|
\brief Create a choice expression for the given functions.
|
|
It is used to mark which functions can be used in a particular application.
|
|
The elaborator decides which one should be used based on the type of the arguments.
|
|
|
|
\pre num_fs >= 2
|
|
*/
|
|
expr mk_choice(unsigned num_fs, expr const * fs);
|
|
/**
|
|
\brief Return true iff \c e is an expression created using \c mk_choice.
|
|
*/
|
|
bool is_choice(expr const & e);
|
|
/**
|
|
\brief Return the number of alternatives in a choice expression.
|
|
We have that <tt>get_num_choices(mk_choice(n, fs)) == n</tt>.
|
|
|
|
\pre is_choice(e)
|
|
*/
|
|
unsigned get_num_choices(expr const & e);
|
|
/**
|
|
\brief Return the (i+1)-th alternative of a choice expression.
|
|
|
|
\pre is_choice(e)
|
|
\pre i < get_num_choices(e)
|
|
*/
|
|
expr const & get_choice(expr const & e, unsigned i);
|
|
}
|