3using namespace std::literals;
14 std::ostream&
stream(
Tab&, std::ostream& os)
const override {
return os <<
"<dummy>"; }
19 using Scope = fe::SymMap<std::pair<Loc, const Decl*>>;
32 void push() { scopes_.emplace_back(); }
35 assert(!scopes_.empty());
40 if (dbg.is_anon())
return nullptr;
42 for (
auto& scope : scopes_ | std::ranges::views::reverse)
43 if (
auto i = scope.find(dbg.sym()); i != scope.end())
return i->second.second;
46 ast().
error(dbg.loc(),
"'{}' not found", dbg.sym());
52 void bind(
Dbg dbg,
const Decl* decl,
bool rebind =
false,
bool quiet =
false) {
53 if (dbg.is_anon())
return;
56 top()[dbg.sym()] = std::pair(dbg.loc(), decl);
57 }
else if (
auto [i, ins] =
top().emplace(dbg.sym(), std::pair(dbg.loc(), decl)); !ins) {
58 auto [prev_loc, prev_decl] = i->second;
59 if (!quiet && !prev_decl->isa<
DummyDecl>()) {
60 ast().
error(dbg.loc(),
"redeclaration of '{}'", dbg);
61 ast().
note(prev_loc,
"previous declaration here");
69 std::deque<Scope> scopes_;
70 absl::flat_hash_map<plugin_t, tag_t> plugin2tag_;
84 for (
const auto&
import :
imports())
import->bind(s);
85 for (
const auto& decl :
decls()) decl->bind(s);
99 s.bind(
dbg(),
this, rebind, quiet);
104 s.bind(
dbg(),
this, rebind, quiet);
116void IdExpr ::bind(
Scopes& s)
const { decl_ = s.find(dbg()); }
117void TypeExpr ::bind(
Scopes& s)
const { level()->bind(s); }
126 if (
tag() == Tag::L_str ||
tag() == Tag::L_c ||
tag() == Tag::L_i)
127 s.ast().error(
type()->
loc(),
"a {} shall not have a type annotation",
tag());
129 if (
tag() == Tag::L_f) s.ast().error(
loc(),
"type annotation mandatory for floating point literal");
135 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->bind(s);
137 for (
const auto& decl :
decls()) decl->bind(s);
153 for (
const auto& dom : doms()) dom->
bind(s);
155 if (tag() == Tag::K_Cn) s.ast().error(codom()->
loc(),
"a continuation shall not have a codomain");
174 ptrn()->bind(s,
true,
false);
180 ptrn()->bind(s,
false,
false);
185 for (
const auto& elem : elems()) elem->bind(s);
190 shape()->bind(s,
false,
false);
200 if (
auto expr = std::get_if<
Ptr<Expr>>(&index()))
204 decl_ = s.find(dbg,
true);
219 auto sym = s.ast().sym(axiom->
dbg().
sym().str() +
"."s + dbg().sym().str());
220 full_ =
Dbg(dbg().
loc(), sym);
226 annex_ = s.ast().name2annex(dbg(),
nullptr);
229 annex_->normalizer = normalizer();
230 else if (annex_->normalizer.sym() != normalizer().sym()) {
231 auto l = normalizer().loc() ? normalizer().loc() :
loc().anew_finis();
232 s.ast().error(l,
"normalizer mismatch for axiom '{}'", dbg());
233 if (
auto norm = annex_->normalizer)
234 s.ast().note(norm.loc(),
"previous normalizer '{}'", norm);
236 s.ast().note(l,
"initially no normalizer specified");
239 if (num_subs() == 0) {
242 if (
auto old = s.find(dbg(),
true)) {
243 if (
auto old_ax = old->isa<
AxiomDecl>()) {
244 if (old_ax->num_subs() == 0) {
245 s.ast().error(dbg().
loc(),
"redeclared sub-less axiom '{}' with subs", dbg());
246 s.ast().note(old_ax->dbg().loc(),
"previous location here");
250 for (
const auto& aliases : subs())
251 for (
const auto& alias : aliases) alias->bind(s,
this);
259 ptrn()->bind(s,
true,
false);
261 if (
auto id = ptrn()->isa<IdPtrn>()) annex_ = s.ast().name2annex(id->dbg(), &sub_);
265 for (
auto curr =
this; curr; curr = curr->next()) curr->bind_decl(s);
266 for (
auto curr =
this; curr; curr = curr->next()) curr->bind_body(s);
267 annex_ = s.ast().name2annex(dbg(), &sub_);
271 if (
auto t = type()) t->bind(s);
272 if (!type()->isa<InferExpr>() && body()->isa<LamExpr>())
273 s.ast().warn(type()->
loc(),
"type of recursive declaration ignored for function expression");
275 if (!body()->isa<LamExpr>() && !body()->isa<PiExpr>() && !body()->isa<ArrowExpr>() && !body()->isa<SigmaExpr>())
276 s.ast().error(body()->
loc(),
"unsupported expression for a recursive declaration");
285 if (filter() && !quiet) filter()->bind(s);
290 for (
size_t i = 0, e = num_doms(); i != e; ++i) dom(i)->
bind(s);
292 if (
auto filter = doms().back()->filter()) {
294 if (pe->tag() == Tag::K_tt && (tag() == Tag::K_lam || tag() == Tag::T_lm))
295 s.ast().warn(filter->loc(),
296 "'tt'-filter superfluous as the last curried function group of a '{}' receives a "
297 "'tt'-filter by default",
299 if (pe->tag() == Tag::K_ff && (tag() != Tag::K_lam && tag() != Tag::T_lm))
300 s.ast().warn(filter->loc(),
301 "'ff'-filter superfluous as the last curried function group of a '{}' receives a "
302 "'ff'-filter by default",
308 if (tag() == Tag::K_con || tag() == Tag::K_cn)
309 s.ast().error(codom()->
loc(),
"a continuation shall not have a codomain");
315 annex_ = s.ast().name2annex(dbg(), &sub_);
320 for (
const auto& dom : doms()) dom->
bind(s,
true);
327 dom()->
bind(s,
false,
false);
329 if (codom()) codom()->
bind(s);
Some "global" variables needed all over the place.
Keeps track of indentation level.
Error & note(Loc loc, const char *fmt, Args &&... args) const
const Ptrn * ptrn() const
void bind(Scopes &, bool rebind, bool quiet) const override
void bind(Scopes &) const override
void bind(Scopes &) const override
void bind(Scopes &) const override
void bind(Scopes &, const AxiomDecl *) const
void bind(Scopes &) const override
void bind(Scopes &) const override
const Expr * expr() const
const auto & decls() const
void bind(Scopes &) const override
std::ostream & stream(Tab &, std::ostream &os) const override
void bind(Scopes &, bool rebind, bool quiet) const override
virtual void bind(Scopes &) const =0
void bind(Scopes &, bool rebind, bool quiet) const override
void bind(Scopes &, bool rebind, bool quiet) const override
const Expr * type() const
void bind(Scopes &) const
const Module * module() const
void bind(Scopes &) const override
void bind(Scopes &scopes, bool quiet=false) const override
void bind_body(Scopes &) const override
void bind_decl(Scopes &) const override
void bind(Scopes &) const override
void bind(Scopes &) const override
const Expr * type() const
void bind(Scopes &) const override
const auto & decls() const
const auto & implicit_imports() const
const auto & imports() const
virtual void bind(Scopes &scopes, bool quiet=false) const
const IdPtrn * ret() const
const Ptrn * ptrn() const
void bind(Scopes &) const override
void bind(Scopes &) const override
virtual void bind(Scopes &, bool rebind, bool quiet) const =0
virtual void bind_body(Scopes &) const
virtual void bind_decl(Scopes &) const
void bind(Scopes &) const override
void bind(Scopes &) const override
const Decl * dummy() const
const Decl * find(Dbg dbg, bool quiet=false)
void bind(Dbg dbg, const Decl *decl, bool rebind=false, bool quiet=false)
fe::SymMap< std::pair< Loc, const Decl * > > Scope
void bind(Scopes &) const override
void bind(Scopes &) const override
void bind(Scopes &, bool rebind, bool quiet) const override
const Ptrn * ptrn(size_t i) const
const auto & ptrns() const
fe::Arena::Ptr< const T > Ptr
constexpr decltype(auto) get(mim::Span< T, N > span)