25 auto& world = type->
world();
33 return world.call(
quant::star, optional_app->arg());
38 if (
auto quant_app =
Axm::isa<quant>(arg))
return world.app(callee, quant_app->arg());
51 for (
const auto* proj : arg->
projs()) {
56 new_args.push_back(proj);
67 assert(!args.empty());
68 auto& world = args.front()->world();
69 return std::accumulate(args.begin() + 1, args.end(), args.front(), [&world](
const Def* lhs,
const Def* rhs) {
70 return world.call<ConjOrDisj, false>(Defs{lhs, rhs});
75 auto& world = type->
world();
76 world.DLOG(
"conj {}:{} ({})", type, callee, arg);
89 if (lhs_range && rhs_range)
return Lit::as(lhs_range->arg()->proj(0)) <
Lit::as(rhs_range->arg()->proj(0));
91 if (lhs_range)
return false;
92 if (rhs_range)
return true;
94 return lhs->
gid() < rhs->
gid();
98 std::stable_sort(args.begin(), args.end(), &
compare_re);
100 auto new_end = std::unique(args.begin(), args.end());
101 args.erase(new_end, args.end());
118 auto ranges_begin = args.begin();
119 while (ranges_begin != args.end() && !
Axm::isa<range>(*ranges_begin)) ranges_begin++;
120 if (ranges_begin == args.end())
return;
122 std::set<const Def*> to_remove;
124 auto& world = (*ranges_begin)->world();
126 std::transform(ranges_begin, args.end(), std::back_inserter(old_ranges),
get_range);
129 old_ranges, [&world](
auto&&... args) { world.DLOG(std::forward<
decltype(args)>(args)...); });
132 args.erase(ranges_begin, args.end());
133 std::transform(new_ranges.begin(), new_ranges.end(), std::back_inserter(args),
app_range{world});
143 auto check_arg_equiv = [](
const Def* lhs,
const Def* rhs) {
146 if (
auto rng_rhs =
Axm::isa<range>(not_rhs->arg()))
return rng_lhs == rng_rhs;
151 return check_arg_equiv(lhs, rhs) || check_arg_equiv(rhs, lhs);
155 Ranges lhs_ranges, rhs_ranges;
156 auto only_ranges = std::ranges::views::filter([](
auto d) {
return Axm::isa<range>(
d); });
157 std::ranges::transform(lhs | only_ranges, std::back_inserter(lhs_ranges),
get_range);
158 std::ranges::transform(rhs | only_ranges, std::back_inserter(rhs_ranges),
get_range);
159 return std::ranges::includes(lhs_ranges, rhs_ranges) || std::ranges::includes(rhs_ranges, lhs_ranges);
163 auto& world = type->
world();
165 auto contains_any = [](
auto args) {
166 return std::ranges::find_if(args, [](
const Def* ax) ->
bool {
return Axm::isa<any>(ax); }) != args.end();
170 if (contains_any(new_args))
return world.annex<
any>();
174 const Def* to_remove =
nullptr;
175 for (
const auto* cls0 : new_args) {
176 for (
const auto* cls1 : new_args)
188 erase(new_args, to_remove);
189 world.DLOG(
"final ranges {, }", new_args);
192 if (new_args.size() > 1)
return world.call<
disj,
false>(new_args);
193 return new_args.back();
199 auto& world = type->
world();
200 auto [lhs, rhs] = arg->
projs<2>();
202 if (!lhs->isa<
Var>() && !rhs->isa<
Var>())
203 if (lhs->as<
Lit>()->
get() > rhs->as<
Lit>()->
get())
return world.raw_app(type, callee, {rhs, lhs});
static auto isa(const Def *def)
nat_t as_lit_arity() const
World & world() const noexcept
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
static T as(const Def *def)
This is a thin wrapper for absl::InlinedVector<T, N, A> which is a drop-in replacement for std::vecto...
The World represents the whole program and manages creation of MimIR nodes (Defs).
std::pair< std::uint64_t, std::uint64_t > Range
std::optional< Range > merge_ranges(Range a, Range b) noexcept
void merge_ranges(DefVec &args)
void make_vector_unique(DefVec &args)
auto get_range(const Def *rng) -> Range
void flatten_in_arg(const Def *arg, DefVec &new_args)
bool is_in_range(Range range, nat_t needle)
const Def * normalize_conj(const Def *type, const Def *callee, const Def *arg)
const Def * normalize_range(const Def *type, const Def *callee, const Def *arg)
const Def * normalize_disj(const Def *type, const Def *, const Def *arg)
const Def * normalize_quant(const Def *type, const Def *callee, const Def *arg)
const Def * normalize_not(const Def *, const Def *, const Def *)
bool compare_re(const Def *lhs, const Def *rhs)
const Def * make_binary_tree(Defs args)
bool equals_any(const Def *cls0, const Def *cls1)
Vector< const Def * > DefVec
Vector< T, N, A >::size_type erase(Vector< T, N, A > &c, const U &value) noexcept
#define MIM_regex_NORMALIZER_IMPL
const Def * operator()(Range rng)