25 auto& world = type->
world();
33 return world.call(
quant::star, optional_app->arg());
38 if (
auto quant_app =
mim::match<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);
90 if (rhs_range)
return Lit::as(lhs_range->arg()->proj(0)) <
Lit::as(rhs_range->arg()->proj(0));
93 }
else if (rhs_range) {
102 std::stable_sort(args.begin(), args.end(), &
compare_re);
104 auto new_end = std::unique(args.begin(), args.end());
105 args.erase(new_end, args.end());
122 auto ranges_begin = args.begin();
123 while (ranges_begin != args.end() && !
mim::match<range>(*ranges_begin)) ranges_begin++;
124 if (ranges_begin == args.end())
return;
126 std::set<const Def*> to_remove;
128 auto& world = (*ranges_begin)->world();
130 std::transform(ranges_begin, args.end(), std::back_inserter(old_ranges),
get_range);
133 old_ranges, [&world](
auto&&... args) { world.DLOG(std::forward<
decltype(args)>(args)...); });
136 args.erase(ranges_begin, args.end());
137 std::transform(new_ranges.begin(), new_ranges.end(), std::back_inserter(args),
app_range{world});
147 auto check_arg_equiv = [](
const Def* lhs,
const Def* rhs) {
155 return check_arg_equiv(lhs, rhs) || check_arg_equiv(rhs, lhs);
159 Ranges lhs_ranges, rhs_ranges;
160 auto only_ranges = std::ranges::views::filter([](
auto d) {
return match<range>(
d); });
161 std::ranges::transform(lhs | only_ranges, std::back_inserter(lhs_ranges),
get_range);
162 std::ranges::transform(rhs | only_ranges, std::back_inserter(rhs_ranges),
get_range);
163 return std::ranges::includes(lhs_ranges, rhs_ranges) || std::ranges::includes(rhs_ranges, lhs_ranges);
167 auto& world = type->
world();
169 auto contains_any = [](
auto args) {
170 return std::ranges::find_if(args, [](
const Def* ax) ->
bool {
return mim::match<any>(ax); }) != args.end();
174 if (contains_any(new_args))
return world.annex<
any>();
178 const Def* to_remove =
nullptr;
179 for (
const auto* cls0 : new_args) {
180 for (
const auto* cls1 : new_args)
192 erase(new_args, to_remove);
193 world.DLOG(
"final ranges {, }", new_args);
196 if (new_args.size() > 1)
return world.call<
disj,
false>(new_args);
197 return new_args.back();
203 auto& world = type->
world();
204 auto [lhs, rhs] = arg->
projs<2>();
206 if (!lhs->isa<
Var>() && !rhs->isa<
Var>())
207 if (lhs->as<
Lit>()->
get() > rhs->as<
Lit>()->
get())
return world.raw_app(type, callee, {rhs, lhs});
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...
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
auto match(const Def *def)
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)