Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- **Failure is a compilation state, not a type.** `Analysis\CompilationState` records what became of each source — Certified, Failed or Abandoned — and a failed compiled source carries no type and no evaluation: `CompiledSource::$returns` throws on one, and `Diagnosis::$returns` is `null` for an expression whose root itself failed. There is no marker for a host to be handed, wrap in a composite of its own, or claim back, so the types a host authors are never inspected. `Program`'s constructor refuses any node tree in which something failed, at the cost of one boolean read carried bottom-up by the compilation node.
- **A compilation node is certified, failed or abandoned**, on `CompilationNode::$state`. A certified node carries the type it returns and the extension whose compiler owns it. A failed one is a source the compiler gave up on; it claims neither, and never reaches an analysis, because an analysis is built only for a certified program. An abandoned one stands where a child refused and its compiler caught the refusal and compiled without it — the position exists so paths stay stable across the compilations `diagnose()` makes, and it too claims neither type nor compiler: reading `$returns` or `$extension` throws, and `toArray()` renders `['path' => …, 'source' => …, 'abandoned' => true]`. It is never a failure and never blocks certification.
- **Compiled programs report their input reads.** `Program::$references` lists the declared input keys resolved by successful compilation, including reads reached through definitions, in first-read order without duplicates. Consumers can reuse this compiler-produced fact instead of maintaining a second source-tree walk.
- **Lexically scoped source bodies compile once and run many times.** A host source can persist a `ScopedExpression` with explicit parameter names, compile it through `SourceCompilation::scope()` using types certified from sibling sources, and invoke the resulting `CompiledScopedExpression` through `SourceEvaluation::invoke()`. Each invocation supplies exact local bindings while free symbols continue to resolve through the enclosing program. Locals shadow equal outer names, nested scopes shadow lexically, definitions stay global, and bound parameters stay out of the public expression signature. This gives iterators such as host-owned `any` sources typed, short-circuiting predicate evaluation without adding callbacks or a generic lambda source to the persisted language.
- RFC 0001: Typesafe Axiom (`docs/rfc/0001-typesafe-axiom.md`) — the design record for the statically typed, compiled expression language, shipping as one breaking release; `docs/extending-axiom.md` is the extension guide.
- **Compilation**: `Expression::compile(): Result<Program, TypeMismatch>` type-checks a program once — cycles, unbound symbols, unresolvable or ambiguous operators, dead comparisons, non-exhaustive matches, false ascriptions all refuse with named diagnostics — and returns a certified, callable `Program` (`$program->returns` is the inferred type; `$program($bindings)` runs the boundary and then evaluates). A compiled program embeds its operator resolutions and performs **no runtime type dispatch**; definitions compile once and evaluate lazily, memoized per invocation (`Runtime`). `Expression::infer()`/`check()` are conveniences over `compile()`.
- Invocation-scoped execution observation: `Program::call()` accepts an optional `Execution\Observer`; every compiled source node emits ordered `Entered`, `Annotated`, `Exited`, or `Threw` events carrying its source class and certified return type. Observers are never stored on persistable sources or retained by programs, while host source compilers participate automatically through `CompiledSource` composition and may add domain annotations through `SourceEvaluation`.
Expand Down
2 changes: 2 additions & 0 deletions CONTEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,12 @@
## Persistence and compilation

