MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
matrix.h
Go to the documentation of this file.
1#pragma once
2
4#include <mim/world.h>
5
7
9
10#define INTERNAL_PREFIX "internal_mapRed_"
11
12/// %mat.zero: Π [n: .Nat, S: «n; .Nat», m: .Nat] -> %mat.Mat (n,S,(.Idx m));
13inline const Def* zero_int(World& w, Ref n, Ref S, Ref mem, nat_t m) {
14 // TODO: use mim definition by name
15 return w.app(w.annex<matrix::constMat>(), {n, S, w.type_idx(m), mem, w.lit_idx(m, 0)});
16}
17
18inline const Def* op_read(Ref mem, Ref matrix, Ref idx) {
19 auto& world = matrix->world();
20 auto mat_ty = match<Mat>(matrix->type());
21 if (!mat_ty) return matrix;
22 assert(mat_ty);
23 world.DLOG("matrix read: {}[{}]", matrix, idx);
24 world.DLOG(" matrix type: {}", matrix->type());
25 auto [n, S, T] = mat_ty->args<3>();
26 world.DLOG(" (n,S,T): {}, {}, {}", n, S, T);
27 return world.app(world.app(world.annex<read>(), {n, S, T}), {mem, matrix, idx});
28}
29
30} // namespace mim::plug::matrix
Base class for all Defs.
Definition def.h:220
World & world() const
Definition def.cpp:417
const Def * type() const
Definition def.h:245
Helper class to retrieve Infer::arg if present.
Definition def.h:85
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
The matrix Plugin
Definition matrix.h:8
const Def * op_read(Ref mem, Ref matrix, Ref idx)
Definition matrix.h:18
const Def * zero_int(World &w, Ref n, Ref S, Ref mem, nat_t m)
mat.zero: Π [n: .Nat, S: «n; .Nat», m: .Nat] -> mat.Mat (n,S,(.Idx m));
Definition matrix.h:13
The mem Plugin
Definition mem.h:10
u64 nat_t
Definition types.h:43
auto match(Ref def)
Definition axiom.h:105