Structural conversion of sequential GraphSpec chains to DAG terms

This module embeds each sequential primitive as a DAG primitive and lowers composition to explicit SSA-style let bindings.

Lowering: sequential chain → DAG term

GraphSpec has two surface syntaxes:

• NN.GraphSpec.Chain: a sequential DSL (Chain + >>>), ideal for pure pipelines.
• NN.GraphSpec.DAG: a general SSA/A-normal-form term language, ideal for sharing/skip connections.

The DAG term language is GraphSpec’s “general graph” core: it is the representation that can express sharing and skip connections.

Chain exists because it is the clearest way to write pipelines, and it has its own direct Spec semantics (Interp.spec) and program translation (Chain.toProgram).

This lowering is still useful whenever you want to embed a sequential pipeline into the DAG world (e.g. to reuse DAG-only tooling, or to keep a single GraphSpec example surface that can export DAG models).

The declarations below provide a structural lowering:

• Chain.toDAGTerm produces a DAG.Term (ps ++ [σ]) τ, i.e. a DAG term whose environment starts with the parameter list ps and ends with the (single) data input σ. Notes:
• The lowering is purely structural: it introduces let1 binders between stages to make the sequential flow explicit in SSA form.
• Each sequential Primitive ps σ τ is embedded as a DAG primitive op with inputs ps ++ [σ]. This embedding is generic: any custom GraphSpec primitive automatically becomes usable in the DAG world.

Lowering internals

The definitions below (primCall and toTerm) implement the structural lowering. The principal entry point is Chain.toDAGTerm.

Primitive embedding: Primitive → DAG.PrimOp

def NN.GraphSpec.LowerToDAG.Primitive.toDAGPrimOp {ps : List Spec.Shape} {σ τ : Spec.Shape} (p : Primitive ps σ τ) : DAG.PrimOp (ps ++ [σ]) τ

Embed a sequential GraphSpec primitive as a DAG primitive op.

The resulting op has input shapes ps ++ [σ] (parameters followed by the data input).

Building well-typed DAG arguments for a primitive call

def NN.GraphSpec.LowerToDAG.primCall {pre ps post extra : List Spec.Shape} {σ τ : Spec.Shape} (p : Primitive ps σ τ) (x : DAG.Term (pre ++ ps ++ post ++ extra) σ) : DAG.Term (pre ++ ps ++ post ++ extra) τ

Lower a unary Primitive application into the DAG term language.

Parameters are read from the middle ps segment of the ambient environment, in the same order as the primitive's parameter ABI, and the final data input is supplied by x.

Chain lowering

def NN.GraphSpec.LowerToDAG.toTerm {pre ps post extra : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) (x : DAG.Term (pre ++ ps ++ post ++ extra) σ) : DAG.Term (pre ++ ps ++ post ++ extra) τ

Lower a sequential Chain to an SSA-style DAG.Term, with parameters read from the environment.

Public API

def NN.GraphSpec.LowerToDAG.Chain.toDAGTerm {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) : DAG.Term (ps ++ [σ]) τ

Lower a sequential Chain to a DAG term with environment ps ++ [σ].