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);
113void IdExpr ::bind(
Scopes& s)
const { decl_ = s.find(dbg()); }
114void TypeExpr ::bind(
Scopes& s)
const { level()->bind(s); }
123 if (
tag() == Tag::L_str ||
tag() == Tag::L_c ||
tag() == Tag::L_i)
124 s.ast().error(
type()->
loc(),
"a {} shall not have a type annotation",
tag());
126 if (
tag() == Tag::L_f) s.ast().error(
loc(),
"type annotation mandatory for floating point literal");
132 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->bind(s);
134 for (
const auto& decl :
decls()) decl->bind(s);
150 for (
const auto& dom : doms()) dom->
bind(s);
152 if (tag() == Tag::K_Cn) s.ast().error(codom()->
loc(),
"a continuation shall not have a codomain");
182 for (
const auto& elem : elems()) elem->bind(s);
197 if (
auto expr = std::get_if<
Ptr<Expr>>(&index()))
201 decl_ = s.find(dbg,
true);
216 auto sym = s.ast().sym(axiom->
dbg().
sym().str() +
"."s + dbg().sym().str());
217 full_ =
Dbg(dbg().
loc(), sym);
223 annex_ = s.ast().name2annex(dbg(),
nullptr);
226 annex_->normalizer = normalizer();
227 else if (annex_->normalizer.sym() != normalizer().sym()) {
228 auto l = normalizer().loc() ? normalizer().loc() :
loc().anew_finis();
229 s.ast().error(l,
"normalizer mismatch for axiom '{}'", dbg());
230 if (
auto norm = annex_->normalizer)
231 s.ast().note(norm.loc(),
"previous normalizer '{}'", norm);
233 s.ast().note(l,
"initially no normalizer specified");
236 if (num_subs() == 0) {
239 if (
auto old = s.find(dbg(),
true)) {
240 if (
auto old_ax = old->isa<
AxiomDecl>()) {
241 if (old_ax->num_subs() == 0) {
242 s.ast().error(dbg().
loc(),
"redeclared sub-less axiom '{}' with subs", dbg());
243 s.ast().note(old_ax->dbg().loc(),
"previous location here");
247 for (
const auto& aliases : subs())
248 for (
const auto& alias : aliases) alias->bind(s,
this);
258 if (
auto id = ptrn()->isa<IdPtrn>()) annex_ = s.ast().name2annex(id->dbg(), &sub_);
262 for (
auto curr =
this; curr; curr = curr->next()) curr->bind_decl(s);
263 for (
auto curr =
this; curr; curr = curr->next()) curr->bind_body(s);
264 annex_ = s.ast().name2annex(dbg(), &sub_);
268 if (
auto t = type()) t->bind(s);
269 if (!type()->isa<InferExpr>() && body()->isa<LamExpr>())
270 s.ast().warn(type()->
loc(),
"type of recursive declaration ignored for function expression");
272 if (!body()->isa<LamExpr>() && !body()->isa<PiExpr>() && !body()->isa<ArrowExpr>() && !body()->isa<SigmaExpr>())
273 s.ast().error(body()->
loc(),
"unsupported expression for a recursive declaration");
282 if (filter() && !quiet) filter()->bind(s);
287 for (
size_t i = 0, e = num_doms(); i != e; ++i) dom(i)->
bind(s);
289 if (
auto filter = doms().back()->filter()) {
291 if (pe->tag() == Tag::K_tt && (tag() == Tag::K_lam || tag() == Tag::T_lm))
292 s.ast().warn(filter->loc(),
293 "'tt'-filter superfluous as the last curried function group of a '{}' receives a "
294 "'tt'-filter by default",
296 if (pe->tag() == Tag::K_ff && (tag() != Tag::K_lam && tag() != Tag::T_lm))
297 s.ast().warn(filter->loc(),
298 "'ff'-filter superfluous as the last curried function group of a '{}' receives a "
299 "'ff'-filter by default",
305 if (tag() == Tag::K_con || tag() == Tag::K_cn)
306 s.ast().error(codom()->
loc(),
"a continuation shall not have a codomain");
312 annex_ = s.ast().name2annex(dbg(), &sub_);
317 for (
const auto& dom : doms()) dom->
bind(s,
true);
326 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
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 quiet=false) const override
virtual void bind(Scopes &) const =0
void bind(Scopes &, bool quiet=false) const override
void bind(Scopes &, bool quiet=false) 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 quiet=false) 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 quiet=false) 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)