Kina Surface Syntax (.kina)

Status. This is the user-facing program surface syntax for kina-ai using the .kina file extension. The compiler supports both the S-expression (.kina) format and the new .kina syntax, dynamically selected via the input file extension.

Pipeline. Text → Kina_parser_wrapper.parse_kina_program → Ast_surface.expr → Type_formation.check_program → Emitter.emit_tensor_program (MLIR).

Grammar and Syntactic Conventions

Lexical Rules

• Comments: Support for // (single-line comments) and /* ... */ (multi-line comments).
• Dimensions: Separated by commas inside brackets, e.g., [B, S, D]. Static dimensions are integers ≥ 1; symbolic dimensions are variables starting with a letter.
• Named Parameters: Certain methods use explicit parameter names to verify usage correctness (e.g., axis=1).

Syntax Mapping Reference

The following table maps the legacy S-expression syntax to the modern .kina syntax:

Detailed Syntax Examples

1. 2D Matrix Multiplication

• Legacy (.kina):

  (matmul (tensor F32 [2 3]) (tensor F32 [3 4]))
  

• Modern (.kina):

  tensor<F32, [2, 3], @host> @ tensor<F32, [3, 4], @host>
  

2. Constraint validation with requires

• Legacy (.kina):

  (requires (= B B_prime) (= K K_prime) (matmul (tensor F32 [B M K]) (tensor F32 [B_prime K_prime N])))
  

• Modern (.kina):

  requires [B = B_prime, K = K_prime] compute {
    tensor<F32, [B, M, K], @host> @ tensor<F32, [B_prime, K_prime, N], @host>
  }
  

3. Reductions & Keepdims

• Legacy (.kina):

  (reduce_keep mean 1 (tensor F32 [2 3]))
  

• Modern (.kina):

  tensor<F32, [2, 3], @host>.reduce_keep(op=mean, axis=1)
  

4. Slicing & Concatenating Tensors

• Legacy (.kina):

  (slice 0 0 1 (tensor F32 [2 3]))
  

• Modern (.kina):

  tensor<F32, [2, 3], @host>.slice(axis=0, start=0, stop=1)
  

5. Reshaping, Transposing & Broadcasting

• Legacy (.kina):

  (transpose [1 0] (tensor F32 [2 3]))
  

• Modern (.kina):

  tensor<F32, [2, 3], @host>.transpose([1, 0])
  

Phase 0 surface: S-expression programs

Status. This is the user-facing program surface accepted by the Phase 0 bootstrap compiler today. Normative typing rules live in docs/10-spec/11-phase-0/01–03; this page is the grammar and conventions for the concrete syntax. A separate .kina text syntax is Phase 7 (see docs/10-spec/11-phase-0/README.md and docs/10-spec/11-phase-0/05-implementation-infrastructure.md); until then, programs are one parenthesized expression (optionally wrapped in requires).

Pipeline. Text → Sexpr_parser.parse_program → Ast_surface.expr → Type_formation.check_program → Emitter.emit_tensor_program (MLIR).

Lexical rules

• Whitespace: spaces separate tokens; no significance beyond token boundaries.
• Identifiers (dtype, unary op name): letters, digits, underscore (_), matched case-sensitively where the parser uses exact tokens (e.g. F32, sum).
• Symbolic dimensions: non-empty strings of [a-zA-Z0-9_] that are not parsed as positive decimal integers. Examples: B, batch, d0.
• Static dimensions: decimal integers ≥ 1 (tensor axis lengths). Zero or negative literals are rejected for normal tensor shapes.
• Integers elsewhere: slice bounds, transpose permutation entries, reduce / concat / slice axis indices — as signed or unsigned per the form below.

Programs

Program ::= Expr
          | RequiresProgram

RequiresProgram ::= '(' 'requires' RequireClause+ Expr ')'
RequireClause   ::= '(' '=' DimAtom DimAtom ')'
DimAtom         ::= <static-dim> | <symbolic-dim>

• requires is allowed only at the root: one (requires …) wrapping the whole program. Nested requires in sub-expressions is rejected at type-check.
• Each RequireClause is a dimension equality (same meaning as tensor shape entries). They are asserted as extra integer equalities in Z3 together with the default axiom every symbolic dim ≥ 1 (phase-0/02 §15).
• Sugar: (requires (e)) with no (= …) clauses is accepted and treated as e (parser unwraps).

Tensor literal

TensorLiteral ::= '(' 'tensor' DType Shape ')'
DType         ::= 'F32' | 'F16' | 'BF16' | 'F8E4M3' | 'F8E5M2'
                | 'I64' | 'I32' | 'I16' | 'I8' | 'I4' | 'Bool'
Shape         ::= '[' (Dim (' ' Dim)*)? ']'
Dim           ::= <static-dim> | <symbolic-dim>

