1//===- ShapeBase.td ----------------------------------------*- tablegen -*-===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// Base definitions for the `shape` dialect.
10//
11//===----------------------------------------------------------------------===//
12
13#ifndef SHAPE_BASE_TD
14#define SHAPE_BASE_TD
15
16include "mlir/IR/OpBase.td"
17
18//===----------------------------------------------------------------------===//
19// Shape Inference dialect definitions
20//===----------------------------------------------------------------------===//
21
22def ShapeDialect : Dialect {
23  let name = "shape";
24
25  let summary = "Types and operations for shape dialect";
26  let description = [{
27    This dialect contains operations for shape inference.
28
29    Note: Unless explicitly stated, all functions that return a shape and take
30    shapes as input, return the invalid shape if one of its operands is an
31    invalid shape. This avoids flagging multiple errors for one verification
32    failure. The dialect itself does not specify how errors should be combined
33    (there are multiple different options, from always choosing first operand,
34    concatting etc. on how to combine them).
35  }];
36
37  let cppNamespace = "::mlir::shape";
38
39  let hasConstantMaterializer = 1;
40}
41
42def Shape_ComponentType : DialectType<ShapeDialect,
43    CPred<"$_self.isa<::mlir::shape::ComponentType>()">, "component type">,
44    BuildableType<"$_builder.getType<::mlir::shape::ComponentType>()"> {
45  let typeDescription = [{
46    `shape.component_type` represents the tuple of shape, element type and
47    attribute.
48  }];
49}
50
51def Shape_ElementType : DialectType<ShapeDialect,
52    CPred<"$_self.isa<::mlir::shape::ElementType>()">, "element type">,
53    BuildableType<"$_builder.getType<::mlir::shape::ElementType>()"> {
54  let typeDescription = [{
55    `shape.element_type` represents the element type of the ShapedType. It may
56    be unknown, error or regular element type supported by ShapedType.
57  }];
58}
59
60def Shape_ShapeType : DialectType<ShapeDialect,
61    CPred<"$_self.isa<::mlir::shape::ShapeType>()">, "shape">,
62    BuildableType<"$_builder.getType<::mlir::shape::ShapeType>()"> {
63  let typeDescription = [{
64    `shape.type` represents either an unranked shape, a ranked shape with
65    possibly unknown dimensions or an invalid shape. The rank is of type
66    `shape.size` and, if rank is known, the extent is a 1D tensor of type
67    `shape.size`.
68
69    Shape is printed:
70    * `[*]` if it is an unranked shape
71    * `[?, 2]` if a rank 2 tensor with one unknown dimension
72    * `[3, 4]` is a rank 2 static tensor
73    * `[]` is a scalar
74    * `[1]` is a rank 1 tensor with 1 element
75    * `[invalid]` for an invalid shape
76  }];
77}
78
79def Shape_SizeType : DialectType<ShapeDialect,
80    CPred<"$_self.isa<::mlir::shape::SizeType>()">, "size">,
81    BuildableType<"$_builder.getType<::mlir::shape::SizeType>()"> {
82  let typeDescription = [{
83    `shape.size` represents a non-negative integer with support for being
84    unknown and invalid.
85
86    Operations on `shape.size` types are specialized to handle unknown/dynamic
87    value. So, for example, `<unknown> + x == <unknown>` for all non-error `x :
88    !shape.size` (e.g., an unknown value does not become known due to addition).
89  }];
90}
91
92def Shape_ValueShapeType : DialectType<ShapeDialect,
93    CPred<"$_self.isa<::mlir::shape::ValueShapeType>()">, "value shape">,
94    BuildableType<"::mlir::shape::ValueShapeType::get($_builder.getContext())">
95{
96  let typeDescription = [{
97    `shape.value_shape` represents the value produced by an operation (this
98    corresponds to `Value` in the compiler) and a shape. Conceptually this is a
99    tuple of a value (potentially unknown) and `shape.type`. The value and shape
100    can either or both be unknown. If both the `value` and `shape` are known,
101    then the shape of `value` is conformant with `shape`. That is, the shape of
102    the value conforms to the shape of the ValueShape, so that if we have
103    ValueShape `(value, shape)` then `join(shape_of(value), shape)` would be
104    error free and in particular it means that if both are statically known,
105    then they are equal.
106  }];
107}
108
109def Shape_ExtentTensorType :
110    1DTensorOf<[Index]>,
111    BuildableType<"::mlir::RankedTensorType::get({ShapedType::kDynamicSize}, "
112                  "$_builder.getType<::mlir::IndexType>())"> {
113  let typeDescription = [{
114    The extent tensor is a tensor of rank one with arbitrarily many index
115    elements. Like `!shape.shape`, it is used to represent shapes with the
116    difference that it is guaranteed to be error-free.
117  }];
118}
119
120def Shape_ShapeOrSizeType : AnyTypeOf<[Shape_SizeType, Shape_ShapeType],
121  "shape or size">;
122
123def Shape_ShapeOrExtentTensorType : AnyTypeOf<[Shape_ShapeType,
124                                               Shape_ExtentTensorType],
125                                              "shape or extent tensor">;
126
127def Shape_SizeOrIndexType : AnyTypeOf<[Shape_SizeType, Index], "size or index">;
128
129def Shape_WitnessType : DialectType<ShapeDialect,
130    CPred<"$_self.isa<::mlir::shape::WitnessType>()">, "witness">,
131    BuildableType<"$_builder.getType<::mlir::shape::WitnessType>()"> {
132  let typeDescription = [{
133    A witness is a structural device in the compiler to maintain ordering of
134    code relying on information obtained from passing assertions. Witnesses do
135    not represent any physical data.
136
137    "cstr_" operations will return witnesses and be lowered into assertion logic
138    when not resolvable at compile time.
139
140    "assuming_" operations will take witnesses as input and represent only
141    information to the compiler, so they do not exist in executing code. Code
142    that is dependent on "assuming_" operations can assume all cstr operations
143    transitively before are honored as true.
144
145    These abstractions are intended to allow the compiler more freedom with
146    assertions by merely showing the assertion through dataflow at this time
147    rather than a side effecting operation that acts as a barrier. This can be
148    viewed similarly to a compiler representation of promises from asynchronous,
149    possibly crashing assertions. Reliant code will not be reordered to before
150    the code and non-reliant code can be reordered freely, and there are no
151    guarantees on the final ordering of the assertions or their related code.
152  }];
153}
154
155#endif // SHAPE_BASE_TD
156