- A **Source** is a data-only node in a persistable program description. It may contain other sources and scalar/domain data, but no live service collaborators.
- A **ScopedExpression** is a persistable Source body plus the root symbol names its owning Source binds. It is not itself a Source and has no type until that owner's source compiler supplies parameter types through `SourceCompilation::scope()`. The compiler descends the body in that nested scope, resolves the named parameters locally, and records every other symbol as a lexical read from the enclosing expression.
- A **Predicate** is the propositional projection of a Source: core `&&` becomes `AllOf`, core `||` becomes `AnyOf`, and every other Source remains an opaque `Atom`. `PredicateRelations::implies()` is a conservative proof over that closed vocabulary; an unproved implication is not a disproof. `Predicate::partiallyEvaluate()` propagates host-provided atom values and preserves undecided structure as a residual predicate; it is value-level reasoning, not a promise to preserve runtime evaluation of discarded atoms or original Source syntax. Hosts retain the meaning and totality of their atoms and why one predicate must imply another.
- A **source compiler** is a compile-time adapter owning one exact `Source` class: the callback that returns the class's `CompiledSource`. Host extensions register theirs through `Extension::sourceCompilers()`; the core language's nodes are registered by `Dialect::core()` (`CoreSourceCompilers`) through the same map, so every node compiles through one registered rule and claiming an already-owned class is the same loud error either way.
- A **CompiledSource** is in one of two states. A **certified** one couples one certified return type to a composable evaluation. A **failed** one stands for a source whose compilation was refused, with that refusal recorded as a diagnostic; it carries no type and no evaluation — reading `$returns` throws, `failed()` answers the question instead, and every capability that judges or claims over a child absorbs it rather than asking. Failure is a state compilation records (`CompilationState`), never a type: a `CompilationNode` is Certified, Failed or Abandoned, and `Program` certifies by reading that state bottom-up rather than inspecting any type. Its ordinary operations make present-value mapping, absence-aware mapping, child composition, and bound-operation application available without exposing `CompiledNode`, `Runtime`, or the internal `Result<Option<...>>` channel. Present-value mapping derives an optional result type whenever an input is optional; propagating absence can never mint a non-optional claim.
- **SourceCompilation** is the straight-line capability passed to a source compiler. It compiles child sources in the current type environment, resolves symbols, binds typed infix and prefix operations from the composed dialect, types embedded PHP values literal-first, and constructs `CompiledSource` values. Nested refusals automatically return through `Expression::compile()`; source compiler callbacks do not compose compilation `Result` values themselves.
- A **CompiledScopedExpression** is a ScopedExpression body compiled once in a nested lexical environment through the owning compilation's dialect. Its source compiler invokes it repeatedly through `SourceEvaluation::invoke()` with local values already certified by compiled parents. Invocations share the enclosing runtime's inputs, memoized definitions and execution observation while opaque scope identities keep equal local and outer symbol names distinct.
- A **CompilationAnalysis** is the data-only explanation emitted by the same successful compilation that builds a `Program`. Its source graph carries certified return types and source-compiler ownership; its operator selections carry operand and return types plus the stable identity, implementation, and extension of the rule that won. It contains no evaluations or captured collaborators and is not a persistence format for sources. Serializable exports redact literal values by default.
- A **Program** is the ephemeral compiled artifact. Its evaluation closures may capture live services from extensions, so programs are executed and sources are persisted.
- An **execution observer** belongs to one `Program` invocation. Core emits an ordered lifecycle for every compiled source node; tracing and telemetry packages interpret those events. Observers are never stored on sources, expressions, or programs.
Expand Down
5 changes: 5 additions & 0 deletions composer.json
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,11 @@
"php": "8.4.0"
}
},
"extra": {
"branch-alias": {
"dev-STRAT-733-subprogram": "0.6.x-dev"
}
},
"minimum-stability": "dev",
"prefer-stable": true
}
82 changes: 79 additions & 3 deletions docs/extending-axiom.md
Original file line number Diff line number Diff line change
Expand Up @@ -854,9 +854,85 @@ Catch only domain exceptions your callback owns. A broad `catch (RuntimeExceptio

`custom()` is an advanced escape hatch for lazy control flow and annotations. It cannot compile new sources at runtime and does not expose `Runtime`, `Result`, or `Option`.

### Symbols Must Stay Visible
### Step 9: Compile a Lexically Scoped Body

When a host source owns a symbol reference, store the actual `SymbolSource` as a public persisted child and compile it through `symbol()`:
A host source may own a body that runs repeatedly with a value supplied by another child. Persist that body as a `ScopedExpression`, so its compiler can resolve the explicit parameter names in a nested lexical scope:

```php
final readonly class AnySource implements Source
{
public function __construct(
public Source $items,
public ScopedExpression $predicate,
) {}
}
```

The binder is not a reserved `item` convention. The author chooses it, and free symbols remain ordinary lexical references:

```php
new AnySource(
new SymbolSource('quotes'),
new ScopedExpression(
['candidate'],
new InfixExpression(
new MemberAccessSource(new SymbolSource('candidate'), 'premium'),
'<',
new SymbolSource('budget'),
),
),
);
```

Here `candidate` is local to the predicate and `budget` comes from the enclosing expression. Compile the collection first, because its element type supplies the local parameter's type. The predicate compiles once; invocation only supplies a new binding:

```php
private function compileAny(
AnySource $source,
SourceCompilation $compilation,
): CompiledSource {
$items = $compilation->child($source->items, 'items');
$itemsType = PresentType::of($items->returns);

if (!$itemsType instanceof ListType) {
$compilation->reject('Any needs a list.');
}

if (count($source->predicate->parameters) !== 1) {
$compilation->reject('Any needs exactly one predicate parameter.');
}

$parameter = $source->predicate->parameters[0];
$predicate = $compilation
->scope(
$source->predicate,
[$parameter => $itemsType->type],
'predicate',
)
->expectPresent(new BooleanType());

return $compilation->custom(
new BooleanType(),
static function (SourceEvaluation $evaluation) use ($items, $parameter, $predicate): bool {
foreach ($evaluation->value($items) ?? [] as $item) {
if ($evaluation->invoke($predicate, [$parameter => $item]) === true) {
return true;
}
}

return false;
},
);
}
```

The body compiles through the same dialect in a nested lexical environment. Its parameters shadow equal outer names; every other symbol resolves through the enclosing inputs and definitions. Repeated invocations share definition memoization and observation with the enclosing runtime, while opaque scope identities ensure a local name cannot change what an already-compiled outer definition reads.

The supplied local values skip a redundant public-boundary admission because the owning compiler obtained them from certified compiled parents. `scope()` certifies Axiom semantics only: a host that projects the same persisted language into another runtime still owns that portability policy and should admit the body before compiling it here.

### Compile Owned Symbols Explicitly

When a host source owns a symbol reference, compile it through `symbol()`:

```php
use Superscript\Axiom\Sources\SymbolSource;
Expand All @@ -874,7 +950,7 @@ private function compileNamedValue(
}
```

This preserves ordinary declared-input, definition, and per-invocation memoization semantics. More importantly, parameter discovery and definition-cycle analysis can see the dependency. Constructing a new `SymbolSource` from a hidden string inside the compiler is refused because the stored source tree would no longer describe the program's real dependencies.
This preserves ordinary declared-input, definition, and per-invocation memoization semantics. Symbol resolution itself records the dependency for parameter and definition-cycle analysis, so property visibility does not participate. A compiler may derive a `SymbolSource` from its persisted data when that is the source's intended description; persisting the symbol directly is a domain-model choice, not an analysis requirement.

The extension map simply grows as the package gains source kinds:

Expand Down
Loading
Loading