16 if (
s->isa<Nat>())
return true;
17 if (
auto arr =
s->isa<Arr>())
return arr->body()->isa<
Nat>();
18 if (
auto sig =
s->isa_imm<Sigma>())
return std::ranges::all_of(sig->ops(), [](Ref
op) {
return op->isa<
Nat>(); });
23const Def* infer_sigma(World& world,
Defs ops) {
25 for (
size_t i = 0, e = ops.size(); i !=
e; ++i) elems[i] = ops[i]->type();
26 return world.sigma(elems);
34#if (!defined(_MSC_VER) && defined(NDEBUG))
35bool World::Lock::guard_ =
false;
41 data_.univ = insert<Univ>(0, *
this);
46 data_.Bot = insert<thorin::Bot>(0,
type());
47 data_.sigma = insert<Sigma>(0,
type(),
Defs{})->as<Sigma>();
48 data_.tuple = insert<Tuple>(0,
sigma(),
Defs{})->as<Tuple>();
49 data_.type_nat = insert<thorin::Nat>(0, *
this);
51 data_.top_nat = insert<Top>(0,
type_nat());
56 data_.lit_bool[0] =
lit_idx(2, 0_u64);
57 data_.lit_bool[1] =
lit_idx(2, 1_u64);
66 for (
auto def : move_.defs) def->~Def();
82 if (
driver().is_loaded(plugin)) {
94 error(level,
"argument `{}` to `.Type` must be of type `.Univ` but is of type `{}`", level, level->
type());
96 return unify<Type>(1, level)->as<
Type>();
101 error(op,
"operand '{}' of a universe increment must be of type `.Univ` but is of type `{}`", op, op->
type());
104 return unify<UInc>(1, op, offset);
111 if (
auto um = op->isa<
UMax>())
112 ops.insert(ops.end(), um->ops().begin(), um->ops().end());
114 ops.emplace_back(op);
117 for (
auto& op : ops) {
125 error(r,
"operand '{}' must be a .Type of some level", r);
128 if (!r->type()->isa<
Univ>())
129 error(r,
"operand '{}' of a universe max must be of type '.Univ' but is of type '{}'", r, r->type());
134 lvl = std::max(lvl, *l);
143 std::ranges::sort(ops, [](
auto op1,
auto op2) {
return op1->gid() < op2->gid(); });
144 ops.erase(std::unique(ops.begin(), ops.end()), ops.end());
145 ldef = unify<UMax>(ops.size(), *
this, ops);
158 if (
auto var = mut->var_)
return var;
159 return mut->var_ = unify<Var>(1,
type, mut);
163 while (
auto pi = callee->
type()->isa<
Pi>()) {
166 auto a =
app(callee, infer);
170 if (
auto app = callee->isa<
App>();
app &&
app->curry() == 1) {
173 callee = apps.front()->callee();
180 return app(callee, arg);
185 auto pi = callee->
type()->isa<
Pi>();
187 if (!
pi)
error(callee,
"called expression '{}' : '{}' is not of function type", callee, callee->
type());
189 error(arg,
"cannot pass argument \n'{}' of type \n'{}' to \n'{}' of domain \n'{}'", arg, arg->
type(), callee,
192 if (
auto imm = callee->
isa_imm<
Lam>())
return imm->body();
196 DLOG(
"partial evaluate: {} ({})",
lam, arg);
202 return raw_app<true>(
type, callee, arg);
208 curry = curry == 0 ? trip : curry;
211 if (
auto normalize =
axiom->
normalizer(); Normalize && normalize && curry == 0)
212 return normalize(
type, callee, arg);
215 return unify<App>(2,
axiom, curry, trip,
type, callee, arg);
220 if (n == 0)
return sigma();
221 if (n == 1)
return ops[0];
223 return unify<Sigma>(ops.size(), umax<Sort::Type>(ops), ops);
227 if (ops.size() == 1)
return ops[0];
229 auto sigma = infer_sigma(*
this, ops);
232 error(t,
"cannot assign tuple '{}' of type '{}' to incompatible tuple type '{}'", t, t->type(),
sigma);
242 if (n == 0)
return tuple();
243 if (n == 1)
return ops[0];
250 if (
auto extract = ops[0]->isa<Extract>()) {
253 for (
size_t i = 0; i != n && eta; ++i) {
254 if (
auto extract = ops[i]->isa<Extract>()) {
256 if (eta &=
u64(i) == *index) {
257 eta &=
extract->tuple() == tup;
269 return unify<Tuple>(ops.size(),
type, ops);
274 std::ranges::transform(
sym, std::back_inserter(defs), [
this](
auto c) {
return lit_i8(c); });
280 if (index->isa<
Tuple>()) {
282 auto idx =
DefVec(n, [&](
size_t i) {
return index->
op(i); });
283 auto ops =
DefVec(n, [&](
size_t i) {
return d->proj(n,
Lit::as(idx[i])); });
285 }
else if (index->isa<
Pack>()) {
286 auto ops =
DefVec(index->
as_lit_arity(), [&](
size_t) { return extract(d, index->ops().back()); });
293 if (
auto l =
Lit::isa(size); l && *l == 1) {
294 if (
auto l =
Lit::isa(index); !l || *l != 0)
WLOG(
"unknown Idx of size 1: {}", index);
302 if (
auto pack = d->isa_imm<
Pack>())
return pack->body();
305 error(index,
"index '{}' does not fit within arity '{}'", index,
type->
arity());
323 return unify<Extract>(2, t, d, index);
326 return unify<Extract>(2,
sigma->
op(*i), d, index);
337 return unify<Extract>(2, elem_t, d, index);
341 auto type = d->unfold_type();
346 error(index,
"index '{}' does not fit within arity '{}'", index,
type->
arity());
349 auto target_type =
type->
proj(*lidx);
351 error(val,
"value of type {} is not assignable to type {}", val->
type(), target_type);
354 if (
auto l =
Lit::isa(size); l && *l == 1)
355 return tuple(d, {val});
358 if (
auto t = d->isa<
Tuple>(); t && lidx)
return t->refine(*lidx, val);
364 new_ops[*lidx] = val;
374 return unify<Insert>(3, d, index, val);
379 if (!is_shape(shape->type()))
error(shape,
"expected shape but got '{}' of type '{}'", shape, shape->type());
382 if (*a == 0)
return sigma();
383 if (*a == 1)
return body;
387 if (
auto ex = shape->isa<
Extract>()) {
388 if (
auto tup = ex->tuple()->isa<
Tuple>()) {
389 auto arrs =
DefVec(tup->num_ops(), [&](
size_t i) { return arr(tup->op(i), body); });
398 if (
auto p = shape->isa<
Pack>()) {
399 if (
auto s =
Lit::isa(p->shape()))
return arr(*s,
arr(
pack(*s - 1, p->body()), body));
402 return unify<Arr>(2, body->
unfold_type(), shape, body);
406 if (!is_shape(shape->type()))
error(shape,
"expected shape but got '{}' of type '{}'", shape, shape->type());
409 if (*a == 0)
return tuple();
410 if (*a == 1)
return body;
417 if (
auto p = shape->isa<
Pack>()) {
422 return unify<Pack>(1,
type, body);
426 if (shape.empty())
return body;
427 return arr(shape.rsubspan(1),
arr(shape.back(), body));
431 if (shape.empty())
return body;
432 return pack(shape.rsubspan(1),
pack(shape.back(), body));
438 if (*s != 0 && val >= *s)
error(
type,
"index '{}' does not fit within arity '{}'", size, val);
439 }
else if (val != 0) {
440 error(
type,
"cannot create literal '{}' of '.Idx {}' as size is unknown", val, size);
444 return unify<Lit>(0,
type, val);
455 return unify<TExt<Up>>(0,
type);
459 auto kind = umax<Sort::Type>(ops);
462 if (std::ranges::any_of(ops, [&](
Ref op) {
return Up ? bool(op->isa<
Top>()) : bool(op->isa<
thorin::Bot>()); }))
463 return ext<Up>(kind);
466 DefVec cpy(ops.begin(), ops.end());
467 auto [_, end] = std::ranges::copy_if(ops, cpy.begin(), [&](
Ref op) { return !op->isa<Ext>(); });
471 end = std::unique(cpy.begin(), end);
472 cpy.resize(std::distance(cpy.begin(), end));
474 if (cpy.size() == 0)
return ext<!Up>(kind);
475 if (cpy.size() == 1)
return cpy[0];
479 return unify<TBound<Up>>(cpy.size(), kind, cpy);
484 auto types =
DefVec(ops.size(), [&](
size_t i) { return ops[i]->type(); });
485 return unify<Ac>(ops.size(),
meet(types), ops);
488 assert(ops.size() == 1);
495 if (
type->isa<
Join>())
return unify<Vel>(1,
type, value);
503 auto c_pi = clash->
type()->isa<
Pi>();
506 assert(m_pi && c_pi);
507 auto a = m_pi->dom()->isa_lit_arity();
508 assert_unused(a && *a == 2);
511 auto codom =
join({m_pi->codom(), c_pi->
codom()});
512 return unify<Test>(4,
pi(c_pi->
dom(), codom), value, probe,
match, clash);
518 auto name = symbol.str();
520 auto pos =
name.find(suffix);
521 if (pos != std::string::npos) {
522 auto num =
name.substr(pos + suffix.size());
527 num = std::to_string(std::stoi(num) + 1);
528 name =
name.substr(0, pos + suffix.size()) +
"_" + num;
541#ifdef THORIN_ENABLE_CHECKS
546 auto i = std::ranges::find_if(move_.defs, [=](
auto def) { return def->gid() == gid; });
547 if (i == move_.defs.end())
return nullptr;
552 for (
auto [_, mut] :
externals()) assert(mut->is_closed() && mut->is_set());
562template Ref World::umax<Sort::Term>(
Defs);
563template Ref World::umax<Sort::Type>(
Defs);
564template Ref World::umax<Sort::Kind>(
Defs);
565template Ref World::umax<Sort::Univ>(
Defs);
566template Ref World::ext<true>(
Ref);
567template Ref World::ext<false>(
Ref);
568template Ref World::bound<true>(
Defs);
569template Ref World::bound<false>(
Defs);
A (possibly paramterized) Array.
NormalizeFn normalizer() const
static constexpr u8 Trip_End
static std::tuple< const Axiom *, u8, u8 > get(const Def *def)
Yields currying counter of def.
static bool alpha(Ref d1, Ref d2)
Are d1 and d2 α-equivalent?
static Ref is_uniform(Defs defs)
Yields defs.front(), if all defs are Check::alpha-equivalent (infer = false) and nullptr otherwise.
static bool assignable(Ref type, Ref value)
Can value be assigned to sth of type?
nat_t as_lit_arity() const
std::optional< nat_t > isa_lit_arity() const
Ref var(nat_t a, nat_t i)
bool is_set() const
Yields true if empty or the last op is set.
const T * isa_imm() const
const Def * op(size_t i) const
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
DefVec reduce(const Def *arg) const
Rewrites Def::ops by substituting this mutable's Var with arg.
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
bool is_closed() const
Has no free_vars()?
const Def * unfold_type() const
Yields the type of this Def and builds a new .Type (UInc n) if necessary.
const Def * proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
Some "global" variables needed all over the place.
static Ref size(Ref def)
Checks if def is a .Idx s and returns s or nullptr otherwise.
static bool eliminate(Vector< Ref * >)
Eliminate Infers that may have been resolved in the meantime by rebuilding.
Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple.
Lam * set(Filter filter, const Def *body)
static std::optional< T > isa(Ref def)
Facility to log what you are doing.
A (possibly paramterized) Tuple.
A dependent function type.
Helper class to retrieve Infer::arg if present.
static const Def * refer(const Def *def)
Retrieves Infer::arg from def.
This is a thin wrapper for std::span<T, N> with the following additional features:
Specific Bound depending on Up.
Extremum. Either Top (Up) or Bottom.
Data constructor for a Sigma.
const Def * level() const
The World represents the whole program and manages creation of Thorin nodes (Defs).
Ref insert(Ref d, Ref i, Ref val)
Ref ac(Ref type, Defs ops)
Ref iapp(Ref callee, Ref arg)
Places Infer arguments as demanded by Pi::implicit and then apps arg.
const Lit * lit(Ref type, u64 val)
Flags & flags()
Retrive compile Flags.
Ref gid2def(u32 gid)
Lookup Def by gid.
Ref uinc(Ref op, level_t offset=1)
const auto & externals() const
Ref singleton(Ref inner_type)
Sym sym(std::string_view)
const Lit * lit_univ(u64 level)
const Driver & driver() const
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Ref var(Ref type, Def *mut)
World(Driver *)
Inherits the state into the new World.
Ref pack(Ref arity, Ref body)
Ref pick(Ref type, Ref value)
Sigma * mut_sigma(Ref type, size_t size)
const Axiom * axiom(NormalizeFn n, u8 curry, u8 trip, Ref type, plugin_t p, tag_t t, sub_t s)
const Pi * pi(Ref dom, Ref codom, bool implicit=false)
const Lit * lit_idx(nat_t size, u64 val)
Constructs a Lit of type Idx of size size.
Ref vel(Ref type, Ref value)
Ref extract(Ref d, Ref i)
const Tuple * tuple()
the unit value of type []
const Lit * lit_nat(nat_t a)
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating Def with Def::gid gid.
Ref arr(Ref shape, Ref body)
const Def * register_annex(flags_t f, const Def *)
const Def * annex()
Get Axiom from a plugin.
Ref app(Ref callee, Ref arg)
Ref raw_app(Ref type, Ref callee, Ref arg)
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if THORIN_ENABLE_CHECKS.
Infer * mut_infer(Ref type)
Ref test(Ref value, Ref probe, Ref match, Ref clash)
const auto & annexes() const
Lam * mut_lam(const Pi *pi)
const Sigma * sigma()
The unit type within Type 0.
const Lam * lam(const Pi *pi, Lam::Filter f, Ref body)
#define DLOG(...)
Vaporizes to nothingness in Debug build.
Ref op(trait o, Ref type)
void error(const Def *def, const char *fmt, Args &&... args)
uint64_t scalerize_threshold
auto assert_emplace(C &container, Args &&... args)
Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
Vector< const Def * > DefVec
Compiler switches that must be saved and looked up in later phases of compilation.
static Sym demangle(World &, plugin_t u)
Reverts an Axiom::mangled string to a Sym.
absl::flat_hash_set< uint32_t > breakpoints