check

Documentation

Overview

Package check implements the ADR 002 §5 "checked program": the pass that sits between the #196 typed AST and the two sibling projections (the #197 resource projection and the #199 execution lowering, internal/execir). Check lowers both projections and exposes the execution IR on Program.Executables.

.agent  ->  typed AST  ->  checked program  ->  { resource projection, execution lowering }
                           (resolved refs · types · effect bound)

Check resolves cross-declaration references, resolves TypeRef names against loaded JSON Schema documents, and computes the actual reachable effect bound for every workflow so the workflow's `effects { }` clause becomes a checked declaration rather than documentation (issue #198).

Deliberate non-goal: this package does NOT reimplement effect-graph traversal. It lowers every file in the compilation unit through the existing internal/lang/lower (issue #197) into one merged *spec.ProjectGraph and calls the existing, unmodified internal/effects.Compute (issue #189) — the same function the YAML ingress path already uses. Two independent effect walkers could only be tested into agreement and would drift the next time either changed; this package makes "the frontend and YAML paths produce identical bounds" true by construction — which in turn requires lowering the WHOLE compilation unit, not just the file under check: a callee classified but never itself lowered would leave effects.Compute walking a resource that is not in the graph.

This package also introduces one new convention with no prior ADR or grammar text: a TypeRef name resolves to a schema file at <SchemaDir>/schemas/<Name>.json. See doc.go comments in types.go for the gradual-typing rules around it (a missing file is untyped; a file that exists but fails to compile is reported, not swallowed).

Index

• type Options
• type Program
  • func Check(f *lang.File, opts Options) (*Program, lang.Diagnostics)

Types

type Options

type Options struct {
	// Project supplies already-loaded sibling YAML resources (agents, tools,
	// policies, other workflows) so a .agent file can reference and interoperate
	// with them. Nil is treated as an empty graph. Check never mutates Project —
	// it computes against a shallow clone.
	Project *spec.ProjectGraph

	// Files supplies other .agent ASTs in the same compilation unit. Every
	// file listed here is lowered, merged into Program.Graph, type-checked,
	// rebound, and effects-clause-checked exactly like f — this is one
	// compilation unit, not f plus context for f. This is the project-wide
	// symbol table internal/lang/lower/lower.go's Options.Workflows doc
	// comment names as this package's replacement.
	Files []*lang.File

	// SchemaDir overrides where TypeRef names resolve to schema files
	// (<SchemaDir>/schemas/<Name>.json). Defaults to the directory of f's own
	// position (f.Pos.File) when empty.
	SchemaDir string
}

Options supplies context Check cannot derive from f alone.

type Program

type Program struct {
	File   *lang.File
	Graph  *spec.ProjectGraph
	Bounds effects.GraphBounds
	// Executables is the execution-IR projection of every workflow in the
	// compilation unit, keyed by workflow name (ADR 002 §5, #199). This is the
	// form control flow (Branch/Loop/Fork) lives in, executable via execir.Interp.
	// Positional workflow: arguments are rebound to real parameter names here
	// (applyExecRebinds), the same rewrite Graph receives.
	//
	// Not yet on a production path: project.LoadProject (#200) runs Check and uses
	// its Graph (the resource projection), but no planner or runner constructs an
	// execir.Program — the loader instead REFUSES control-flow workflows, and the
	// plan-hash fold of execir.Program.Digest (plan.WorkflowSpecHashWithExec) is
	// unused. Wiring these programs onto the engine is the remaining work (with the
	// persistence half of #199, #207). Populated even when diagnostics are present
	// (best-effort, like Graph).
	Executables map[string]*execir.Program
}

Program is the checked program: f plus the resolved graph and effect bound it type/effect-checks against. A non-nil Program is always returned, even when Check reports errors, so a caller can inspect partial results — the returned Diagnostics is the authority on pass/fail via HasErrors (or AsError to get a plain error, nil for a warning-only result). Do not treat a non-empty Diagnostics or a bare error-interface conversion of it as failure on its own — see Diagnostics.AsError.

func Check

func Check(f *lang.File, opts Options) (*Program, lang.Diagnostics)

Check resolves, type-checks, and effect-checks the WHOLE compilation unit (f plus every file in Options.Files) — not just f. Program.Graph is one merged graph holding every file's lowered workflows, and it is documented (and relied on by callers) as an executable projection; type-checking only f while Files' workflows still sit on that same graph would leave a positional workflow: call in a Files-only file with its lowered arg0/arg1 keys never rebound, silently contradicting that contract for exactly the files a caller is least likely to have already checked directly.

The effect bound is computed by lowering EVERY file in the compilation unit (f plus Options.Files) through lower.LowerFile into one merged *spec.ProjectGraph (with Options.Project) and calling effects.Compute on the result — see doc.go for why this package never walks the AST for effects on its own. Lowering only f and merely classifying Options.Files' declarations for callee-kind purposes would leave a cross-file callee's own body out of the graph: effects.Compute would then walk a workflow callee that resolves to nothing (silently contributing no effects — fail-open) or an agent callee that resolves to nothing (contributing Unknown — fail-closed but still not the real grant set). Lowering the whole unit is what makes "the frontend and YAML paths agree on a bound" true when a program spans more than one .agent file.

Check also REWRITES the resource projection it returns: lower.LowerFile keys a positional call argument by raw index (arg0, arg1, ...) because lowering has no symbol table of its own to resolve a callee's declared parameters against. Type-checking a workflow: call does have that information (checkWorkflowArgs), so Check applies the resolved parameter names back onto the already-lowered graph as a second pass (applyRebinds) — otherwise a positional workflow call would type-check clean while Program.Graph still carried a with: map the callee cannot read. This only touches steps this call itself just lowered, never a resource reachable through Options.Project.