Expressions

Axes in transpose, reduce, slice, concat are 0-based (first axis is 0).

Expr ::=
    TensorLiteral
  | '(' 'add' Expr Expr ')'
  | '(' 'mul' Expr Expr ')'
  | '(' 'sub' Expr Expr ')'
  | '(' 'div' Expr Expr ')'
  | '(' 'pow' Expr Expr ')'
  | '(' 'max' Expr Expr ')'
  | '(' 'min' Expr Expr ')'
  | '(' 'eq' Expr Expr ')'
  | '(' 'ne' Expr Expr ')'
  | '(' 'lt' Expr Expr ')'
  | '(' 'le' Expr Expr ')'
  | '(' 'gt' Expr Expr ')'
  | '(' 'ge' Expr Expr ')'
  | '(' 'bitwise_and' Expr Expr ')'
  | '(' 'bitwise_or' Expr Expr ')'
  | '(' 'bitwise_xor' Expr Expr ')'
  | '(' 'rem' Expr Expr ')'
  | '(' 'frem' Expr Expr ')'
  | '(' 'matmul' Expr Expr ')'
  | '(' 'unary' <name> Expr ')'
  | '(' 'cast' DType Expr ')'
  | '(' 'transpose' Permutation Expr ')'
  | '(' 'reduce' <op> <axis> Expr ')'
  | '(' 'reduce_keep' <op> <axis> Expr ')'
  | '(' 'broadcast' Shape Expr ')'
  | '(' 'slice' <axis> <start> <stop> Expr ')'
  | '(' 'concat' <axis> Expr Expr ')'
  | '(' 'reshape' Expr Shape ')'

Permutation ::= '[' (<int> (' ' <int>)*)? ']'

• Elementwise binary: add / mul / sub / div share dtypes and shapes; pow is on all float dtypes (float8 uses extf → math.powf → truncf in a linalg.generic); max / min use linalg.maxf / minf for f32/f16/bf16 and arith.maximumf / minimumf for float8, or signed int max/min; comparisons eq … ge yield Bool tensors (i1 in MLIR); lt–ge are not defined for bool operands. bitwise_* require bool or signed int operands. rem is signed int remainder (arith.remsi). frem is floating remainder (arith.remf, with an f32 bridge for float8).
• unary: <name> is lowered for relu, neg, abs, exp, log, sqrt, rsqrt, tanh, sigmoid, silu, gelu, bitwise_not, …; float8 nonlinear ops use an f32 bridge inside linalg.generic (see ADR). Typed reduce mean on float8 is supported.
• reduce / reduce_keep: <op> is a word (sum, mean, max, min, …); <axis> is a non-negative int. reduce_keep keeps the reduced axis as length 1.
• broadcast: target Shape must have rank ≥ source rank; rules match shape_ops.broadcastable (NumPy-style trailing alignment).
• slice: static axis size required in the checker for the sliced dimension.
• reshape: element count (∏ dims) must be provable — static product, or Z3 (including requires). MLIR lowering still requires a fully static target Shape for tensor.reshape’s shape operand.

Unsupported leading keywords → parse error: "unsupported expression form".

Examples

(add (tensor F32 [2 3]) (tensor F32 [2 3]))
(matmul (tensor F32 [2 3]) (tensor F32 [3 4]))
(reduce sum 1 (tensor F32 [2 3]))
(broadcast [2 3] (tensor F32 [1 3]))
(requires (= B A) (broadcast [A A] (tensor F32 [B 1])))
(requires (= A 6) (reshape (tensor F32 [A]) [1 6]))

Runnable copies live under tests/compiler/examples/*.kina (see tests/compiler/examples/README.md).

API: pretty-printing

The OCaml module Ast_surface exposes pp_tensor and pp_expr: turn a parsed expr back into canonical S-expression text (for docs, diffs, and tests). This is not a full formatter for arbitrary user spacing; it emits a consistent shape.

Compiler work next (after surface)

Ordered backlog aligned with docs/30-decisions/32-phase-0-reference-implementation-status.md:

1. MLIR lowering gaps: any remaining unary_ok vs emit holes; cast pairs still rejected at emit; extra binary ops if §06 grows (floored mod, div rounding modes, …); optional native float8 linalg.* where a bridge is slower than a dedicated op.
2. Reduce: prod, argmax, … in reduce_ok + emitter.
3. Types / SMT: refinements R on tensor types and §03-style implication (large); extend requires beyond pairwise = on dims when the spec demands it.
4. Reshape emit: symbolic target dims (dynamic tensor.reshape shape operand or equivalent).
5. Infra: CI workflow when policy allows; exercise toolchain pins on runners.
6. Surface (Phase 7): human-facing syntax and desugaring to this IR — out of scope for the bootstrap compiler until explicitly scheduled.

Last updated: 2026-07-17.