1/*
2Copyright (c) 2018 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 "util/name_generator.h"
9#include "util/rb_map.h"
10#include "util/name_map.h"
11#include "kernel/expr.h"
12
13namespace lean {
14/*
15inductive LocalDecl
16| cdecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo)
17| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
18*/
19class local_decl : public object_ref {
20 friend class local_ctx;
21 friend class local_context;
22 friend void initialize_local_ctx();
23 local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v);
24 local_decl(local_decl const & d, expr const & t, expr const & v);
25 local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi);
26 local_decl(local_decl const & d, expr const & t);
27public:
28 local_decl();
29 local_decl(local_decl const & other):object_ref(other) {}
30 local_decl(local_decl && other):object_ref(other) {}
31 local_decl(obj_arg o):object_ref(o) {}
32 local_decl(b_obj_arg o, bool):object_ref(o, true) {}
33 local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
34 local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; }
35 friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
36 unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
37 name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
38 name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 2)); }
39 expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 3)); }
40 optional<expr> get_value() const {
41 if (cnstr_tag(raw()) == 0) return none_expr();
42 return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 4)));
43 }
44 binder_info get_info() const;
45 expr mk_ref() const;
46};
47
48/* Plain local context object used by the kernel type checker. */
49class local_ctx : public object_ref {
50protected:
51 template<bool is_lambda> expr mk_binding(unsigned num, expr const * fvars, expr const & b, bool remove_dead_let = false) const;
52public:
53 local_ctx();
54 explicit local_ctx(obj_arg o):object_ref(o) {}
55 local_ctx(b_obj_arg o, bool):object_ref(o, true) {}
56 local_ctx(local_ctx const & other):object_ref(other) {}
57 local_ctx(local_ctx && other):object_ref(other) {}
58 local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; }
59 local_ctx & operator=(local_ctx && other) { object_ref::operator=(other); return *this; }
60
61 bool empty() const;
62
63 /* Low level `mk_local_decl` */
64 local_decl mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi);
65 /* Low level `mk_local_decl` */
66 local_decl mk_local_decl(name const & n, name const & un, expr const & type, expr const & value);
67
68 expr mk_local_decl(name_generator & g, name const & un, expr const & type, binder_info bi = mk_binder_info()) {
69 return mk_local_decl(g.next(), un, type, bi).mk_ref();
70 }
71
72 expr mk_local_decl(name_generator & g, name const & un, expr const & type, expr const & value) {
73 return mk_local_decl(g.next(), un, type, value).mk_ref();
74 }
75
76 /** \brief Return the local declarations for the given reference. */
77 optional<local_decl> find_local_decl(name const & n) const;
78 optional<local_decl> find_local_decl(expr const & e) const { return find_local_decl(fvar_name(e)); }
79
80 local_decl get_local_decl(name const & n) const;
81 local_decl get_local_decl(expr const & e) const { return get_local_decl(fvar_name(e)); }
82
83 /* \brief Return type of the given free variable.
84 \pre is_fvar(e) */
85 expr get_type(expr const & e) const { return get_local_decl(e).get_type(); }
86
87 /** Return the free variable associated with the given name.
88 \pre get_local_decl(n) */
89 expr get_local(name const & n) const;
90
91 /** \brief Remove the given local decl. */
92 void clear(local_decl const & d);
93
94 expr mk_lambda(unsigned num, expr const * fvars, expr const & e, bool remove_dead_let = false) const;
95 expr mk_pi(unsigned num, expr const * fvars, expr const & e, bool remove_dead_let = false) const;
96 expr mk_lambda(buffer<expr> const & fvars, expr const & e, bool remove_dead_let = false) const { return mk_lambda(fvars.size(), fvars.data(), e, remove_dead_let); }
97 expr mk_pi(buffer<expr> const & fvars, expr const & e, bool remove_dead_let = false) const { return mk_pi(fvars.size(), fvars.data(), e, remove_dead_let); }
98 expr mk_lambda(expr const & fvar, expr const & e) { return mk_lambda(1, &fvar, e); }
99 expr mk_pi(expr const & fvar, expr const & e) { return mk_pi(1, &fvar, e); }
100 expr mk_lambda(std::initializer_list<expr> const & fvars, expr const & e) { return mk_lambda(fvars.size(), fvars.begin(), e); }
101 expr mk_pi(std::initializer_list<expr> const & fvars, expr const & e) { return mk_pi(fvars.size(), fvars.begin(), e); }
102};
103
104void initialize_local_ctx();
105void finalize_local_ctx();
106}
107