27 if (
auto def = std::get_if<Ref>(&m))
return *def;
28 if (
auto nat = std::get_if<nat_t>(&m))
return w.lit_nat(*
nat);
29 return w.lit_nat((
nat_t)std::get<Mode>(m));
37 return w.app(w.annex(o), type);
45 return w.app(w.app(w.annex(o), def->
type()), def);
64 World& w = d->world();
65 return w.extract(d, w.call(
conv::u, d->unfold_type()->arity(), i));
68 World& w = d->world();
76 World& w = d->world();
77 return w.insert(d, w.call(
conv::u, d->unfold_type()->arity(), i), val);
80 World& w = d->world();
107 auto tab = make_truth_table(
id);
108 return tab[0][1] == tab[1][0];
113 case plug::core::bit2::t:
120 case plug::core::bit2::f:
return true;
121 default:
return false;
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
Helper class to retrieve Infer::arg if present.
Specific Bound depending on Up.
The World represents the whole program and manages creation of Thorin nodes (Defs).
Ref extract_unsafe(Ref d, Ref i)
Ref insert_unsafe(Ref d, Ref i, Ref val)
constexpr std::array< std::array< u64, 2 >, 2 > make_truth_table(bit2 id)
Use like this: a op b = tab[a][b]
Ref op(trait o, Ref type)
std::variant< Mode, nat_t, Ref > VMode
Give Mode as thorin::plug::math::Mode, thorin::nat_t or Ref.
const Sigma * convert(const TBound< up > *b)
constexpr bool is_associative(Id id)
constexpr bool is_commutative(Id)
#define THORIN_ENUM_OPERATORS(E)
Use this to declare all kind of bit and comparison operators for an enum E.