Skip to content

Commit

Permalink
cleanup parsing ptrns:
Browse files Browse the repository at this point in the history 
* new feature: [ptrn] «x: Nat, T» -> U
* better handling of implicit in parser/ast
  • Loading branch information
@leissa
leissa committed Nov 1, 2024
1 parent ccfa537 commit e702361
Show file tree
Hide file tree
Showing 9 changed files with 54 additions and 54 deletions.
13 changes: 7 additions & 6 deletions include/mim/ast/ast.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,7 @@ class Ptrn : public Decl {

bool rebind() const { return rebind_; }
Dbg dbg() const { return dbg_; }
virtual bool implicit() const { return false; }

virtual void bind(Scopes&, bool quiet = false) const = 0;
Ref emit_value(Emitter&, Ref) const;
Expand Down Expand Up @@ -257,6 +258,7 @@ class TuplePtrn : public Ptrn {
Tok::Tag delim_r() const { return Tok::delim_l2r(delim_l()); }
bool is_paren() const { return delim_l() == Tok::Tag::D_paren_l; }
bool is_brckt() const { return delim_l() == Tok::Tag::D_brckt_l; }
bool implicit() const override { return delim_l_ == Tok::Tag::D_brace_l; }

const auto& ptrns() const { return ptrns_; }
const Ptrn* ptrn(size_t i) const { return ptrns_[i].get(); }
Expand Down Expand Up @@ -442,12 +444,11 @@ class PiExpr : public Expr {
public:
class Dom : public Node {
public:
Dom(Loc loc, bool is_implicit, Ptr<Ptrn>&& ptrn)
Dom(Loc loc, Ptr<Ptrn>&& ptrn)
: Node(loc)
, is_implicit_(is_implicit)
, ptrn_(std::move(ptrn)) {}

bool is_implicit() const { return is_implicit_; }
bool implicit() const { return ptrn_->implicit(); }
const Ptrn* ptrn() const { return ptrn_.get(); }
const IdPtrn* ret() const { return ret_.get(); }

Expand All @@ -465,7 +466,6 @@ class PiExpr : public Expr {
mutable Pi* decl_ = nullptr;

private:
bool is_implicit_;
Ptr<Ptrn> ptrn_;
mutable Ptr<IdPtrn> ret_;

Expand Down Expand Up @@ -811,10 +811,11 @@ class LamDecl : public RecDecl {
public:
class Dom : public PiExpr::Dom {
public:
Dom(Loc loc, bool is_implicit, Ptr<Ptrn>&& ptrn, Ptr<Expr>&& filter)
: PiExpr::Dom(loc, is_implicit, std::move(ptrn))
Dom(Loc loc, Ptr<Ptrn>&& ptrn, Ptr<Expr>&& filter)
: PiExpr::Dom(loc, std::move(ptrn))
, filter_(std::move(filter)) {}

bool implicit() const { return ptrn()->implicit(); }
const Expr* filter() const { return filter_.get(); }

void bind(Scopes& scopes, bool quiet = false) const override;
Expand Down
4 changes: 2 additions & 2 deletions include/mim/plug/affine/pass/lower_for.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ namespace mim::plug::affine {
/// con %affine.For_impl
/// (m: Nat , n: Nat , Ts: «n; *»)
/// (begin: Idx m, end: Idx m, step: Idx m, init: «i: n; Ts#i»,
/// body: Cn [iter: Idx m, acc: «i: n; Ts#i», yield: Cn [«i: n; Ts#i»]],
/// exit: Cn [«i: n; Ts#i»]
/// body: Cn [iter: Idx m, acc: «i: n; Ts#i», yield: Cn «i: n; Ts#i»],
/// exit: Cn «i: n; Ts#i»
/// ) =
/// con head(iter: Idx m, acc: «i: n; Ts#i») =
/// con new_body() = body (iter, acc, cn acc: «i: n; Ts#i» =
Expand Down
4 changes: 2 additions & 2 deletions src/mim/ast/emit.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ Ref ArrowExpr::emit_(Emitter& e) const {
}

void PiExpr::Dom::emit_type(Emitter& e) const {
pi_ = decl_ ? decl_ : e.world().mut_pi(e.world().type_infer_univ(), is_implicit());
pi_ = decl_ ? decl_ : e.world().mut_pi(e.world().type_infer_univ(), implicit());
auto dom_t = ptrn()->emit_type(e);

if (ret()) {
Expand All @@ -216,7 +216,7 @@ void PiExpr::Dom::emit_type(Emitter& e) const {

Ref PiExpr::emit_decl(Emitter& e, Ref type) const {
const auto& first = doms().front();
return first->decl_ = e.world().mut_pi(type, first->is_implicit())->set(loc());
return first->decl_ = e.world().mut_pi(type, first->implicit())->set(loc());
}

void PiExpr::emit_body(Emitter& e, Ref) const { emit(e); }
Expand Down
59 changes: 29 additions & 30 deletions src/mim/ast/parser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,10 +78,19 @@
case Tag::D_paren_l: /*TupleExpr*/ \
case Tag::D_quote_l /*ArrExpr*/

#define C_PTRN \
#define C_CURRIED_B \
D_brace_l: \
case Tag::D_brckt_l: \
case Tag::D_quote_l

#define C_CURRIED_P \
D_brace_l: \
case Tag::D_brckt_l: \
case Tag::D_paren_l

#define C_PTRN_P \
M_id: \
case Tag::T_backtick: \
case Tag::D_brace_l: \
case Tag::D_brckt_l: \
case Tag::D_paren_l
// clang-format on
Expand Down Expand Up @@ -338,9 +347,11 @@ Ptr<Expr> Parser::parse_lit_expr() {

Ptr<Expr> Parser::parse_sigma_expr() {
auto ptrn = parse_tuple_ptrn();
if (ahead().isa(Tag::D_brace_l) || ahead().isa(Tag::D_brckt_l) || ahead().isa(Tag::T_arrow))
return parse_pi_expr(std::move(ptrn));
return ptr<SigmaExpr>(std::move(ptrn));
switch (ahead().tag()) {
case Tag::C_CURRIED_B:
case Tag::T_arrow: return parse_pi_expr(std::move(ptrn)); // TODO precedences for patterns
default: return ptr<SigmaExpr>(std::move(ptrn));
}
}

Ptr<Expr> Parser::parse_tuple_expr() {
Expand Down Expand Up @@ -369,25 +380,18 @@ Ptr<Expr> Parser::parse_pi_expr(Ptr<Ptrn>&& ptrn) {
entity = "returning continuation type";

Ptrs<PiExpr::Dom> doms;
if (has_first) doms.emplace_back(ptr<PiExpr::Dom>(ptrn->loc(), false, std::move(ptrn)));
if (has_first) doms.emplace_back(ptr<PiExpr::Dom>(ptrn->loc(), std::move(ptrn)));

if (!has_first || !ahead().isa(Tag::T_arrow)) {
while (true) {
auto track = tracker();
auto implicit = false;
Ptr<Ptrn> ptrn;
if (ahead().isa(Tok::Tag::D_brace_l)) {
implicit = true;
ptrn = parse_tuple_ptrn();
} else {
auto prec = tag == Tag::K_Cn ? Prec::Bot : Prec::Pi;
ptrn = parse_ptrn(Tag::D_brckt_l, "domain of a "s + entity, prec);
}

doms.emplace_back(ptr<PiExpr::Dom>(track, implicit, std::move(ptrn)));
auto track = tracker();
auto prec = tag == Tag::K_Cn ? Prec::Bot : Prec::Pi;
auto ptrn = ahead().isa(Tok::Tag::D_brace_l) ? parse_tuple_ptrn()
: parse_ptrn(Tag::D_brckt_l, "domain of a "s + entity, prec);
doms.emplace_back(ptr<PiExpr::Dom>(track, std::move(ptrn)));

switch (ahead().tag()) {
case Tag::C_PTRN: continue;
case Tag::C_CURRIED_B: continue;
default: break;
}
break;
Expand Down Expand Up @@ -666,20 +670,15 @@ Ptr<LamDecl> Parser::parse_lam_decl() {
auto dbg = decl ? parse_name(entity) : Dbg();
Ptrs<LamDecl::Dom> doms;
while (true) {
auto track = tracker();
bool implicit = false;
Ptr<Ptrn> ptrn;
if (ahead().isa(Tok::Tag::D_brace_l)) {
implicit = true;
ptrn = parse_tuple_ptrn();
} else {
ptrn = parse_ptrn(Tag::D_paren_l, "domain pattern of a "s + entity, prec);
}
auto track = tracker();
auto ptrn = ahead().isa(Tok::Tag::D_brace_l)
? parse_tuple_ptrn()
: parse_ptrn(Tag::D_paren_l, "domain pattern of a "s + entity, prec);
auto filter = accept(Tag::T_at) ? parse_expr("filter") : nullptr;
doms.emplace_back(ptr<LamDecl::Dom>(track, std::move(ptrn), std::move(filter)));

doms.emplace_back(ptr<LamDecl::Dom>(track, implicit, std::move(ptrn), std::move(filter)));
switch (ahead().tag()) {
case Tag::C_PTRN: continue;
case Tag::C_CURRIED_P: continue;
default: break;
}
break;
Expand Down
4 changes: 2 additions & 2 deletions src/mim/ast/stream.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ std::ostream& ArrowExpr::stream(Tab& tab, std::ostream& os) const {
}

std::ostream& PiExpr::Dom::stream(Tab& tab, std::ostream& os) const {
print(os, "{}{}", is_implicit() ? "." : "", S(tab, ptrn()));
print(os, "{}{}", implicit() ? "." : "", S(tab, ptrn()));
if (ret()) print(os, " -> {}", S(tab, ret()->type()));
return os;
}
Expand Down Expand Up @@ -187,7 +187,7 @@ std::ostream& RecDecl::stream(Tab& tab, std::ostream& os) const {
}

std::ostream& LamDecl::Dom::stream(Tab& tab, std::ostream& os) const {
print(os, "{}{}", is_implicit() ? "." : "", S(tab, ptrn()));
print(os, "{}{}", implicit() ? "." : "", S(tab, ptrn()));
if (filter()) print(os, "@({})", S(tab, filter()));
if (ret()) print(os, ": {}", S(tab, ret()->type()));
return os;
Expand Down
4 changes: 2 additions & 2 deletions src/mim/plug/affine/affine.mim
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ import mem;
axm %affine.For:
Cn [m: Nat , n: Nat , Ts: «n; *»]
[begin: Idx m, _end: Idx m, step: Idx m, init: «i: n; Ts#i»,
body: Cn [iter: Idx m, acc: «i: n; Ts#i», yield: Cn [«i: n; Ts#i»]],
exit: Cn [«i: n; Ts#i»]
body: Cn [iter: Idx m, acc: «i: n; Ts#i», yield: Cn «i: n; Ts#i»],
exit: Cn «i: n; Ts#i»
];
///
/// ## Passes and Phases
Expand Down
8 changes: 4 additions & 4 deletions src/mim/plug/core/core.mim
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,22 +102,22 @@ axm %core.bit1(f, neg, id, t): {s: Nat} [m: Nat] [Idx s] → Idx s, normalize_bi
///
axm %core.bit2( f, nor, nciff, nfst, niff, nsnd, xor_, nand,
and_, nxor, snd, iff, fst, ciff, or_, t):
{s: Nat} [m: Nat] [«2; Idx s»] → Idx s , normalize_bit2;
{s: Nat} [m: Nat] «2; Idx s» → Idx s , normalize_bit2;
///
/// ### %%core.shr
///
/// Shift right:
/// * [`a`rithmetic shift right](https://en.wikipedia.org/wiki/Arithmetic_shift)
/// * [`l`ogical shift right](https://en.wikipedia.org/wiki/Logical_shift)
///
axm %core.shr(a, l): {s: Nat} [«2; Idx s»] → Idx s, normalize_shr;
axm %core.shr(a, l): {s: Nat} «2; Idx s» → Idx s, normalize_shr;
///
/// ### %%core.wrap
///
/// Integer operations that may overflow.
/// You can specify the desired behavior in the case of an overflow with the curried argument just in front of the actual argument by providing a mim::plug::core::Mode as `Nat`.
///
axm %core.wrap(add, sub, mul, shl): {s: Nat} [m: Nat] [«2; Idx s»] → Idx s, normalize_wrap;
axm %core.wrap(add, sub, mul, shl): {s: Nat} [m: Nat] «2; Idx s» → Idx s, normalize_wrap;

lam %core.minus {s: Nat} (m: Nat) (a: Idx s): Idx s = %core.wrap.sub m (0:(Idx s), a);
///
Expand Down Expand Up @@ -202,7 +202,7 @@ axm %core.icmp(xygle = f, xyglE = e, xygLe, xygLE,
XyGle = sg, XyGlE = sge, XyGLe, XyGLE,
XYgle, XYglE, XYgLe, XYgLE,
XYGle, XYGlE, XYGLe = ne, XYGLE = t):
{s: Nat} [«2; Idx s»] → Bool , normalize_icmp;
{s: Nat} «2; Idx s» → Bool , normalize_icmp;
///
/// ### %%core.extrema
///
Expand Down
8 changes: 4 additions & 4 deletions src/mim/plug/math/math.mim
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ let %math.PXR24 = %math.F %math.pxr24;
///
/// Arithmetic operations.
axm %math.arith(add, sub, mul, div, rem):
{pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_arith;
{pe: «2; Nat»} [Nat] «2; %math.F pe» → %math.F pe, normalize_arith;

lam %math.minus {pe: «2; Nat»} (m: Nat) (a: %math.F pe): %math.F pe =
%math.arith.sub m (0:(%math.F pe), a);
Expand Down Expand Up @@ -72,7 +72,7 @@ lam %math.minus {pe: «2; Nat»} (m: Nat) (a: %math.F pe): %math.F pe =
///
axm %math.extrema(im = fmin, iM = fmax,
Im = ieee754min, IM = ieee754max):
{pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_extrema;
{pe: «2; Nat»} [Nat] «2; %math.F pe» → %math.F pe, normalize_extrema;
///
/// ### %%math.tri
///
Expand Down Expand Up @@ -111,7 +111,7 @@ axm %math.tri(ahff = sin , ahfF = cos , ahFf = tan , ahFF,
///
/// Power function: \f$x^y\f$
///
axm %math.pow: {pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_pow;
axm %math.pow: {pe: «2; Nat»} [Nat] «2; %math.F pe» → %math.F pe, normalize_pow;
///
/// ### %%math.rt
///
Expand Down Expand Up @@ -223,7 +223,7 @@ axm %math.cmp(ugle = f, uglE = e, ugLe = l, ugLE = le,
uGle = g, uGlE = ge, uGLe = ne, uGLE = o,
Ugle = u, UglE = ue, UgLe = ul, UgLE = ule,
UGle = ug, UGlE = uge, UGLe = une, UGLE = t):
{pe: «2; Nat»} [Nat] [«2; %math.F pe»] → Bool, normalize_cmp;
{pe: «2; Nat»} [Nat] «2; %math.F pe» → Bool, normalize_cmp;
///
/// ### %%math.conv
///
Expand Down
4 changes: 2 additions & 2 deletions src/mim/plug/regex/regex.mim
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,13 @@ let RE = {n: Nat} [%mem.M, Str n, Idx n] → Res n;
/// A sequence of RE's, e.g. `\d\d\d` matching 3 digits:
/// `%%regex.conj (%%regex.cls.d, %%regex.cls.d, %%regex.cls.d)`
///
axm %regex.conj: [n: Nat] [«n; RE»] → RE, normalize_conj, 2;
axm %regex.conj: [n: Nat] «n; RE» → RE, normalize_conj, 2;
///
/// ### %%regex.disj
///
/// Match any of the sub expressions: `[0123456789]`
///
axm %regex.disj: [n: Nat] [«n; RE»] → RE, normalize_disj, 2;
axm %regex.disj: [n: Nat] «n; RE» → RE, normalize_disj, 2;
///
/// ## Values
///
Expand Down

0 comments on commit e702361

Please sign in to comment.