1/*
2Copyright (c) 2013 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 <iostream>
9#include <algorithm>
10#include <utility>
11#include "runtime/optional.h"
12#include "runtime/list_ref.h"
13#include "util/name.h"
14#include "util/options.h"
15
16namespace lean {
17class environment;
18struct level_cell;
19/**
20inductive level
21| zero : level
22| succ : level → level
23| max : level → level → level
24| imax : level → level → level
25| param : name → level
26| mvar : name → level
27
28We level.imax to handle Pi-types.
29*/
30enum class level_kind { Zero, Succ, Max, IMax, Param, MVar };
31
32/** \brief Universe level. */
33class level : public object_ref {
34 friend level mk_succ(level const & l);
35 friend level mk_max_core(level const & l1, level const & l2);
36 friend level mk_imax_core(level const & l1, level const & l2);
37 friend level mk_univ_param(name const & n);
38 friend level mk_univ_mvar(name const & n);
39 explicit level(object_ref && o):object_ref(o) {}
40public:
41 /** \brief Universe zero */
42 level();
43 explicit level(obj_arg o):object_ref(o) {}
44 explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
45 level(level const & other):object_ref(other) {}
46 level(level && other):object_ref(other) {}
47 level_kind kind() const {
48 return lean_is_scalar(raw()) ? level_kind::Zero : static_cast<level_kind>(lean_ptr_tag(raw()));
49 }
50 unsigned hash() const;
51
52 level & operator=(level const & other) { object_ref::operator=(other); return *this; }
53 level & operator=(level && other) { object_ref::operator=(other); return *this; }
54
55 friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }
56
57 bool is_zero() const { return kind() == level_kind::Zero; }
58 bool is_succ() const { return kind() == level_kind::Succ; }
59 bool is_max() const { return kind() == level_kind::Max; }
60 bool is_imax() const { return kind() == level_kind::IMax; }
61 bool is_param() const { return kind() == level_kind::Param; }
62 bool is_mvar() const { return kind() == level_kind::MVar; }
63
64 friend inline level const & max_lhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_get_ref(l, 0)); }
65 friend inline level const & max_rhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_get_ref(l, 1)); }
66 friend inline level const & imax_lhs(level const & l) { lean_assert(l.is_imax()); return static_cast<level const &>(cnstr_get_ref(l, 0)); }
67 friend inline level const & imax_rhs(level const & l) { lean_assert(l.is_imax()); return static_cast<level const &>(cnstr_get_ref(l, 1)); }
68 friend inline level const & level_lhs(level const & l) { lean_assert(l.is_max() || l.is_imax()); return static_cast<level const &>(cnstr_get_ref(l, 0)); }
69 friend inline level const & level_rhs(level const & l) { lean_assert(l.is_max() || l.is_imax()); return static_cast<level const &>(cnstr_get_ref(l, 1)); }
70 friend inline level const & succ_of(level const & l) { lean_assert(l.is_succ()); return static_cast<level const &>(cnstr_get_ref(l, 0)); }
71 friend inline name const & param_id(level const & l) { lean_assert(l.is_param()); return static_cast<name const &>(cnstr_get_ref(l, 0)); }
72 friend inline name const & mvar_id(level const & l) { lean_assert(l.is_mvar()); return static_cast<name const &>(cnstr_get_ref(l, 0)); }
73 friend inline name const & level_id(level const & l) { lean_assert(l.is_param() || l.is_mvar()); return static_cast<name const &>(cnstr_get_ref(l, 0)); }
74};
75
76typedef list_ref<level> levels;
77typedef pair<level, level> level_pair;
78
79bool operator==(level const & l1, level const & l2);
80inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
81
82struct level_hash { unsigned operator()(level const & n) const { return n.hash(); } };
83struct level_eq { bool operator()(level const & n1, level const & n2) const { return n1 == n2; } };
84
85inline optional<level> none_level() { return optional<level>(); }
86inline optional<level> some_level(level const & e) { return optional<level>(e); }
87inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }
88
89level const & mk_level_zero();
90level const & mk_level_one();
91level mk_max_core(level const & l1, level const & l2);
92level mk_imax_core(level const & l1, level const & l2);
93level mk_max(level const & l1, level const & l2);
94level mk_imax(level const & l1, level const & l2);
95level mk_succ(level const & l);
96level mk_univ_param(name const & n);
97level mk_univ_mvar(name const & n);
98
99/** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
100pair<level, unsigned> to_offset(level l);
101
102inline unsigned hash(level const & l) { return l.hash(); }
103inline level_kind kind(level const & l) { return l.kind(); }
104inline bool is_zero(level const & l) { return l.is_zero(); }
105inline bool is_param(level const & l) { return l.is_param(); }
106inline bool is_mvar(level const & l) { return l.is_mvar(); }
107inline bool is_succ(level const & l) { return l.is_succ(); }
108inline bool is_max(level const & l) { return l.is_max(); }
109inline bool is_imax(level const & l) { return l.is_imax(); }
110bool is_one(level const & l);
111
112unsigned get_depth(level const & l);
113
114/** \brief Return true iff \c l is an explicit level.
115 We say a level l is explicit iff
116 1) l is zero OR
117 2) l = succ(l') and l' is explicit */
118bool is_explicit(level const & l);
119/** \brief Convert an explicit universe into a unsigned integer.
120 \pre is_explicit(l) */
121unsigned to_explicit(level const & l);
122/** \brief Return true iff \c l contains placeholder (aka meta parameters). */
123bool has_mvar(level const & l);
124/** \brief Return true iff \c l contains parameters */
125bool has_param(level const & l);
126
127/** \brief Return a new level expression based on <tt>l == succ(arg)</tt>, where \c arg is replaced with
128 \c new_arg.
129 \pre is_succ(l) */
130level update_succ(level const & l, level const & new_arg);
131/** \brief Return a new level expression based on <tt>l == max(lhs, rhs)</tt>, where \c lhs is replaced with
132 \c new_lhs and \c rhs is replaced with \c new_rhs.
133
134 \pre is_max(l) || is_imax(l) */
135level update_max(level const & l, level const & new_lhs, level const & new_rhs);
136
137/** \brief Return true if lhs and rhs denote the same level.
138 The check is done by normalization. */
139bool is_equivalent(level const & lhs, level const & rhs);
140/** \brief Return the given level expression normal form */
141level normalize(level const & l);
142
143/** \brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
144 in \c l1 and \l2, we have that the universe level l1[A] is bigger or equal to l2[A].
145
146 \remark This function assumes l1 and l2 are normalized */
147bool is_geq_core(level l1, level l2);
148
149bool is_geq(level const & l1, level const & l2);
150
151bool levels_has_mvar(object * ls);
152bool has_mvar(levels const & ls);
153bool levels_has_param(object * ls);
154bool has_param(levels const & ls);
155
156/** \brief An arbitrary (monotonic) total order on universe level terms. */
157bool is_lt(level const & l1, level const & l2, bool use_hash);
158bool is_lt(levels const & as, levels const & bs, bool use_hash);
159struct level_quick_cmp { int operator()(level const & l1, level const & l2) const { return is_lt(l1, l2, true) ? -1 : (l1 == l2 ? 0 : 1); } };
160
161/** \brief Functional for applying <tt>F</tt> to each level expressions. */
162class for_each_level_fn {
163 std::function<bool(level const &)> m_f; // NOLINT
164 void apply(level const & l);
165public:
166 template<typename F> for_each_level_fn(F const & f):m_f(f) {}
167 void operator()(level const & l) { return apply(l); }
168};
169template<typename F> void for_each(level const & l, F const & f) { return for_each_level_fn(f)(l); }
170
171/** \brief Functional for applying <tt>F</tt> to the level expressions. */
172class replace_level_fn {
173 std::function<optional<level>(level const &)> m_f;
174 level apply(level const & l);
175public:
176 template<typename F> replace_level_fn(F const & f):m_f(f) {}
177 level operator()(level const & l) { return apply(l); }
178};
179template<typename F> level replace(level const & l, F const & f) { return replace_level_fn(f)(l); }
180
181/** \brief Return true if \c u occurs in \c l */
182bool occurs(level const & u, level const & l);
183
184/** \brief If \c l contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
185optional<name> get_undef_param(level const & l, names const & lparams);
186
187/** \brief Instantiate the universe level parameters \c ps occurring in \c l with the levels \c ls.
188 \pre length(ps) == length(ls) */
189level instantiate(level const & l, names const & ps, levels const & ls);
190
191/** \brief Printer for debugging purposes */
192std::ostream & operator<<(std::ostream & out, level const & l);
193
194/** \brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
195 in \c l, l[A] != zero. */
196bool is_not_zero(level const & l);
197
198/** \brief Convert a list of universe level parameter names into a list of levels. */
199levels lparams_to_levels(names const & ps);
200
201void initialize_level();
202void finalize_level();
203}
204void print(lean::level const & l);
205