220 lines
9.3 KiB
C++
220 lines
9.3 KiB
C++
/*
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#pragma once
|
|
#include "runtime/pair_ref.h"
|
|
#include "runtime/list_ref.h"
|
|
#include "util/name_hash_set.h"
|
|
#include "kernel/expr.h"
|
|
#include "kernel/type_checker.h"
|
|
#include "library/constants.h"
|
|
#include "library/util.h"
|
|
|
|
namespace lean {
|
|
/* Return the `some(n)` if `I` is the name of an inductive datatype that contains only constructors with 0-arguments,
|
|
and `n` is `1`, `2` or `4`, i.e., the number of bytes that should be used to store a value of this type.
|
|
Otherwise, it return `none`.
|
|
Remark: if the inductive datatype `I` has more than `2^32` constructors (very unlikely), the result is also `none`. */
|
|
optional<unsigned> is_enum_type(environment const & env, name const & I);
|
|
|
|
optional<expr> to_uint_type(unsigned nbytes);
|
|
|
|
/* A "compiler" declaration `x := e` */
|
|
typedef pair_ref<name, expr> comp_decl;
|
|
typedef list_ref<comp_decl> comp_decls;
|
|
|
|
void trace_comp_decl(comp_decl const & d);
|
|
void trace_comp_decls(comp_decls const & ds);
|
|
|
|
unsigned get_num_nested_lambdas(expr e);
|
|
|
|
bool is_lcnf_atom(expr const & e);
|
|
|
|
expr elim_trivial_let_decls(expr const & e);
|
|
|
|
bool has_inline_attribute(environment const & env, name const & n);
|
|
bool has_noinline_attribute(environment const & env, name const & n);
|
|
bool has_inline_if_reduce_attribute(environment const & env, name const & n);
|
|
bool has_never_extract_attribute(environment const & env, name const & n);
|
|
|
|
expr unfold_macro_defs(environment const & env, expr const & e);
|
|
|
|
/* Return true if the given argument is mdata relevant to the compiler
|
|
|
|
Remark: we currently don't keep any metadata in the compiler. */
|
|
inline bool is_lc_mdata(expr const &) { return false; }
|
|
|
|
bool is_cases_on_recursor(environment const & env, name const & n);
|
|
/* We defined the "arity" of a cases_on application as the sum:
|
|
```
|
|
number of inductive parameters +
|
|
1 + // motive
|
|
number of inductive indices +
|
|
1 + // major premise
|
|
number of constructors // cases_on has a minor premise for each constructor
|
|
```
|
|
\pre is_cases_on_recursor(env, c) */
|
|
unsigned get_cases_on_arity(environment const & env, name const & c, bool before_erasure = true);
|
|
/* Return the `inductive_val` for the cases_on constant `c`. */
|
|
inline inductive_val get_cases_on_inductive_val(environment const & env, name const & c) {
|
|
lean_assert(is_cases_on_recursor(env, c));
|
|
return env.get(c.get_prefix()).to_inductive_val();
|
|
}
|
|
inline inductive_val get_cases_on_inductive_val(environment const & env, expr const & c) {
|
|
lean_assert(is_constant(c));
|
|
return get_cases_on_inductive_val(env, const_name(c));
|
|
}
|
|
inline bool is_cases_on_app(environment const & env, expr const & e) {
|
|
expr const & fn = get_app_fn(e);
|
|
return is_constant(fn) && is_cases_on_recursor(env, const_name(fn));
|
|
}
|
|
/* Return the major premise of a cases_on-application.
|
|
\pre is_cases_on_app(env, c) */
|
|
expr get_cases_on_app_major(environment const & env, expr const & c, bool before_erasure = true);
|
|
unsigned get_cases_on_major_idx(environment const & env, name const & c, bool before_erasure = true);
|
|
/* Return the pair `(b, e)` such that `i in [b, e)` is argument `i` in a `c` cases_on
|
|
application is a minor premise.
|
|
\pre is_cases_on_recursor(env, c) */
|
|
pair<unsigned, unsigned> get_cases_on_minors_range(environment const & env, name const & c, bool before_erasure = true);
|
|
|
|
inline bool is_quot_primitive(environment const & env, name const & n) {
|
|
optional<constant_info> info = env.find(n);
|
|
return info && info->is_quot();
|
|
}
|
|
|
|
inline bool is_lc_unreachable_app(expr const & e) { return is_app_of(e, get_lc_unreachable_name(), 1); }
|
|
inline bool is_lc_proof_app(expr const & e) { return is_app_of(e, get_lc_proof_name(), 1); }
|
|
|
|
expr mk_lc_unreachable(type_checker::state & s, local_ctx const & lctx, expr const & type);
|
|
|
|
inline name mk_join_point_name(name const & n) { return name(n, "_join"); }
|
|
bool is_join_point_name(name const & n);
|
|
/* Pseudo "do" joinpoints are used to implement a temporary HACK. See `visit_let` method at `lcnf.cpp` */
|
|
inline name mk_pseudo_do_join_point_name(name const & n) { return name(n, "__do_jp"); }
|
|
bool is_pseudo_do_join_point_name(name const & n);
|
|
|
|
/* Create an auxiliary names for a declaration that saves the result of the compilation
|
|
after step simplification. */
|
|
inline name mk_cstage1_name(name const & decl_name) {
|
|
return name(decl_name, "_cstage1");
|
|
}
|
|
|
|
/* Create an auxiliary names for a declaration that saves the result of the compilation
|
|
after step erasure. */
|
|
inline name mk_cstage2_name(name const & decl_name) {
|
|
return name(decl_name, "_cstage2");
|
|
}
|
|
|
|
/* Set `used[i] = true` if `fvars[i]` occurs in `e` */
|
|
void mark_used_fvars(expr const & e, buffer<expr> const & fvars, buffer<bool> & used);
|
|
|
|
/* Return true if `e` contains the free variable `fvar` */
|
|
bool has_fvar(expr const & e, expr const & fvar);
|
|
|
|
expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term);
|
|
|
|
void sort_fvars(local_ctx const & lctx, buffer<expr> & fvars);
|
|
|
|
/* Return the "code" size for `e` */
|
|
unsigned get_lcnf_size(environment const & env, expr e);
|
|
|
|
// =======================================
|
|
// Auxiliary expressions for erasure.
|
|
// We use them after we have erased proofs and unnecessary type information.
|
|
// `enf` stands for "erasure normal form". It is LCNF after erasure.
|
|
|
|
/* Create a neutral expression used at ENF */
|
|
expr mk_enf_neutral();
|
|
/* Create an unreachable expression used at ENF */
|
|
expr mk_enf_unreachable();
|
|
expr mk_enf_object_type();
|
|
expr mk_enf_neutral_type();
|
|
/* "Void" type used in LLNF. Remark: the ENF types neutral and object are also used in LLNF. */
|
|
expr mk_llnf_void_type();
|
|
|
|
bool is_enf_neutral(expr const & e);
|
|
bool is_enf_unreachable(expr const & e);
|
|
bool is_enf_object_type(expr const & e);
|
|
bool is_llnf_void_type(expr const & e);
|
|
bool is_llnf_unboxed_type(expr const & type);
|
|
|
|
/* Return (some idx) iff inductive datatype `I_name` is safe, has only one constructor,
|
|
and this constructor has only one relevant field, `idx` is the field position. */
|
|
optional<unsigned> has_trivial_structure(environment const & env, name const & I_name);
|
|
|
|
expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e);
|
|
|
|
// =======================================
|
|
|
|
/* Return true if `n` is the name of a type with builtin support in the code generator. */
|
|
bool is_runtime_builtin_type(name const & n);
|
|
inline bool is_runtime_builtin_type(expr const & e) {
|
|
return is_constant(e) && is_runtime_builtin_type(const_name(e));
|
|
}
|
|
|
|
/* Return true if `n` is the name of a type that is treated as a scalar type by the code generator. */
|
|
bool is_runtime_scalar_type(name const & n);
|
|
|
|
bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type);
|
|
bool is_irrelevant_type(environment const & env, expr const & type);
|
|
|
|
void collect_used(expr const & e, name_hash_set & S);
|
|
/* Return true iff `e` contains a free variable in `s` */
|
|
bool depends_on(expr const & e, name_hash_set const & s);
|
|
|
|
bool is_stage2_decl(environment const & env, name const & n);
|
|
environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v);
|
|
environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v);
|
|
|
|
/* Return `some n` iff `e` is of the forms `expr.lit (literal.nat n)` or `uint*.of_nat (expr.lit (literal.nat n))` */
|
|
optional<nat> get_num_lit_ext(expr const & e);
|
|
inline bool is_morally_num_lit(expr const & e) { return static_cast<bool>(get_num_lit_ext(e)); }
|
|
|
|
/* Return `some n` if `c` is of the form `fix_core_n` where `n in [1, 6]`.
|
|
Remark: this function is assuming the core library contains `fix_core_1` ... `fix_core_6` definitions. */
|
|
optional<unsigned> is_fix_core(name const & c);
|
|
/* Return the `fix_core_n` constant, and `none` if `n` is not in `[1, 6]`.
|
|
Remark: this function is assuming the core library contains `fix_core_1` ... `fix_core_6` definitions.
|
|
Remark: this function assumes universe levels have already been erased. */
|
|
optional<expr> mk_enf_fix_core(unsigned n);
|
|
|
|
bool lcnf_check_let_decls(environment const & env, comp_decl const & d);
|
|
bool lcnf_check_let_decls(environment const & env, comp_decls const & ds);
|
|
|
|
// =======================================
|
|
/* Similar to `type_checker::eta_expand`, but preserves LCNF */
|
|
expr lcnf_eta_expand(type_checker::state & st, local_ctx lctx, expr e);
|
|
|
|
// =======================================
|
|
// UInt and USize helper functions
|
|
|
|
expr mk_usize_type();
|
|
bool is_usize_type(expr const & e);
|
|
optional<unsigned> is_builtin_scalar(expr const & type);
|
|
optional<unsigned> is_enum_type(environment const & env, expr const & type);
|
|
|
|
// =======================================
|
|
|
|
extern "C" uint8 lean_is_matcher(object* env, object* n);
|
|
|
|
inline bool is_matcher(environment const & env, name const & n) {
|
|
return lean_is_matcher(env.to_obj_arg(), n.to_obj_arg());
|
|
}
|
|
|
|
inline bool is_matcher_app(environment const & env, expr const & e) {
|
|
expr const & f = get_app_fn(e);
|
|
return is_constant(f) && is_matcher(env, const_name(f));
|
|
}
|
|
|
|
/*
|
|
Return true if the given expression must be in eta-expanded form during compilation.
|
|
Example: constructors, `casesOn` applications must always be in eta-expanded form.
|
|
*/
|
|
bool must_be_eta_expanded(environment const & env, expr const & e);
|
|
|
|
void initialize_compiler_util();
|
|
void finalize_compiler_util();
|
|
}
|