1/*
2Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
3Released under Apache 2.0 license as described in the file LICENSE.
4
5Author: Leonardo de Moura
6*/
7#pragma once
8#include <algorithm>
9#include <iostream>
10#include <limits>
11#include <utility>
12#include <tuple>
13#include <string>
14#include "runtime/optional.h"
15#include "runtime/thread.h"
16#include "runtime/hash.h"
17#include "runtime/buffer.h"
18#include "util/name.h"
19#include "util/nat.h"
20#include "util/kvmap.h"
21#include "util/list_fn.h"
22#include "kernel/level.h"
23#include "kernel/expr_eq_fn.h"
24
25namespace lean {
26/* Binder annotations for Pi/lambda expressions */
27enum class binder_info { Default, Implicit, StrictImplicit, InstImplicit, Rec };
28
29inline binder_info mk_binder_info() { return binder_info::Default; }
30inline binder_info mk_implicit_binder_info() { return binder_info::Implicit; }
31inline binder_info mk_strict_implicit_binder_info() { return binder_info::StrictImplicit; }
32inline binder_info mk_inst_implicit_binder_info() { return binder_info::InstImplicit; }
33inline binder_info mk_rec_info() { return binder_info::Rec; }
34
35inline bool is_default(binder_info bi) { return bi == binder_info::Default; }
36inline bool is_implicit(binder_info bi) { return bi == binder_info::Implicit; }
37inline bool is_strict_implicit(binder_info bi) { return bi == binder_info::StrictImplicit; }
38inline bool is_inst_implicit(binder_info bi) { return bi == binder_info::InstImplicit; }
39inline bool is_explicit(binder_info bi) { return !is_implicit(bi) && !is_strict_implicit(bi) && !is_inst_implicit(bi); }
40inline bool is_rec(binder_info bi) { return bi == binder_info::Rec; }
41
42/* Expression literal values */
43enum class literal_kind { Nat, String };
44class literal : public object_ref {
45 explicit literal(b_obj_arg o, bool b):object_ref(o, b) {}
46public:
47 explicit literal(char const * v);
48 explicit literal(unsigned v);
49 explicit literal(mpz const & v);
50 explicit literal(nat const & v);
51 literal():literal(0u) {}
52 literal(literal const & other):object_ref(other) {}
53 literal(literal && other):object_ref(other) {}
54 literal & operator=(literal const & other) { object_ref::operator=(other); return *this; }
55 literal & operator=(literal && other) { object_ref::operator=(other); return *this; }
56
57 static literal_kind kind(object * o) { return static_cast<literal_kind>(cnstr_tag(o)); }
58 literal_kind kind() const { return kind(raw()); }
59 string_ref const & get_string() const { lean_assert(kind() == literal_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
60 nat const & get_nat() const { lean_assert(kind() == literal_kind::Nat); return static_cast<nat const &>(cnstr_get_ref(*this, 0)); }
61 bool is_zero() const { return kind() == literal_kind::Nat && get_nat().is_zero(); }
62 friend bool operator==(literal const & a, literal const & b);
63 friend bool operator<(literal const & a, literal const & b);
64};
65inline bool operator!=(literal const & a, literal const & b) { return !(a == b); }
66
67/* =======================================
68 Expressions
69
70inductive Expr
71| bvar : Nat → Expr -- bound variables
72| fvar : Name → Expr -- free variables
73| mvar : Name → Expr -- meta variables
74| sort : Level → Expr -- Sort
75| const : Name → List Level → Expr -- constants
76| app : Expr → Expr → Expr -- application
77| lam : Name → BinderInfo → Expr → Expr → Expr -- lambda abstraction
78| forallE : Name → BinderInfo → Expr → Expr → Expr -- (dependent) arrow
79| letE : Name → Expr → Expr → Expr → Expr -- let expressions
80| lit : Literal → Expr -- literals
81| mdata : MData → Expr → Expr -- metadata
82| proj : Name → Nat → Expr → Expr -- projection
83*/
84enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj };
85class expr : public object_ref {
86 explicit expr(object_ref && o):object_ref(o) {}
87
88 friend expr mk_lit(literal const & lit);
89 friend expr mk_mdata(kvmap const & d, expr const & e);
90 friend expr mk_proj(name const & s, nat const & idx, expr const & e);
91 friend expr mk_bvar(nat const & idx);
92 friend expr mk_mvar(name const & n);
93 friend expr mk_fvar(name const & n);
94 friend expr mk_const(name const & n, levels const & ls);
95 friend expr mk_app(expr const & f, expr const & a);
96 friend expr mk_sort(level const & l);
97 friend expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info bi);
98 friend expr mk_pi(name const & n, expr const & t, expr const & e, binder_info bi);
99 friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
100public:
101 expr();
102 expr(expr const & other):object_ref(other) {}
103 expr(expr && other):object_ref(other) {}
104 explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
105 explicit expr(obj_arg o):object_ref(o) {}
106 static expr_kind kind(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
107 expr_kind kind() const { return kind(raw()); }
108
109 expr & operator=(expr const & other) { object_ref::operator=(other); return *this; }
110 expr & operator=(expr && other) { object_ref::operator=(other); return *this; }
111
112 friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
113};
114
115typedef list_ref<expr> exprs;
116typedef pair<expr, expr> expr_pair;
117
118inline optional<expr> none_expr() { return optional<expr>(); }
119inline optional<expr> some_expr(expr const & e) { return optional<expr>(e); }
120inline optional<expr> some_expr(expr && e) { return optional<expr>(std::forward<expr>(e)); }
121
122inline bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
123 return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
124}
125
126unsigned hash(expr const & e);
127bool has_expr_mvar(expr const & e);
128bool has_univ_mvar(expr const & e);
129inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
130bool has_fvar(expr const & e);
131bool has_univ_param(expr const & e);
132unsigned get_loose_bvar_range(expr const & e);
133
134struct expr_hash { unsigned operator()(expr const & e) const { return hash(e); } };
135struct expr_pair_hash {
136 unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); }
137};
138struct expr_pair_eq {
139 bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
140};
141
142// =======================================
143// Testers
144static expr_kind expr_kind_core(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
145inline bool is_bvar(expr const & e) { return e.kind() == expr_kind::BVar; }
146inline bool is_fvar_core(object * o) { return expr_kind_core(o) == expr_kind::FVar; }
147inline bool is_mvar_core(object * o) { return expr_kind_core(o) == expr_kind::MVar; }
148inline bool is_fvar(expr const & e) { return e.kind() == expr_kind::FVar; }
149inline bool is_const(expr const & e) { return e.kind() == expr_kind::Const; }
150inline bool is_mvar(expr const & e) { return e.kind() == expr_kind::MVar; }
151inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
152inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
153inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
154inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; }
155inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; }
156inline bool is_lit(expr const & e) { return e.kind() == expr_kind::Lit; }
157inline bool is_mdata(expr const & e) { return e.kind() == expr_kind::MData; }
158inline bool is_proj(expr const & e) { return e.kind() == expr_kind::Proj; }
159inline bool is_binding(expr const & e) { return is_lambda(e) || is_pi(e); }
160
161bool is_atomic(expr const & e);
162bool is_arrow(expr const & t);
163bool is_default_var_name(name const & n);
164// =======================================
165
166// =======================================
167// Constructors
168expr mk_lit(literal const & lit);
169expr mk_mdata(kvmap const & d, expr const & e);
170expr mk_proj(name const & s, nat const & idx, expr const & e);
171inline expr mk_proj(name const & s, unsigned idx, expr const & e) { return mk_proj(s, nat(idx), e); }
172expr mk_bvar(nat const & idx);
173inline expr mk_bvar(unsigned idx) { return mk_bvar(nat(idx)); }
174expr mk_fvar(name const & n);
175expr mk_const(name const & n, levels const & ls);
176inline expr mk_const(name const & n) { return mk_const(n, levels()); }
177expr mk_mvar(name const & n);
178expr mk_app(expr const & f, expr const & a);
179expr mk_app(expr const & f, unsigned num_args, expr const * args);
180expr mk_app(unsigned num_args, expr const * args);
181inline expr mk_app(std::initializer_list<expr> const & l) { return mk_app(l.size(), l.begin()); }
182inline expr mk_app(buffer<expr> const & args) { return mk_app(args.size(), args.data()); }
183inline expr mk_app(expr const & f, buffer<expr> const & args) { return mk_app(f, args.size(), args.data()); }
184expr mk_app(expr const & f, list<expr> const & args);
185inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
186inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
187inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
188expr mk_rev_app(expr const & f, unsigned num_args, expr const * args);
189expr mk_rev_app(unsigned num_args, expr const * args);
190inline expr mk_rev_app(buffer<expr> const & args) { return mk_rev_app(args.size(), args.data()); }
191inline expr mk_rev_app(expr const & f, buffer<expr> const & args) { return mk_rev_app(f, args.size(), args.data()); }
192expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info());
193expr mk_pi(name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info());
194inline expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info()) {
195 return k == expr_kind::Pi ? mk_pi(n, t, e, bi) : mk_lambda(n, t, e, bi);
196}
197expr mk_arrow(expr const & t, expr const & e);
198expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
199expr mk_sort(level const & l);
200expr mk_Prop();
201expr mk_Type();
202// =======================================
203
204// =======================================
205// Accessors
206inline literal const & lit_value(expr const & e) { lean_assert(is_lit(e)); return static_cast<literal const &>(cnstr_get_ref(e, 0)); }
207inline bool is_nat_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::Nat; }
208inline bool is_string_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::String; }
209expr lit_type(literal const & e);
210inline kvmap const & mdata_data(expr const & e) { lean_assert(is_mdata(e)); return static_cast<kvmap const &>(cnstr_get_ref(e, 0)); }
211inline expr const & mdata_expr(expr const & e) { lean_assert(is_mdata(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
212inline name const & proj_sname(expr const & e) { lean_assert(is_proj(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
213inline nat const & proj_idx(expr const & e) { lean_assert(is_proj(e)); return static_cast<nat const &>(cnstr_get_ref(e, 1)); }
214inline expr const & proj_expr(expr const & e) { lean_assert(is_proj(e)); return static_cast<expr const &>(cnstr_get_ref(e, 2)); }
215inline nat const & bvar_idx(expr const & e) { lean_assert(is_bvar(e)); return static_cast<nat const &>(cnstr_get_ref(e, 0)); }
216inline bool is_bvar(expr const & e, unsigned i) { return is_bvar(e) && bvar_idx(e) == i; }
217inline name const & fvar_name_core(object * o) { lean_assert(is_fvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
218inline name const & fvar_name(expr const & e) { lean_assert(is_fvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
219inline level const & sort_level(expr const & e) { lean_assert(is_sort(e)); return static_cast<level const &>(cnstr_get_ref(e, 0)); }
220inline name const & mvar_name_core(object * o) { lean_assert(is_mvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
221inline name const & mvar_name(expr const & e) { lean_assert(is_mvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
222inline name const & const_name(expr const & e) { lean_assert(is_const(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
223inline levels const & const_levels(expr const & e) { lean_assert(is_const(e)); return static_cast<levels const &>(cnstr_get_ref(e, 1)); }
224inline bool is_const(expr const & e, name const & n) { return is_const(e) && const_name(e) == n; }
225inline expr const & app_fn(expr const & e) { lean_assert(is_app(e)); return static_cast<expr const &>(cnstr_get_ref(e, 0)); }
226inline expr const & app_arg(expr const & e) { lean_assert(is_app(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
227inline name const & binding_name(expr const & e) { lean_assert(is_binding(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
228inline expr const & binding_domain(expr const & e) { lean_assert(is_binding(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
229inline expr const & binding_body(expr const & e) { lean_assert(is_binding(e)); return static_cast<expr const &>(cnstr_get_ref(e, 2)); }
230binder_info binding_info(expr const & e);
231inline name const & let_name(expr const & e) { lean_assert(is_let(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
232inline expr const & let_type(expr const & e) { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
233inline expr const & let_value(expr const & e) { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 2)); }
234inline expr const & let_body(expr const & e) { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 3)); }
235inline bool is_shared(expr const & e) { return !is_exclusive(e.raw()); }
236//
237
238// =======================================
239// Update
240expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
241expr update_binding(expr const & e, expr const & new_domain, expr const & new_body);
242expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info bi);
243expr update_sort(expr const & e, level const & new_level);
244expr update_const(expr const & e, levels const & new_levels);
245expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
246expr update_mdata(expr const & e, expr const & new_e);
247expr update_proj(expr const & e, expr const & new_e);
248// =======================================
249
250
251/** \brief Given \c e of the form <tt>(...(f a1) ... an)</tt>, store a1 ... an in args.
252 If \c e is not an application, then nothing is stored in args.
253
254 It returns the f. */
255expr const & get_app_args(expr const & e, buffer<expr> & args);
256/** \brief Similar to \c get_app_args, but stores at most num args.
257 Examples:
258 1) get_app_args_at_most(f a b c, 2, args);
259 stores {b, c} in args and returns (f a)
260
261 2) get_app_args_at_most(f a b c, 4, args);
262 stores {a, b, c} in args and returns f */
263expr const & get_app_args_at_most(expr const & e, unsigned num, buffer<expr> & args);
264
265/** \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args.
266 If e is of the form <tt>(...(f a1) ... an)</tt>, then the procedure stores [an, ..., a1] in \c args. */
267expr const & get_app_rev_args(expr const & e, buffer<expr> & args);
268/** \brief Given \c e of the form <tt>(...(f a_1) ... a_n)</tt>, return \c f. If \c e is not an application, then return \c e. */
269expr const & get_app_fn(expr const & e);
270/** \brief Given \c e of the form <tt>(...(f a_1) ... a_n)</tt>, return \c n. If \c e is not an application, then return 0. */
271unsigned get_app_num_args(expr const & e);
272
273/** \brief Return true iff \c e is a metavariable or an application of a metavariable */
274inline bool is_mvar_app(expr const & e) { return is_mvar(get_app_fn(e)); }
275
276expr consume_type_annotations(expr const & e);
277
278// =======================================
279// Loose bound variable management
280
281/** \brief Return true iff the given expression has loose bound variables. */
282inline bool has_loose_bvars(expr const & e) { return get_loose_bvar_range(e) > 0; }
283
284/** \brief Return true iff \c e contains the loose bound variable <tt>(var i)</tt>. */
285bool has_loose_bvar(expr const & e, unsigned i);
286
287/** \brief Lower the loose bound variables >= s in \c e by \c d. That is, a loose bound variable <tt>(var i)</tt> s.t.
288 <tt>i >= s</tt> is mapped into <tt>(var i-d)</tt>.
289
290 \pre s >= d */
291expr lower_loose_bvars(expr const & e, unsigned s, unsigned d);
292expr lower_loose_bvars(expr const & e, unsigned d);
293
294/** \brief Lift loose bound variables >= s in \c e by d. */
295expr lift_loose_bvars(expr const & e, unsigned s, unsigned d);
296expr lift_loose_bvars(expr const & e, unsigned d);
297// =======================================
298
299
300// =======================================
301// Implicit argument inference
302/**
303 \brief Given \c t of the form <tt>Pi (x_1 : A_1) ... (x_k : A_k), B</tt>,
304 mark the first \c num_params as implicit if they are not already marked, and
305 they occur in the remaining arguments. If \c strict is false, then we
306 also mark it implicit if it occurs in \c B.
307*/
308expr infer_implicit(expr const & t, unsigned num_params, bool strict);
309expr infer_implicit(expr const & t, bool strict);
310// =======================================
311
312// =======================================
313// Low level (raw) printing
314std::ostream & operator<<(std::ostream & out, expr const & e);
315// =======================================
316
317void initialize_expr();
318void finalize_expr();
319
320/* ================= LEGACY ============== */
321inline bool has_expr_metavar(expr const & e) { return has_expr_mvar(e); }
322inline bool has_univ_metavar(expr const & e) { return has_univ_mvar(e); }
323inline bool has_metavar(expr const & e) { return has_mvar(e); }
324inline bool has_param_univ(expr const & e) { return has_univ_param(e); }
325inline bool is_var(expr const & e) { return is_bvar(e); }
326inline bool is_var(expr const & e, unsigned idx) { return is_bvar(e, idx); }
327inline bool is_metavar(expr const & e) { return is_mvar(e); }
328inline bool is_metavar_app(expr const & e) { return is_mvar_app(e); }
329inline expr mk_metavar(name const & n) { return mk_mvar(n); }
330inline expr mk_constant(name const & n, levels const & ls) { return mk_const(n, ls); }
331inline expr mk_constant(name const & n) { return mk_constant(n, levels()); }
332inline bool is_constant(expr const & e) { return is_const(e); }
333inline expr update_constant(expr const & e, levels const & new_levels) { return update_const(e, new_levels); }
334/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types.
335 It also returns the meta-variable application found in \c e. */
336optional<expr> has_expr_metavar_strict(expr const & e);
337inline bool is_constant(expr const & e, name const & n) { return is_const(e, n); }
338}
339