276 lines
13 KiB
C++
276 lines
13 KiB
C++
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#pragma once
|
|
#include "kernel/environment.h"
|
|
|
|
namespace lean {
|
|
|
|
/** \brief Return the universe level of the type of \c A.
|
|
Throws an exception if the (relaxed) whnf of the type
|
|
of A is not a sort. */
|
|
level get_level(abstract_type_context & ctx, expr const & A);
|
|
|
|
/** \brief Return true iff \c n occurs in \c m */
|
|
bool occurs(expr const & n, expr const & m);
|
|
/** \brief Return true iff there is a constant named \c n in \c m. */
|
|
bool occurs(name const & n, expr const & m);
|
|
|
|
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
|
|
bool is_app_of(expr const & t, name const & f_name);
|
|
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
|
|
bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
|
|
|
|
/** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
|
|
where \c f is a constant */
|
|
optional<expr> unfold_term(environment const & env, expr const & e);
|
|
/** \brief If \c e is of the form <tt>(f a_1 ... a_n)</tt>, where \c f is
|
|
a non-opaque definition, then unfold \c f, and beta reduce.
|
|
Otherwise, return none. */
|
|
optional<expr> unfold_app(environment const & env, expr const & e);
|
|
|
|
/** \brief Reduce (if possible) universe level by 1.
|
|
\pre is_not_zero(l) */
|
|
optional<level> dec_level(level const & l);
|
|
|
|
/** \brief Return true iff \c env has been configured with an impredicative and proof irrelevant Prop. */
|
|
bool is_standard(environment const & env);
|
|
|
|
bool has_poly_unit_decls(environment const & env);
|
|
bool has_eq_decls(environment const & env);
|
|
bool has_heq_decls(environment const & env);
|
|
bool has_prod_decls(environment const & env);
|
|
bool has_lift_decls(environment const & env);
|
|
|
|
/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
|
|
That is, it must be an inductive datatype AND contain a recursive constructor.
|
|
|
|
\remark Records are inductive datatypes, but they are not recursive.
|
|
|
|
\remark For mutually indutive datatypes, \c n is considered recursive
|
|
if there is a constructor taking \c n. */
|
|
bool is_recursive_datatype(environment const & env, name const & n);
|
|
|
|
/** \brief Return true if \c n is a recursive *and* reflexive datatype.
|
|
|
|
We say an inductive type T is reflexive if it contains at least one constructor that
|
|
takes as an argument a function returning T. */
|
|
bool is_reflexive_datatype(abstract_type_context & tc, name const & n);
|
|
|
|
/** \brief Return true iff \c n is an inductive predicate, i.e., an inductive datatype that is in Prop.
|
|
|
|
\remark If \c env does not have Prop (i.e., Type.{0} is not impredicative), then this method always return false. */
|
|
bool is_inductive_predicate(environment const & env, name const & n);
|
|
|
|
/** \brief Return true iff \c n is an inductive type with a recursor with an extra level parameter. */
|
|
bool can_elim_to_type(environment const & env, name const & n);
|
|
|
|
/** \brief Store in \c result the introduction rules of the given inductive datatype.
|
|
\remark this procedure does nothing if \c n is not an inductive datatype. */
|
|
void get_intro_rule_names(environment const & env, name const & n, buffer<name> & result);
|
|
|
|
/** \brief If \c e is a constructor application, then return the name of the constructor.
|
|
Otherwise, return none. */
|
|
optional<name> is_constructor_app(environment const & env, expr const & e);
|
|
|
|
/** \brief If \c e is a constructor application, or a definition that wraps a
|
|
constructor application, then return the name of the constructor.
|
|
Otherwise, return none. */
|
|
optional<name> is_constructor_app_ext(environment const & env, expr const & e);
|
|
|
|
/** \brief Store in \c result a bit-vector indicating which fields of the constructor \c n are
|
|
(computationally) relevant.
|
|
\pre inductive::is_intro_rule(env, n) */
|
|
void get_constructor_relevant_fields(environment const & env, name const & n, buffer<bool> & result);
|
|
|
|
/** \brief Return the index (position) of the given constructor in the inductive datatype declaration.
|
|
\pre inductive::is_intro_rule(env, n) */
|
|
unsigned get_constructor_idx(environment const & env, name const & n);
|
|
|
|
/** Given a C.rec, each minor premise has n arguments, and some of these arguments are inductive
|
|
hypotheses. This function return then number of inductive hypotheses for the minor premise associated with
|
|
the constructor named \c n. */
|
|
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n);
|
|
|
|
/* Store in `rec_args` the recursive arguments of constructor application \c `e`.
|
|
The result is false if `e` is not a constructor application.
|
|
The unsigned value at rec_args represents the arity of the recursive argument.
|
|
The value is only greater than zero for reflexive inductive datatypes such as:
|
|
|
|
inductive inftree (A : Type)
|
|
| leaf : A → inftree
|
|
| node : (nat → inftree) → inftree
|
|
*/
|
|
bool get_constructor_rec_args(environment const & env, expr const & e, buffer<pair<expr, unsigned>> & rec_args);
|
|
|
|
/** \brief Given an expression \c e, return the number of arguments expected arguments.
|
|
|
|
\remark This function computes the type of \c e, and then counts the number of nested
|
|
Pi's. Weak-head-normal-forms are computed for the type of \c e.
|
|
\remark The type and whnf are computed using \c tc. */
|
|
unsigned get_expect_num_args(abstract_type_context & ctx, expr e);
|
|
|
|
/** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type
|
|
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
|
|
binder_info, otherwise the procedure uses the one attached in the domain.
|
|
The procedure returns the "body" of type. */
|
|
expr to_telescope(expr const & type, buffer<expr> & telescope,
|
|
optional<binder_info> const & binfo = optional<binder_info>());
|
|
|
|
/** \brief "Consume" fun/lambda. This procedure creates local constants based on the arguments of \c e
|
|
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
|
|
binder_info, otherwise the procedure uses the one attached to the arguments.
|
|
The procedure returns the "body" of function. */
|
|
expr fun_to_telescope(expr const & e, buffer<expr> & telescope, optional<binder_info> const & binfo);
|
|
|
|
/** \brief Similar to previous procedure, but puts \c type in whnf */
|
|
expr to_telescope(type_checker & ctx, expr type, buffer<expr> & telescope,
|
|
optional<binder_info> const & binfo = optional<binder_info>());
|
|
|
|
/** \brief Create a telescope equality for HoTT library.
|
|
This procedure assumes eq supports dependent elimination.
|
|
For HoTT, we can't use heterogeneous equality. */
|
|
void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs);
|
|
void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs);
|
|
|
|
/** \brief Return the universe where inductive datatype resides
|
|
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt> */
|
|
level get_datatype_level(expr ind_type);
|
|
|
|
expr instantiate_univ_param (expr const & e, name const & p, level const & l);
|
|
|
|
/** \brief Create a format object for a type mismatch where typeof(v) (i.e., v_type) does not match
|
|
expected type \c t. */
|
|
format pp_type_mismatch(formatter const & fmt, expr const & v, expr const & v_type, expr const & t);
|
|
|
|
|
|
expr mk_true();
|
|
bool is_true(expr const & e);
|
|
expr mk_true_intro();
|
|
|
|
bool is_and(expr const & e, expr & arg1, expr & arg2);
|
|
bool is_and(expr const & e);
|
|
expr mk_and(expr const & a, expr const & b);
|
|
expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb);
|
|
expr mk_and_elim_left(abstract_type_context & ctx, expr const & H);
|
|
expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
|
|
|
|
expr mk_unit(level const & l);
|
|
expr mk_unit_mk(level const & l);
|
|
|
|
expr mk_prod(abstract_type_context & ctx, expr const & A, expr const & B);
|
|
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b);
|
|
expr mk_pr1(abstract_type_context & ctx, expr const & p);
|
|
expr mk_pr2(abstract_type_context & ctx, expr const & p);
|
|
|
|
expr mk_unit(level const & l, bool prop);
|
|
expr mk_unit_mk(level const & l, bool prop);
|
|
|
|
expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
|
expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
|
expr mk_pr1(abstract_type_context & ctx, expr const & p, bool prop);
|
|
expr mk_pr2(abstract_type_context & ctx, expr const & p, bool prop);
|
|
|
|
expr mk_nat_one();
|
|
expr mk_nat_add(expr const & e1, expr const & e2);
|
|
|
|
bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f);
|
|
bool is_ite(expr const & e);
|
|
|
|
bool is_iff(expr const & e);
|
|
bool is_iff(expr const & e, expr & lhs, expr & rhs);
|
|
expr mk_iff(expr const & lhs, expr const & rhs);
|
|
expr mk_iff_refl(expr const & a);
|
|
|
|
expr apply_propext(expr const & iff_pr, expr const & iff_term);
|
|
|
|
expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
|
|
expr mk_eq_refl(abstract_type_context & ctx, expr const & a);
|
|
expr mk_eq_symm(abstract_type_context & ctx, expr const & H);
|
|
expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2);
|
|
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
|
|
expr const & x, expr const & y, expr const & xeqy, expr const & h);
|
|
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h);
|
|
|
|
expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H);
|
|
|
|
/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_prop.elim (in HoTT mode) */
|
|
expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y);
|
|
|
|
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
|
|
bool is_eq_rec_core(expr const & e);
|
|
/** \brief Return true iff \c e is a term of the form (eq.rec ....) in the standard library,
|
|
and (eq.nrec ...) in the HoTT library. */
|
|
bool is_eq_rec(environment const & env, expr const & e);
|
|
/** \brief Return true iff \c e is a term of the form (eq.drec ....) in the standard library,
|
|
and (eq.rec ...) in the HoTT library. */
|
|
bool is_eq_drec(environment const & env, expr const & e);
|
|
|
|
bool is_eq(expr const & e);
|
|
bool is_eq(expr const & e, expr & lhs, expr & rhs);
|
|
bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
|
|
/** \brief Return true iff \c e is of the form (eq A a a) */
|
|
bool is_eq_a_a(expr const & e);
|
|
/** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
|
|
bool is_eq_a_a(abstract_type_context & ctx, expr const & e);
|
|
|
|
expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
|
|
bool is_heq(expr const & e);
|
|
bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
|
|
|
|
/** \brief If in HoTT mode, apply lift.down.
|
|
The no_confusion constructions uses lifts in the proof relevant version (aka HoTT mode).
|
|
We must apply lift.down to eliminate the auxiliary lift. */
|
|
optional<expr> lift_down_if_hott(abstract_type_context & ctx, expr const & v);
|
|
|
|
expr mk_false();
|
|
expr mk_empty();
|
|
/** \brief Return false (in standard mode) and empty (in HoTT) mode */
|
|
expr mk_false(environment const & env);
|
|
|
|
bool is_false(expr const & e);
|
|
bool is_empty(expr const & e);
|
|
/** \brief Return true iff \c e is false (in standard mode) or empty (in HoTT) mode */
|
|
bool is_false(environment const & env, expr const & e);
|
|
/** \brief Return an element of type t given an element \c f : false (in standard mode) and empty (in HoTT) mode */
|
|
expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t);
|
|
|
|
bool is_or(expr const & e);
|
|
bool is_or(expr const & e, expr & A, expr & B);
|
|
|
|
/** \brief Return true if \c e is of the form <tt>(not arg)</tt>, and store \c arg in \c a.
|
|
Return false otherwise */
|
|
bool is_not(environment const & env, expr const & e, expr & a);
|
|
bool is_not(expr const & e, expr & a);
|
|
bool is_not(environment const & env, expr const & e);
|
|
expr mk_not(abstract_type_context & ctx, expr const & e);
|
|
|
|
/** \brief Create the term <tt>absurd e not_e : t</tt>. */
|
|
expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e);
|
|
|
|
/** \brief Returns none if \c e is not an application with at least two arguments.
|
|
Otherwise it returns <tt>app_fn(app_fn(e))</tt>. */
|
|
optional<expr> get_binary_op(expr const & e);
|
|
optional<expr> get_binary_op(expr const & e, expr & arg1, expr & arg2);
|
|
|
|
/** \brief Makes n-ary (right-associative) application. */
|
|
expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
|
|
expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
|
|
|
|
expr try_eta(expr const & e);
|
|
expr beta_reduce(expr t);
|
|
expr eta_reduce(expr t);
|
|
expr beta_eta_reduce(expr t);
|
|
|
|
enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
|
|
|
|
/** \brief Infer implicit parameter annotations for the first \c nparams using mode
|
|
specified by \c k. */
|
|
expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
|
|
|
|
void initialize_library_util();
|
|
void finalize_library_util();
|
|
}
|