From 66053c9e83e14560c69d223a49475df64678485d Mon Sep 17 00:00:00 2001 From: Robert van Steen Date: Sun, 16 Aug 2026 15:23:20 +0200 Subject: [PATCH] Rewrite stored source under proved obligations Add Superscript\Axiom\Rewrite: a rule set applied bottom-up over an immutable Source tree, returning the new tree plus a report of every site a rule fired, every site a rule was refused, and every shape the walk could not see inside. A rule owns matching and replacement for the exact classes it visits and writes no traversal; descent belongs to the toolkit, is exhaustive over the core node set by law, and joins host arms through Extension::sourceDescenders(). A class no extension claims is an opaque leaf: never descended, never rewritten, always reported. Nothing is applied that was not proved. Every replacement compiles against the expression's own scope and must certify the type it replaces, or refuse identically; a rule may claim verdict preservation, checked against a host bindings corpus. A broken obligation refuses that one site and reports it. Co-Authored-By: Claude Fable 5 --- CHANGELOG.md | 3 + CONTEXT.md | 1 + README.md | 18 + docs/rewriting.md | 240 ++++++++++ src/Extension.php | 20 + src/Rewrite/ArrayBindingsCorpus.php | 21 + src/Rewrite/BindingsCorpus.php | 20 + src/Rewrite/CoreSourceDescenders.php | 153 +++++++ src/Rewrite/Descent.php | 43 ++ src/Rewrite/Describes.php | 26 ++ src/Rewrite/Obligation.php | 18 + src/Rewrite/ObligationVerdict.php | 49 ++ src/Rewrite/OpaqueSource.php | 35 ++ src/Rewrite/Preservation.php | 38 ++ src/Rewrite/RewriteOutcome.php | 14 + src/Rewrite/RewriteRecord.php | 46 ++ src/Rewrite/RewriteReport.php | 47 ++ src/Rewrite/RewriteRule.php | 61 +++ src/Rewrite/RewriteRun.php | 43 ++ src/Rewrite/RewriteSite.php | 69 +++ src/Rewrite/RewriteWalk.php | 151 ++++++ src/Rewrite/Rewriter.php | 89 ++++ src/Rewrite/Rules/RemoveDoubleNegation.php | 87 ++++ src/Rewrite/Rules/RemoveRedundantDefault.php | 55 +++ src/Rewrite/SourceDescenders.php | 59 +++ src/Rewrite/SourcePath.php | 52 +++ src/Rewrite/TypePreservation.php | 61 +++ src/Rewrite/VerdictPreservation.php | 76 ++++ .../Rewrite/CoreDescentExhaustivenessTest.php | 84 ++++ tests/Rewrite/Fixtures/BoxExtension.php | 41 ++ tests/Rewrite/Fixtures/BoxSource.php | 19 + tests/Rewrite/Fixtures/StubRule.php | 46 ++ tests/Rewrite/ObligationTest.php | 221 +++++++++ tests/Rewrite/RewriterTest.php | 430 ++++++++++++++++++ .../Rules/RemoveDoubleNegationTest.php | 155 +++++++ .../Rules/RemoveRedundantDefaultTest.php | 105 +++++ tests/Rewrite/SourceDescendersTest.php | 67 +++ 37 files changed, 2763 insertions(+) create mode 100644 docs/rewriting.md create mode 100644 src/Rewrite/ArrayBindingsCorpus.php create mode 100644 src/Rewrite/BindingsCorpus.php create mode 100644 src/Rewrite/CoreSourceDescenders.php create mode 100644 src/Rewrite/Descent.php create mode 100644 src/Rewrite/Describes.php create mode 100644 src/Rewrite/Obligation.php create mode 100644 src/Rewrite/ObligationVerdict.php create mode 100644 src/Rewrite/OpaqueSource.php create mode 100644 src/Rewrite/Preservation.php create mode 100644 src/Rewrite/RewriteOutcome.php create mode 100644 src/Rewrite/RewriteRecord.php create mode 100644 src/Rewrite/RewriteReport.php create mode 100644 src/Rewrite/RewriteRule.php create mode 100644 src/Rewrite/RewriteRun.php create mode 100644 src/Rewrite/RewriteSite.php create mode 100644 src/Rewrite/RewriteWalk.php create mode 100644 src/Rewrite/Rewriter.php create mode 100644 src/Rewrite/Rules/RemoveDoubleNegation.php create mode 100644 src/Rewrite/Rules/RemoveRedundantDefault.php create mode 100644 src/Rewrite/SourceDescenders.php create mode 100644 src/Rewrite/SourcePath.php create mode 100644 src/Rewrite/TypePreservation.php create mode 100644 src/Rewrite/VerdictPreservation.php create mode 100644 tests/Rewrite/CoreDescentExhaustivenessTest.php create mode 100644 tests/Rewrite/Fixtures/BoxExtension.php create mode 100644 tests/Rewrite/Fixtures/BoxSource.php create mode 100644 tests/Rewrite/Fixtures/StubRule.php create mode 100644 tests/Rewrite/ObligationTest.php create mode 100644 tests/Rewrite/RewriterTest.php create mode 100644 tests/Rewrite/Rules/RemoveDoubleNegationTest.php create mode 100644 tests/Rewrite/Rules/RemoveRedundantDefaultTest.php create mode 100644 tests/Rewrite/SourceDescendersTest.php diff --git a/CHANGELOG.md b/CHANGELOG.md index e813c44..2c0bbf9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] ### Added +- **A rewriting toolkit for stored source** (`Superscript\Axiom\Rewrite`, documented in `docs/rewriting.md`). `Rewriter::rewrite(Expression): RewriteRun` applies a set of `RewriteRule`s bottom-up over an immutable source tree and returns the new tree plus a report of every site a rule fired, every site a rule was refused, and every shape the walk could not see inside; report-only is the same run with the tree ignored. A rule owns matching and replacement for the exact `Source` classes it visits and writes no traversal — descent is the toolkit's, dispatch is one array lookup per node, and untouched subtrees come back as the same instance, so `RewriteRun::$changed` is answered by identity. Core node descent is exhaustive by law (a test reflects over `src/Sources` and fails on a class without an arm); host shapes register through `Extension::sourceDescenders()` with the exact, unranked ownership `sourceCompilers()` already uses. **A class no extension claims is an opaque leaf** — never descended, never rewritten, and named in the report rather than silently skipped, so a forgotten arm cannot read as a clean tree. + - **Nothing is applied that was not proved.** Every replacement is compiled against the expression's own dialect, definitions and declarations, and must certify the same type as what it replaces — or refuse identically, so a rewrite is never what changes the diagnostic an author reads. A rule may claim more: `Preservation::Verdict` runs both programs over a host `BindingsCorpus` and compares answers case by case, with disagreements naming the case. A broken obligation refuses that one site and reports it; a claim the run has no oracle for is reported *unchecked*, which neither blocks a rewrite nor counts as evidence for one. Subtrees compile standalone in the whole expression's scope exactly because the language has no binding form. + - `Rules\RemoveDoubleNegation` is the reference rule: `!!x` becomes `x` for either spelling of core negation. It is neutral because core's `!` is the only row for its symbol — Boolean in, Boolean out — so a `!!x` that compiles has an operand of `Boolean` or, lifted, `Boolean?`, and on both the operation is total and involutive. `!!count` over a Number is refused rather than simplified: the original never compiled, and the replacement would be a certified Number program nobody wrote. `Rules\\RemoveRedundantDefault` is the other shape a rule takes — one whose applicability matching cannot settle: `x ?? 0` is the identity exactly when `x` can never be absent, which is a fact about types, so the rule proposes the removal everywhere and type preservation decides site by site (`Number` against `Number?` refuses the ones absence can reach). - **Declarations and records now use one required-by-default property model.** `Expression::$declarations` is a `RecordType` (array input remains shorthand), and every bare property must exist. `new Optional(new NumberType())` permits a property to be omitted without turning `Optional` into a `Type`; `OptionType` independently permits an explicitly supplied absent value. This makes all four useful states representable: required `T`, required `Option`, optional `T`, and optional `Option`. Missing optional properties remain missing during record coercion rather than being canonicalized to `null`. - **Input paths are structural.** `SymbolSource` names only root symbols and `MemberAccessSource` traverses one record property per node; empty and dotted member names are rejected. Declarations and bindings are nested records; flat dotted namespaces and the namespace argument on `SymbolSource` are removed. Compiler-resolved reads remain `ReferencePath` values through programs and diagnostics, serialize as `{"root":"customer","properties":["turnover"]}`, and render as `customer.turnover` only when `describe()` is requested. Compilation projects the declaration record to only the paths the program reads while preserving required/optional qualifiers at every level. - **Compilation that reports everything wrong, not just the first thing.** `Expression::diagnose(): Diagnosis` compiles for the sake of what compilation learns: every refusal in the expression, the access paths it read even through the parts that refuse, the root type, and — when nothing refused — the certified `Program`, through `Diagnosis::program(): Result>`. `mystery > 1000 && postcode == 'SW1'` with `mystery` undeclared reports one diagnostic (the unbound symbol), still type-checks the right-hand comparison, and still reports the `mystery` and `postcode` references — where `compile()` reports the unbound symbol and stops. `compile()` is one attempt of the same walk and behaves exactly as before: its refusal is the diagnosis' first diagnostic, same message, same path. diff --git a/CONTEXT.md b/CONTEXT.md index f3d83bc..08cd02b 100644 --- a/CONTEXT.md +++ b/CONTEXT.md @@ -9,6 +9,7 @@ - **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 **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. +- A **rewrite rule** owns matching and replacement for exact `Source` classes; **descent** — reaching a node's children and rebuilding it around new ones — belongs to the rewriter, registered per exact class the way source compilers are (`Extension::sourceDescenders()`), so structural knowledge lives in rules and arms and never as a method on `Source`. A class with no arm is an **opaque leaf**: never descended, never rewritten, always reported. A replacement is applied only once it discharges its **preservation obligations** — certified type always, runtime verdicts when the host supplies a bindings corpus — and a broken one refuses that site rather than the run. Rewriting is a tool over stored sources: it runs before compilation and no compiled artifact knows about it. - 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. Use “source compiler” for this seam. Do not call it a resolver: runtime source resolution and its delegating registry were removed by the compilation pivot. diff --git a/README.md b/README.md index a391f0d..50dca9f 100644 --- a/README.md +++ b/README.md @@ -18,6 +18,7 @@ The design principle is **compile, then trust**: `Expression::compile()` type-ch - [Operators](#operators) - [Execution Observation](#execution-observation) - [Extending Axiom](#extending-axiom) +- [Rewriting Stored Source](#rewriting-stored-source) - [Development](#development) - [License](#license) @@ -538,6 +539,23 @@ Use **[the extension guide](docs/extending-axiom.md)** for a progressive tutoria | Add a data source | `Extension::sourceCompilers()` plus composable `CompiledSource` values; sources stay data-only | Host sources | | Add match pattern kinds | (reserved: an `Extension::matchers()` hook can be added without breaking implementors) | — | | Prove your rules honest | the totality harness + admission-honesty law patterns | Testing your extension | +| Rewrite a stored corpus | `Extension::sourceDescenders()` plus `RewriteRule` implementations | [Rewriting Stored Source](docs/rewriting.md) | + +## Rewriting Stored Source + +A host that stores expressions eventually has to change them in bulk. `Rewrite\Rewriter` applies a set of `RewriteRule`s bottom-up over an immutable source tree and returns the new tree with a report of what it did: + +```php +$run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression); + +$run->report->describe(); // dry run: read this, take nothing +$run->changed; // false when every subtree came back identical +$run->source; // the tree to store +``` + +Nothing is applied that was not proved. Every replacement is compiled against the expression's own declarations and must certify the same type as what it replaces — or refuse identically; a rule may also claim verdict preservation, which the run checks against a host `BindingsCorpus`. A broken obligation refuses that one site and reports it, because a fold that type-checks can still invert the meaning of a condition. A node class with no descent arm is an opaque leaf: never descended, never rewritten, and always named in the report. + +See **[Rewriting Stored Source](docs/rewriting.md)** for rules, descent, obligations, and the report. ## Development diff --git a/docs/rewriting.md b/docs/rewriting.md new file mode 100644 index 0000000..cebbe38 --- /dev/null +++ b/docs/rewriting.md @@ -0,0 +1,240 @@ +# Rewriting Stored Source + +- [Why](#why) +- [A Worked Example](#a-worked-example) +- [Rules](#rules) +- [Descent, and the Opaque-Leaf Policy](#descent-and-the-opaque-leaf-policy) +- [Obligations](#obligations) +- [The Report](#the-report) +- [Writing a Rule](#writing-a-rule) +- [When the Rule Cannot Decide](#when-the-rule-cannot-decide) +- [What Is Not a Source Rewrite](#what-is-not-a-source-rewrite) + +## Why + +A host that stores expressions accumulates a corpus it did not write all at once: thousands of conditions authored over years, against a language that has since grown a better spelling for something. Editing them by hand is a migration nobody finishes; editing them with a script is a migration nobody can prove. + +This is the toolkit for the middle path: a rule set applied to stored source, bottom-up over an immutable tree, where every replacement must discharge an obligation before it is applied, and everything the run did — and everything it could not see — is reported. + +## A Worked Example + +An author wrote a double negation, and the corpus has 400 more like it: + +```php +use Superscript\Axiom\Expression; +use Superscript\Axiom\Rewrite\{ArrayBindingsCorpus, Rewriter, VerdictPreservation}; +use Superscript\Axiom\Rewrite\Rules\RemoveDoubleNegation; +use Superscript\Axiom\Sources\{InfixExpression, StaticSource, SymbolSource, UnaryExpression}; +use Superscript\Axiom\Types\{BooleanType, NumberType, OptionType, Optional}; + +$not = fn ($source) => new UnaryExpression('!', $source); + +$expression = new Expression( + source: new InfixExpression( + $not($not(new InfixExpression(new SymbolSource('roof'), '>', new StaticSource(0.25)))), + '&&', + $not($not(new SymbolSource('flag'))), + ), + declarations: [ + 'roof' => new Optional(new OptionType(new NumberType())), + 'flag' => new BooleanType(), + ], +); + +$rewriter = new Rewriter( + [new RemoveDoubleNegation()], + obligations: [new VerdictPreservation(new ArrayBindingsCorpus([ + 'answered' => ['roof' => 0.3, 'flag' => true], + 'unanswered' => ['flag' => false], + ]))], +); + +$run = $rewriter->rewrite($expression); +``` + +Read the report first and take nothing — that is the dry run: + +``` +applied axiom.rewrite.remove-double-negation at $.left: !!(roof > 0.25) => roof > 0.25 + type preservation upheld: both compile to Boolean? + verdict preservation upheld: 2 corpus case(s) agree +applied axiom.rewrite.remove-double-negation at $.right: !!flag => flag + type preservation upheld: both compile to Boolean + verdict preservation upheld: 2 corpus case(s) agree +``` + +Then take the tree: + +```php +$run->changed; // true +$run->source->describe(); // (roof > 0.25) && flag +$run->expression(); // the same dialect, definitions, declarations and boundary over the new tree +``` + +There is no mode flag: report-only is this same run with the tree ignored. + +Now the same rule against a stored expression that never compiled — `!!count` where `count` is a Number: + +``` +refused axiom.rewrite.remove-double-negation at $: !!count => count + type preservation broken: the original refuses and the replacement compiles: [!] expects Boolean; got Number. + Number is not assignable to Boolean. + verdict preservation unchecked: the run was given no oracle for this claim +``` + +`$run->changed` is `false` and `$run->source` is the very tree that went in. Simplifying here would have handed back a certified Number program in place of a refusal — a program the author never wrote and the checker never blessed. One site is refused; the rest of the run proceeds. + +## Rules + +A rule owns matching and replacement for exact source classes: + +```php +interface RewriteRule +{ + public function identifier(): string; + + /** @return non-empty-list> */ + public function visits(): array; + + public function rewrite(Source $source): ?Source; // null = nothing to do here + + /** @return list */ + public function preserves(): array; +} +``` + +Structural knowledge lives here rather than on `Source`, and descent lives in the toolkit. A `Source` is data a host persists; every method the language puts on it is a method every host node must implement forever. A rule that only rewrites `!!x` needs to know about exactly two node shapes, and writes no traversal at all. + +Dispatch is by exact class, the same ownership model source compilers use: rules are indexed by the classes they visit, so a node costs one array lookup however many rules the run carries. A rule listing a parent class is never offered a subclass. + +At each node, rules registered for its class are offered in registration order until one takes it. A rule that returns `null` is passed over; a rule whose replacement breaks an obligation is recorded refused and the next rule is asked; the first sound replacement wins and ends the visit. + +## Descent, and the Opaque-Leaf Policy + +The walk is bottom-up: a node's children are rewritten, the node is rebuilt around whatever came back, and only then are rules offered the rebuilt node. A rule therefore always sees the shape that will actually be stored, and one pass collapses a nest — `!!!!x` reduces at every level on the way out. + +**Structural sharing.** A node whose children all came back identical is returned as-is, so an untouched subtree is the same instance in the new tree. `$run->changed` is answered by identity, not comparison. + +**Core shapes** are the toolkit's own: `CoreSourceDescenders` has an arm per node class, and an exhaustiveness law reflects over `src/Sources` and fails if a class exists without one. + +**Host shapes** register through the extension a package already ships: + +```php +final class BoxExtension extends Extension +{ + public function sourceDescenders(): array + { + return [BoxSource::class => $this->descend(...)]; + } + + private function descend(BoxSource $source, Descent $descent): Source + { + $inner = $descent->child($source->inner, 'inner'); + + return $inner === $source->inner ? $source : new BoxSource($inner); + } +} + +$rewriter = new Rewriter($rules, SourceDescenders::core()->with(new BoxExtension())); +``` + +An arm asks for each child by the property holding it — that name is the path segment the report prints — and returns the same instance when no child moved. Ownership is exact and unranked: two extensions claiming one class is a configuration error. + +**A class no extension claims is an opaque leaf.** It is never descended, never rewritten — not even by a rule naming its own class, because a rule cannot be trusted to rebuild a shape the toolkit cannot take apart — and it is *reported*: + +``` +opaque Acme\Sources\LookupSource at $.right: LookupSource +``` + +Silence would be the dangerous answer. A host that adds a source class and forgets its descent arm would read "no rewrites needed" as "nothing to do" for as long as the omission lasted. + +## Obligations + +A rule declares what it preserves; the run checks what it can. + +| Preservation | Oracle | When | +| --- | --- | --- | +| `CertifiedType` | compile both subtrees in the expression's declaration scope | always, whether or not the rule claims it | +| `Verdict` | run both programs over a `BindingsCorpus` and compare answers | when the run is given a `VerdictPreservation` | + +Both subtrees are compiled standalone *in the whole expression's scope*, which is exact rather than approximate because the language has no binding form: no node introduces a name for its children, so a subtree reads the same environment wherever it sits. + +Type preservation demands the same certified type — or the same refusal, since neither tree can then run and a rewrite must not be what changes the diagnostic an author reads. + +Verdict preservation is evidence, not proof: only the host knows what its programs are fed, and a corpus that never exercises a branch says nothing about it. Its cases are labelled, because a disagreement has to be reproducible: + +``` +verdict preservation broken: case [zero]: the original answers error(Division by zero) and the replacement value(5) +``` + +A verdict comes in three states, and the report keeps them apart: **upheld** (checked, and it holds), **broken** (checked, and it does not — the site is refused), and **unchecked** (no oracle was supplied, so nothing is known either way). Unchecked never blocks a rewrite and never counts as evidence for one. + +## The Report + +```php +$run->report->applied(); // list: rule, path, before, after, verdicts +$run->report->refused(); // the same, for replacements an obligation broke +$run->report->opaque; // list: path, class, describe +$run->report->describe(); // all of it, as text +``` + +Paths are property-named: `$.left.operand`, `$.arms[1].expression`. That is deliberately not the `$.children[0].node` language compilation failures and analyses speak — those number the children a *compiler* recorded, and a compiler records what it needs (a wildcard arm records no pattern child at all), so the same arm sits at a different index depending on which patterns precede it. A coordinate into stored source has to name the same node before anything is compiled. + +## Writing a Rule + +`RemoveDoubleNegation` is the reference. What makes it sound is worth copying, more than the code is: + +```php +public function rewrite(Source $source): ?Source +{ + if (! $source instanceof UnaryExpression || ! $this->negates($source->operator)) { + return null; + } + + $operand = $source->operand; + + if (! $operand instanceof UnaryExpression || ! $this->negates($operand->operator)) { + return null; + } + + return $operand->operand; +} +``` + +The neutrality argument is about the *dialect*, not the shape. Core's `!` is the only row for that symbol: it takes Boolean and returns Boolean. So a `!!x` that compiles at all has an `x` of `Boolean` or, through the resolver's lift, `Boolean?`. On `Boolean`, `!` is total and involutive. On `Boolean?` the resolver lifts that same row, and lifting is functorial — absence propagates through each negation untouched, so `!!` is the lift of `!∘!`, the identity. Every operand type the rewrite can meet is one it is neutral on. + +Note what the argument rests on, and say so in the rule: a host is free to register `!` over its own type and make it something other than an involution, so the spellings are a constructor argument (`new RemoveDoubleNegation(['!'])`) rather than a constant. The obligations then check what the argument assumed rather than trusting it — which is the point. A fold that type-checks can still invert the meaning of a condition, and a rewrite nobody proved is a rewrite nobody should store. + +## When the Rule Cannot Decide + +`RemoveRedundantDefault` is the other shape a rule takes: one whose applicability is not decided by matching at all. + +A `DefaultValue` over a source that can never be absent is already the identity — the compiler returns the inner compiled source untouched, default and all — so the node is noise in stored source, and it reads as if absence were possible where it is not. But whether the inner source can be absent is a fact about *types*, and no amount of looking at the tree settles it. + +So the rule proposes the removal everywhere and lets the obligation settle it: + +```php +public function rewrite(Source $source): ?Source +{ + return $source instanceof DefaultValue ? $source->source : null; +} +``` + +Over an optional inner, `x ?? 0` certifies `Number` while `x` certifies `Number?`; the types differ and the site is refused. Over a definite inner, both certify the same type — necessarily, since they compile to the same node — and the rewrite is taken. In `amount ?? 1 ?? 0` with `amount` optional, the inner default — the one absence can actually reach — is refused, and the outer one, which never fires, is removed: + +``` +refused axiom.rewrite.remove-redundant-default at $.source: amount ?? 1 => amount + type preservation broken: the original compiles to Number and the replacement to Number? + verdict preservation unchecked: the run was given no oracle for this claim +applied axiom.rewrite.remove-redundant-default at $: amount ?? 1 ?? 0 => amount ?? 1 + type preservation upheld: both compile to Number + verdict preservation unchecked: the run was given no oracle for this claim +``` + +Removing the node does change what an execution observer sees — the `default` label and its annotations go with it. That is a change to the program's trace, not to what it answers. + +## What Is Not a Source Rewrite + +A migration only becomes a rewrite rule once both the old and new shapes are representable as `Source` trees. Where a language change removed the old shape from the node set, there is nothing for a rule to match: the old form cannot be hydrated into any `Source` at all, and the migration belongs in the host's deserializer, before a tree exists. + +The namespaced-symbol migration is exactly that case. `SymbolSource` no longer carries a namespace, and its constructor rejects a dotted name outright, so stored `{"name": "turnover", "namespace": "customer"}` has no `Source` to become except the one the host's hydration chooses — `MemberAccessSource(SymbolSource('customer'), 'turnover')`. Reach for this toolkit for changes *within* the node set; reach for the wire format for changes *to* it. diff --git a/src/Extension.php b/src/Extension.php index 2343ebf..1b4dbd1 100644 --- a/src/Extension.php +++ b/src/Extension.php @@ -100,4 +100,24 @@ public function sourceCompilers(): array { return []; } + + /** + * Exact host Source class → how to descend into it and rebuild it, for + * {@see \Superscript\Axiom\Rewrite\Rewriter}. Registration mirrors + * {@see sourceCompilers()} — exact ownership, no precedence — so one + * package declares both how its node compiles and how a rewrite reaches + * through it, and the two cannot end up in different places. A class no + * extension claims is an opaque leaf: never descended, never rewritten, + * and named in the run's report. + * + * An arm receives its source and a {@see \Superscript\Axiom\Rewrite\Descent}, + * asks for each child by the property holding it, and returns the same + * instance when no child moved. + * + * @return array, callable(Source, \Superscript\Axiom\Rewrite\Descent): Source> + */ + public function sourceDescenders(): array + { + return []; + } } diff --git a/src/Rewrite/ArrayBindingsCorpus.php b/src/Rewrite/ArrayBindingsCorpus.php new file mode 100644 index 0000000..5694539 --- /dev/null +++ b/src/Rewrite/ArrayBindingsCorpus.php @@ -0,0 +1,21 @@ +> $cases */ + public function __construct(private array $cases) {} + + /** @return iterable> */ + public function cases(): iterable + { + return $this->cases; + } +} diff --git a/src/Rewrite/BindingsCorpus.php b/src/Rewrite/BindingsCorpus.php new file mode 100644 index 0000000..a5ffd0d --- /dev/null +++ b/src/Rewrite/BindingsCorpus.php @@ -0,0 +1,20 @@ +> label => bindings */ + public function cases(): iterable; +} diff --git a/src/Rewrite/CoreSourceDescenders.php b/src/Rewrite/CoreSourceDescenders.php new file mode 100644 index 0000000..90de9d9 --- /dev/null +++ b/src/Rewrite/CoreSourceDescenders.php @@ -0,0 +1,153 @@ +, callable(Source, Descent): Source> + */ + public static function sources(): array + { + /** @var array, callable(Source, Descent): Source> */ + return [ + StaticSource::class => self::leaf(...), + SymbolSource::class => self::leaf(...), + Coerce::class => self::coerce(...), + Ascription::class => self::ascription(...), + DefaultValue::class => self::defaultValue(...), + MemberAccessSource::class => self::memberAccess(...), + UnaryExpression::class => self::unary(...), + InfixExpression::class => self::infix(...), + MatchExpression::class => self::matchExpression(...), + ]; + } + + /** + * @return array, callable(MatchPattern, Descent): MatchPattern> + */ + public static function patterns(): array + { + /** @var array, callable(MatchPattern, Descent): MatchPattern> */ + return [ + WildcardPattern::class => self::leafPattern(...), + LiteralPattern::class => self::leafPattern(...), + ExpressionPattern::class => self::expressionPattern(...), + ]; + } + + /** A node with no source children: there is nothing under it to rewrite. */ + private static function leaf(Source $source, Descent $descent): Source + { + return $source; + } + + private static function leafPattern(MatchPattern $pattern, Descent $descent): MatchPattern + { + return $pattern; + } + + private static function coerce(Coerce $source, Descent $descent): Source + { + $inner = $descent->child($source->source, 'source'); + + return $inner === $source->source ? $source : new Coerce($source->type, $inner); + } + + private static function ascription(Ascription $source, Descent $descent): Source + { + $inner = $descent->child($source->source, 'source'); + + return $inner === $source->source ? $source : new Ascription($source->type, $inner); + } + + private static function defaultValue(DefaultValue $source, Descent $descent): Source + { + $inner = $descent->child($source->source, 'source'); + + return $inner === $source->source ? $source : new DefaultValue($inner, $source->default); + } + + private static function memberAccess(MemberAccessSource $source, Descent $descent): Source + { + $object = $descent->child($source->object, 'object'); + + return $object === $source->object ? $source : new MemberAccessSource($object, $source->property); + } + + private static function unary(UnaryExpression $source, Descent $descent): Source + { + $operand = $descent->child($source->operand, 'operand'); + + return $operand === $source->operand ? $source : new UnaryExpression($source->operator, $operand); + } + + private static function infix(InfixExpression $source, Descent $descent): Source + { + $left = $descent->child($source->left, 'left'); + $right = $descent->child($source->right, 'right'); + + return $left === $source->left && $right === $source->right + ? $source + : new InfixExpression($left, $source->operator, $right); + } + + private static function matchExpression(MatchExpression $source, Descent $descent): Source + { + $subject = $descent->child($source->subject, 'subject'); + $arms = []; + $moved = $subject !== $source->subject; + + foreach ($source->arms as $index => $arm) { + $rewritten = $descent->arm($arm, sprintf('arms[%d]', $index)); + $moved = $moved || $rewritten !== $arm; + $arms[] = $rewritten; + } + + return $moved ? new MatchExpression($subject, $arms) : $source; + } + + private static function expressionPattern(ExpressionPattern $pattern, Descent $descent): MatchPattern + { + $inner = $descent->child($pattern->source, 'source'); + + return $inner === $pattern->source ? $pattern : new ExpressionPattern($inner); + } +} diff --git a/src/Rewrite/Descent.php b/src/Rewrite/Descent.php new file mode 100644 index 0000000..5bbf05c --- /dev/null +++ b/src/Rewrite/Descent.php @@ -0,0 +1,43 @@ +walk->source($source, $this->path->child($segment)); + } + + public function pattern(MatchPattern $pattern, string $segment): MatchPattern + { + return $this->walk->pattern($pattern, $this->path->child($segment)); + } + + public function arm(MatchArm $arm, string $segment): MatchArm + { + return $this->walk->arm($arm, $this->path->child($segment)); + } +} diff --git a/src/Rewrite/Describes.php b/src/Rewrite/Describes.php new file mode 100644 index 0000000..6a3df81 --- /dev/null +++ b/src/Rewrite/Describes.php @@ -0,0 +1,26 @@ +describe() + : (new ReflectionClass($node))->getShortName(); + } +} diff --git a/src/Rewrite/Obligation.php b/src/Rewrite/Obligation.php new file mode 100644 index 0000000..e3aeda5 --- /dev/null +++ b/src/Rewrite/Obligation.php @@ -0,0 +1,18 @@ +checked => 'unchecked', + $this->broken => 'broken', + default => 'upheld', + }; + + return sprintf('%s %s: %s', $this->preservation->describe(), $status, $this->explanation); + } +} diff --git a/src/Rewrite/OpaqueSource.php b/src/Rewrite/OpaqueSource.php new file mode 100644 index 0000000..c07d630 --- /dev/null +++ b/src/Rewrite/OpaqueSource.php @@ -0,0 +1,35 @@ +describe(), $node::class, Describes::node($node)); + } + + public function describe(): string + { + return sprintf('opaque %s at %s: %s', $this->class, $this->path, $this->describe); + } +} diff --git a/src/Rewrite/Preservation.php b/src/Rewrite/Preservation.php new file mode 100644 index 0000000..5fd5672 --- /dev/null +++ b/src/Rewrite/Preservation.php @@ -0,0 +1,38 @@ + 'type preservation', + self::Verdict => 'verdict preservation', + }; + } +} diff --git a/src/Rewrite/RewriteOutcome.php b/src/Rewrite/RewriteOutcome.php new file mode 100644 index 0000000..8e54cc0 --- /dev/null +++ b/src/Rewrite/RewriteOutcome.php @@ -0,0 +1,14 @@ + $verdicts */ + private function __construct( + public RewriteOutcome $outcome, + public string $path, + public string $rule, + public string $before, + public string $after, + public array $verdicts, + ) {} + + /** @param list $verdicts */ + public static function applied(SourcePath $path, RewriteRule $rule, object $before, object $after, array $verdicts): self + { + return new self(RewriteOutcome::Applied, $path->describe(), $rule->identifier(), Describes::node($before), Describes::node($after), $verdicts); + } + + /** @param list $verdicts */ + public static function refused(SourcePath $path, RewriteRule $rule, object $before, object $after, array $verdicts): self + { + return new self(RewriteOutcome::Refused, $path->describe(), $rule->identifier(), Describes::node($before), Describes::node($after), $verdicts); + } + + public function describe(): string + { + $lines = sprintf('%s %s at %s: %s => %s', $this->outcome->value, $this->rule, $this->path, $this->before, $this->after); + + foreach ($this->verdicts as $verdict) { + $lines .= "\n " . $verdict->describe(); + } + + return $lines; + } +} diff --git a/src/Rewrite/RewriteReport.php b/src/Rewrite/RewriteReport.php new file mode 100644 index 0000000..c68336e --- /dev/null +++ b/src/Rewrite/RewriteReport.php @@ -0,0 +1,47 @@ + $records + * @param list $opaque + */ + public function __construct( + public array $records, + public array $opaque, + ) {} + + /** @return list */ + public function applied(): array + { + return array_values(array_filter($this->records, fn(RewriteRecord $record): bool => $record->outcome === RewriteOutcome::Applied)); + } + + /** @return list */ + public function refused(): array + { + return array_values(array_filter($this->records, fn(RewriteRecord $record): bool => $record->outcome === RewriteOutcome::Refused)); + } + + public function describe(): string + { + $lines = array_map(fn(RewriteRecord $record): string => $record->describe(), $this->records); + $lines = [...$lines, ...array_map(fn(OpaqueSource $opaque): string => $opaque->describe(), $this->opaque)]; + + return $lines === [] ? 'no rewrites, nothing opaque' : implode("\n", $lines); + } +} diff --git a/src/Rewrite/RewriteRule.php b/src/Rewrite/RewriteRule.php new file mode 100644 index 0000000..c78f330 --- /dev/null +++ b/src/Rewrite/RewriteRule.php @@ -0,0 +1,61 @@ +> + */ + public function visits(): array; + + /** + * The replacement for this node, or null for "nothing to do here" — the + * common answer, and the one that keeps the tree's identity intact. + * + * The node arrives with its children already rewritten. The replacement is + * taken as final: the rewriter does not descend into it, so a rule that + * synthesises new structure owns the shape of what it returns. + */ + public function rewrite(Source $source): ?Source; + + /** + * What the replacement keeps, beyond the type preservation every rewrite + * is held to. Each claim is checked at each site the rule fires, and a + * claim the run has no oracle for is reported unchecked. + * + * @return list + */ + public function preserves(): array; +} diff --git a/src/Rewrite/RewriteRun.php b/src/Rewrite/RewriteRun.php new file mode 100644 index 0000000..7d5b221 --- /dev/null +++ b/src/Rewrite/RewriteRun.php @@ -0,0 +1,43 @@ +changed = $original->source !== $source; + } + + /** The rewritten expression: the original's dialect, definitions, declarations and boundary over the new tree. */ + public function expression(): Expression + { + return new Expression( + source: $this->source, + definitions: $this->original->definitions, + dialect: $this->original->dialect, + declarations: $this->original->declarations, + boundary: $this->original->boundary, + ); + } +} diff --git a/src/Rewrite/RewriteSite.php b/src/Rewrite/RewriteSite.php new file mode 100644 index 0000000..326567d --- /dev/null +++ b/src/Rewrite/RewriteSite.php @@ -0,0 +1,69 @@ + */ + private ?Result $compiledBefore = null; + + /** @var ?Result */ + private ?Result $compiledAfter = null; + + public function __construct( + public readonly Expression $context, + public readonly SourcePath $path, + public readonly Source $before, + public readonly Source $after, + ) {} + + /** @return Result */ + public function compileBefore(): Result + { + return $this->compiledBefore ??= $this->compile($this->before); + } + + /** @return Result */ + public function compileAfter(): Result + { + return $this->compiledAfter ??= $this->compile($this->after); + } + + /** @return Result */ + private function compile(Source $source): Result + { + return (new Expression( + source: $source, + definitions: $this->context->definitions, + dialect: $this->context->dialect, + declarations: $this->context->declarations, + boundary: $this->context->boundary, + ))->compile(); + } +} diff --git a/src/Rewrite/RewriteWalk.php b/src/Rewrite/RewriteWalk.php new file mode 100644 index 0000000..ff12040 --- /dev/null +++ b/src/Rewrite/RewriteWalk.php @@ -0,0 +1,151 @@ + */ + private array $records = []; + + /** @var list */ + private array $opaque = []; + + /** + * @param array, list> $rules Indexed by the exact class each rule visits. + * @param array $obligations Keyed by the preservation each discharges. + */ + public function __construct( + private readonly Expression $context, + private readonly array $rules, + private readonly SourceDescenders $descenders, + private readonly array $obligations, + ) {} + + public function run(): RewriteRun + { + $source = $this->source($this->context->source, SourcePath::root()); + + return new RewriteRun($this->context, $source, new RewriteReport($this->records, $this->opaque)); + } + + /** + * Bottom-up: a node's children are rewritten, the node is rebuilt around + * whatever came back, and only then are rules offered the rebuilt node. + * That order is what lets one pass collapse a nest — `!!!!x` reduces at + * every level on the way out — and it means a rule always sees the shape + * that will actually be stored, never one a deeper rewrite is about to + * change. + */ + public function source(Source $node, SourcePath $path): Source + { + $descender = $this->descenders->sources[$node::class] ?? null; + + if ($descender === null) { + $this->opaque[] = OpaqueSource::at($path, $node); + + return $node; + } + + return $this->apply($descender($node, new Descent($this, $path)), $path); + } + + public function pattern(MatchPattern $node, SourcePath $path): MatchPattern + { + $descender = $this->descenders->patterns[$node::class] ?? null; + + if ($descender === null) { + $this->opaque[] = OpaqueSource::at($path, $node); + + return $node; + } + + return $descender($node, new Descent($this, $path)); + } + + public function arm(MatchArm $arm, SourcePath $path): MatchArm + { + $descent = new Descent($this, $path); + $pattern = $descent->pattern($arm->pattern, 'pattern'); + $expression = $descent->child($arm->expression, 'expression'); + + return $pattern === $arm->pattern && $expression === $arm->expression + ? $arm + : new MatchArm($pattern, $expression); + } + + /** + * The rules registered for this exact class, in registration order, until + * one of them takes the site. A rule that offers nothing is passed over; a + * rule whose replacement breaks an obligation is recorded refused and the + * next rule is asked. The first sound replacement wins and ends the visit: + * two rules that both want a node would otherwise compose in an order + * nobody chose, and a rule offered its own output could rewrite forever. + * Opportunities a rewrite creates are found by running the rewriter again + * — a decision the caller makes, and can see in the report. + */ + private function apply(Source $node, SourcePath $path): Source + { + foreach ($this->rules[$node::class] ?? [] as $rule) { + $replacement = $rule->rewrite($node); + + if ($replacement === null) { + continue; + } + + $verdicts = $this->judge($rule, new RewriteSite($this->context, $path, $node, $replacement)); + + if (array_any($verdicts, static fn(ObligationVerdict $verdict): bool => $verdict->broken)) { + $this->records[] = RewriteRecord::refused($path, $rule, $node, $replacement, $verdicts); + + continue; + } + + $this->records[] = RewriteRecord::applied($path, $rule, $node, $replacement, $verdicts); + + return $replacement; + } + + return $node; + } + + /** + * Type preservation is checked at every site whether or not the rule + * claims it: the toolkit always has that oracle, and a rewrite that + * changes a program's type is not one anybody asked for. Everything else + * a rule claims is checked when the run was given the oracle for it, and + * reported unchecked when it was not. A rule free to name type + * preservation among its own claims costs nothing by doing so: a claim + * made twice is judged once. + * + * @return list + */ + private function judge(RewriteRule $rule, RewriteSite $site): array + { + $verdicts = []; + + foreach (array_unique([Preservation::CertifiedType, ...$rule->preserves()], SORT_REGULAR) as $preservation) { + $obligation = $this->obligations[$preservation->value] ?? null; + + $verdicts[] = $obligation === null + ? ObligationVerdict::unchecked($preservation, 'the run was given no oracle for this claim') + : $obligation->check($site); + } + + return $verdicts; + } +} diff --git a/src/Rewrite/Rewriter.php b/src/Rewrite/Rewriter.php new file mode 100644 index 0000000..173214e --- /dev/null +++ b/src/Rewrite/Rewriter.php @@ -0,0 +1,89 @@ +rewrite($expression); + * + * $run->report->describe(); // dry run: read this, take nothing + * $run->changed; // false when every subtree came back identical + * $run->source; // the tree to store + * ``` + * + * Four decisions govern a run: + * + * - **Bottom-up, one pass.** Children are rewritten before their parent is + * offered to rules, so a rule sees the shape that will be stored. + * - **Exact-class dispatch.** A rule declares the classes it visits and is + * indexed by them, so a node costs one array lookup no matter how many + * rules the run carries. + * - **Prove, then apply.** Every replacement is compiled against the + * expression's own declarations and must certify the same type as what it + * replaces; a rule may claim more, and the run checks each claim it has an + * oracle for. A broken obligation refuses that one site — the rest of the + * run proceeds — and the refusal is reported. This is the whole point: a + * fold that type-checks can still invert the meaning of a condition, and a + * rewrite nobody proved is a rewrite nobody should store. + * - **Opaque leaves are reported, never skipped.** A node class with no + * descent arm is not descended and not rewritten, and it appears in the + * report; silence about a shape the run could not see would read exactly + * like a clean tree. + * + * A rewriter is a value: it holds no run state, so one can be shared across + * every expression in a corpus. + */ +final readonly class Rewriter +{ + /** @var array, list> */ + private array $rules; + + /** @var array */ + private array $obligations; + + private SourceDescenders $descenders; + + /** + * @param list $rules Applied in this order at every node they visit. + * @param list $obligations Oracles beyond type preservation — a + * {@see VerdictPreservation} over the host's corpus, typically. One + * supplied for a preservation the toolkit already answers replaces it. + */ + public function __construct( + array $rules, + ?SourceDescenders $descenders = null, + array $obligations = [], + ) { + $indexed = []; + + foreach ($rules as $rule) { + foreach ($rule->visits() as $class) { + $indexed[$class][] = $rule; + } + } + + $checkers = [Preservation::CertifiedType->value => new TypePreservation()]; + + foreach ($obligations as $obligation) { + $checkers[$obligation->preservation()->value] = $obligation; + } + + $this->rules = $indexed; + $this->obligations = $checkers; + $this->descenders = $descenders ?? SourceDescenders::core(); + } + + public function rewrite(Expression $expression): RewriteRun + { + return (new RewriteWalk($expression, $this->rules, $this->descenders, $this->obligations))->run(); + } +} diff --git a/src/Rewrite/Rules/RemoveDoubleNegation.php b/src/Rewrite/Rules/RemoveDoubleNegation.php new file mode 100644 index 0000000..61de219 --- /dev/null +++ b/src/Rewrite/Rules/RemoveDoubleNegation.php @@ -0,0 +1,87 @@ + */ + private array $negations; + + /** + * @param list $negations The operator spellings that denote an + * involutive negation in the dialect this rule runs against. + */ + public function __construct(array $negations = ['!', 'not']) + { + $this->negations = $negations; + } + + public function identifier(): string + { + return 'axiom.rewrite.remove-double-negation'; + } + + public function visits(): array + { + return [UnaryExpression::class]; + } + + public function preserves(): array + { + return [Preservation::Verdict]; + } + + public function rewrite(Source $source): ?Source + { + if (! $source instanceof UnaryExpression || ! $this->negates($source->operator)) { + return null; + } + + $operand = $source->operand; + + if (! $operand instanceof UnaryExpression || ! $this->negates($operand->operator)) { + return null; + } + + return $operand->operand; + } + + private function negates(string $operator): bool + { + return in_array($operator, $this->negations, strict: true); + } +} diff --git a/src/Rewrite/Rules/RemoveRedundantDefault.php b/src/Rewrite/Rules/RemoveRedundantDefault.php new file mode 100644 index 0000000..99cb956 --- /dev/null +++ b/src/Rewrite/Rules/RemoveRedundantDefault.php @@ -0,0 +1,55 @@ +`, the types differ, and the site is refused. Over a + * definite inner both compile to the same type — necessarily, since they + * compile to the same node — and the rewrite is taken. + * + * Removing the node does change what an execution observer sees: the + * `default` label and its annotations go with it. That is a change to the + * trace of the program, not to what the program answers. + */ +final readonly class RemoveRedundantDefault implements RewriteRule +{ + public function identifier(): string + { + return 'axiom.rewrite.remove-redundant-default'; + } + + public function visits(): array + { + return [DefaultValue::class]; + } + + public function preserves(): array + { + return [Preservation::Verdict]; + } + + public function rewrite(Source $source): ?Source + { + return $source instanceof DefaultValue ? $source->source : null; + } +} diff --git a/src/Rewrite/SourceDescenders.php b/src/Rewrite/SourceDescenders.php new file mode 100644 index 0000000..cf28e5f --- /dev/null +++ b/src/Rewrite/SourceDescenders.php @@ -0,0 +1,59 @@ +, callable(Source, Descent): Source> $sources + * @param array, callable(MatchPattern, Descent): MatchPattern> $patterns + */ + private function __construct( + public array $sources, + public array $patterns, + ) {} + + public static function core(): self + { + return new self(CoreSourceDescenders::sources(), CoreSourceDescenders::patterns()); + } + + public function with(Extension ...$extensions): self + { + $sources = $this->sources; + + foreach ($extensions as $extension) { + foreach ($extension->sourceDescenders() as $class => $descender) { + if (array_key_exists($class, $sources)) { + throw new InvalidArgumentException(sprintf( + 'Source class [%s] has two descent arms; descent ownership is exact and extension order carries no precedence.', + $class, + )); + } + + $sources[$class] = $descender; + } + } + + return new self($sources, $this->patterns); + } +} diff --git a/src/Rewrite/SourcePath.php b/src/Rewrite/SourcePath.php new file mode 100644 index 0000000..277f47f --- /dev/null +++ b/src/Rewrite/SourcePath.php @@ -0,0 +1,52 @@ + $segments */ + private function __construct(private array $segments) {} + + public static function root(): self + { + return new self([]); + } + + /** + * @param string $segment The property holding the child, optionally + * subscripted for a list slot: `arms[1]`. + */ + public function child(string $segment): self + { + if ($segment === '') { + throw new InvalidArgumentException('A source path segment names a property and cannot be empty.'); + } + + return new self([...$this->segments, $segment]); + } + + public function describe(): string + { + if ($this->segments === []) { + return '$'; + } + + return '$.' . implode('.', $this->segments); + } +} diff --git a/src/Rewrite/TypePreservation.php b/src/Rewrite/TypePreservation.php new file mode 100644 index 0000000..dba230c --- /dev/null +++ b/src/Rewrite/TypePreservation.php @@ -0,0 +1,61 @@ +compileBefore(); + $after = $site->compileAfter(); + + if ($before->isErr() && $after->isErr()) { + $original = $before->unwrapErr()->describe(); + $replacement = $after->unwrapErr()->describe(); + + return $original === $replacement + ? ObligationVerdict::upheld($this->preservation(), sprintf('both refuse: %s', $original)) + : ObligationVerdict::broken($this->preservation(), sprintf('both refuse, but differently: [%s] against [%s]', $original, $replacement)); + } + + if ($before->isErr()) { + return ObligationVerdict::broken($this->preservation(), sprintf('the original refuses and the replacement compiles: %s', $before->unwrapErr()->describe())); + } + + if ($after->isErr()) { + return ObligationVerdict::broken($this->preservation(), sprintf('the original compiles and the replacement refuses: %s', $after->unwrapErr()->describe())); + } + + $beforeType = $before->unwrap()->returns; + $afterType = $after->unwrap()->returns; + + return TypeRelations::areEquivalent($beforeType, $afterType)->isOk() + ? ObligationVerdict::upheld($this->preservation(), sprintf('both compile to %s', TypeDescriber::describe($beforeType))) + : ObligationVerdict::broken($this->preservation(), sprintf( + 'the original compiles to %s and the replacement to %s', + TypeDescriber::describe($beforeType), + TypeDescriber::describe($afterType), + )); + } +} diff --git a/src/Rewrite/VerdictPreservation.php b/src/Rewrite/VerdictPreservation.php new file mode 100644 index 0000000..f416cf2 --- /dev/null +++ b/src/Rewrite/VerdictPreservation.php @@ -0,0 +1,76 @@ +compileBefore(); + $after = $site->compileAfter(); + + if ($before->isErr() || $after->isErr()) { + return ObligationVerdict::unchecked($this->preservation(), 'a subtree does not compile, so there is no pair of programs to run'); + } + + $original = $before->unwrap(); + $replacement = $after->unwrap(); + $cases = 0; + + foreach ($this->corpus->cases() as $label => $bindings) { + $cases++; + $answered = self::answer($original($bindings)); + $answers = self::answer($replacement($bindings)); + + if ($answered !== $answers) { + return ObligationVerdict::broken($this->preservation(), sprintf( + 'case [%s]: the original answers %s and the replacement %s', + $label, + $answered, + $answers, + )); + } + } + + return ObligationVerdict::upheld($this->preservation(), sprintf('%d corpus case(s) agree', $cases)); + } + + /** + * @param Result, Throwable> $result + */ + private static function answer(Result $result): string + { + /** @var string */ + return $result->mapOrElse( + fn(Throwable $error): string => sprintf('error(%s)', $error->getMessage()), + fn(Option $value): string => $value->mapOr('absent', fn(mixed $present): string => sprintf('value(%s)', (new Exporter())->shortenedExport($present))), + ); + } +} diff --git a/tests/Rewrite/CoreDescentExhaustivenessTest.php b/tests/Rewrite/CoreDescentExhaustivenessTest.php new file mode 100644 index 0000000..fedfc76 --- /dev/null +++ b/tests/Rewrite/CoreDescentExhaustivenessTest.php @@ -0,0 +1,84 @@ +assertArrayHasKey($class, $arms, sprintf( + '[%s] is a core source with no descent arm: the rewriter would treat it as an opaque leaf and never rewrite inside it.', + $class, + )); + } + + $this->assertSame([], array_diff(array_keys($arms), self::coreClasses(Source::class)), 'every arm names a core source class'); + } + + #[Test] + public function every_core_pattern_class_has_a_descent_arm(): void + { + $arms = CoreSourceDescenders::patterns(); + + foreach (self::coreClasses(MatchPattern::class) as $class) { + $this->assertArrayHasKey($class, $arms, sprintf('[%s] is a core match pattern with no descent arm.', $class)); + } + + $this->assertSame([], array_diff(array_keys($arms), self::coreClasses(MatchPattern::class)), 'every arm names a core pattern class'); + } + + /** + * Read off the directory rather than a hand-kept list: a list would have + * to be updated by the same person who forgot the arm. + * + * @param class-string $interface + * @return list + */ + private static function coreClasses(string $interface): array + { + $classes = []; + + foreach (glob(__DIR__ . '/../../src/Sources/*.php') ?: [] as $file) { + /** @var class-string $class */ + $class = 'Superscript\\Axiom\\Sources\\' . basename($file, '.php'); + + if (! class_exists($class)) { + continue; + } + + $reflection = new ReflectionClass($class); + + if ($reflection->isAbstract() || ! $reflection->implementsInterface($interface)) { + continue; + } + + $classes[] = $class; + } + + return $classes; + } +} diff --git a/tests/Rewrite/Fixtures/BoxExtension.php b/tests/Rewrite/Fixtures/BoxExtension.php new file mode 100644 index 0000000..caeef83 --- /dev/null +++ b/tests/Rewrite/Fixtures/BoxExtension.php @@ -0,0 +1,41 @@ + $this->compile(...), + ]; + } + + public function sourceDescenders(): array + { + return [ + BoxSource::class => $this->descend(...), + ]; + } + + private function compile(BoxSource $source, SourceCompilation $compilation): CompiledSource + { + return $compilation->child($source->inner, 'inner'); + } + + private function descend(BoxSource $source, Descent $descent): Source + { + $inner = $descent->child($source->inner, 'inner'); + + return $inner === $source->inner ? $source : new BoxSource($inner); + } +} diff --git a/tests/Rewrite/Fixtures/BoxSource.php b/tests/Rewrite/Fixtures/BoxSource.php new file mode 100644 index 0000000..7a280ca --- /dev/null +++ b/tests/Rewrite/Fixtures/BoxSource.php @@ -0,0 +1,19 @@ +inner instanceof Describable ? $this->inner->describe() : $this->inner::class); + } +} diff --git a/tests/Rewrite/Fixtures/StubRule.php b/tests/Rewrite/Fixtures/StubRule.php new file mode 100644 index 0000000..e336a66 --- /dev/null +++ b/tests/Rewrite/Fixtures/StubRule.php @@ -0,0 +1,46 @@ +> $visits + * @param Closure(Source): ?Source $rewrite + * @param list $preserves + */ + public function __construct( + private string $identifier, + private array $visits, + private Closure $rewrite, + private array $preserves = [], + ) {} + + public function identifier(): string + { + return $this->identifier; + } + + public function visits(): array + { + return $this->visits; + } + + public function rewrite(Source $source): ?Source + { + return ($this->rewrite)($source); + } + + public function preserves(): array + { + return $this->preserves; + } +} diff --git a/tests/Rewrite/ObligationTest.php b/tests/Rewrite/ObligationTest.php new file mode 100644 index 0000000..49dce57 --- /dev/null +++ b/tests/Rewrite/ObligationTest.php @@ -0,0 +1,221 @@ + $declarations */ + private static function site(Source $before, Source $after, array $declarations = []): RewriteSite + { + return new RewriteSite(new Expression($before, declarations: $declarations), SourcePath::root(), $before, $after); + } + + #[Test] + public function a_site_compiles_each_subtree_once(): void + { + $site = self::site(new StaticSource(1), new StaticSource(2)); + + $this->assertSame($site->compileBefore(), $site->compileBefore()); + $this->assertSame($site->compileAfter(), $site->compileAfter()); + $this->assertNotSame($site->compileBefore(), $site->compileAfter()); + } + + #[Test] + public function a_subtree_compiles_in_the_whole_expressions_scope(): void + { + $site = self::site(new SymbolSource('flag'), new SymbolSource('flag'), ['flag' => new BooleanType()]); + + $this->assertTrue($site->compileBefore()->isOk(), 'the declaration the whole expression makes is the one a subtree is compiled against'); + } + + #[Test] + public function equal_certified_types_uphold_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))), + new SymbolSource('flag'), + ['flag' => new BooleanType()], + )); + + $this->assertTrue($verdict->checked); + $this->assertFalse($verdict->broken); + $this->assertSame('type preservation upheld: both compile to Boolean', $verdict->describe()); + } + + #[Test] + public function different_certified_types_break_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new Coerce(new BooleanType(), new StaticSource(true)), + new Coerce(new StringType(), new StaticSource('true')), + )); + + $this->assertTrue($verdict->broken); + $this->assertSame('type preservation broken: the original compiles to Boolean and the replacement to String', $verdict->describe()); + } + + #[Test] + public function turning_a_refusal_into_a_program_breaks_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))), + new SymbolSource('count'), + ['count' => new NumberType()], + )); + + $this->assertTrue($verdict->broken); + $this->assertStringStartsWith('type preservation broken: the original refuses and the replacement compiles: [!] expects Boolean; got Number.', $verdict->describe()); + } + + #[Test] + public function turning_a_program_into_a_refusal_breaks_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new SymbolSource('count'), + new UnaryExpression('!', new SymbolSource('count')), + ['count' => new NumberType()], + )); + + $this->assertTrue($verdict->broken); + $this->assertStringStartsWith('type preservation broken: the original compiles and the replacement refuses: [!] expects Boolean; got Number.', $verdict->describe()); + } + + #[Test] + public function the_same_refusal_on_both_sides_upholds_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new Coerce(new NumberType(), new SymbolSource('missing')), + new Coerce(new StringType(), new SymbolSource('missing')), + )); + + $this->assertFalse($verdict->broken, 'neither tree can run, and the author is told the same thing either way'); + $this->assertStringStartsWith('type preservation upheld: both refuse:', $verdict->describe()); + } + + #[Test] + public function two_different_refusals_break_type_preservation(): void + { + $verdict = (new TypePreservation())->check(self::site( + new SymbolSource('missing'), + new UnaryExpression('!', new SymbolSource('count')), + ['count' => new NumberType()], + )); + + $this->assertTrue($verdict->broken, 'a rewrite must not be what changes the diagnostic an author reads'); + $this->assertStringContainsString('both refuse, but differently:', $verdict->describe()); + } + + #[Test] + public function a_corpus_that_agrees_upholds_verdict_preservation(): void + { + $obligation = new VerdictPreservation(new ArrayBindingsCorpus([ + 'yes' => ['flag' => true], + 'no' => ['flag' => false], + ])); + + $verdict = $obligation->check(self::site( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))), + new SymbolSource('flag'), + ['flag' => new BooleanType()], + )); + + $this->assertFalse($verdict->broken); + $this->assertSame('verdict preservation upheld: 2 corpus case(s) agree', $verdict->describe()); + } + + #[Test] + public function absence_answers_alike_and_still_counts(): void + { + $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['unanswered' => []])); + + $verdict = $obligation->check(self::site( + new SymbolSource('roof'), + new SymbolSource('roof'), + ['roof' => new Optional(new OptionType(new NumberType()))], + )); + + $this->assertSame('verdict preservation upheld: 1 corpus case(s) agree', $verdict->describe()); + } + + #[Test] + public function one_disagreeing_case_breaks_verdict_preservation_and_names_itself(): void + { + $obligation = new VerdictPreservation(new ArrayBindingsCorpus([ + 'ordinary' => ['divisor' => 2], + 'zero' => ['divisor' => 0], + ])); + + $verdict = $obligation->check(self::site( + new InfixExpression(new StaticSource(10), '/', new SymbolSource('divisor')), + new StaticSource(5), + ['divisor' => new NumberType()], + )); + + $this->assertTrue($verdict->broken); + $this->assertStringContainsString('case [zero]: the original answers error(', $verdict->describe()); + $this->assertStringContainsString('and the replacement value(5)', $verdict->describe()); + } + + #[Test] + public function a_subtree_that_does_not_compile_leaves_verdicts_unchecked(): void + { + $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['any' => []])); + + $verdict = $obligation->check(self::site(new SymbolSource('missing'), new StaticSource(1))); + + $this->assertFalse($verdict->checked); + $this->assertFalse($verdict->broken); + $this->assertSame('verdict preservation unchecked: a subtree does not compile, so there is no pair of programs to run', $verdict->describe()); + } + + #[Test] + public function a_replacement_that_does_not_compile_leaves_verdicts_unchecked(): void + { + $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['any' => []])); + + $verdict = $obligation->check(self::site(new StaticSource(1), new SymbolSource('missing'))); + + $this->assertFalse($verdict->checked); + } + + #[Test] + public function each_obligation_answers_for_one_preservation(): void + { + $this->assertSame(Preservation::CertifiedType, (new TypePreservation())->preservation()); + $this->assertSame(Preservation::Verdict, (new VerdictPreservation(new ArrayBindingsCorpus([])))->preservation()); + } +} diff --git a/tests/Rewrite/RewriterTest.php b/tests/Rewrite/RewriterTest.php new file mode 100644 index 0000000..902c3c7 --- /dev/null +++ b/tests/Rewrite/RewriterTest.php @@ -0,0 +1,430 @@ + $rules */ + private static function rewrite(Source $source, array $rules, RecordType|array $declarations = [], ?SourceDescenders $descenders = null): RewriteRun + { + return (new Rewriter($rules, $descenders))->rewrite(new Expression($source, declarations: $declarations)); + } + + private static function replaces(string $identifier, string $class, Source $replacement): StubRule + { + /** @var non-empty-list> $visits */ + $visits = [$class]; + + return new StubRule($identifier, $visits, static fn(Source $source): Source => $replacement); + } + + #[Test] + public function an_untouched_tree_comes_back_as_the_same_instance(): void + { + $source = new InfixExpression(new SymbolSource('a'), '&&', new SymbolSource('b')); + + $run = self::rewrite($source, [], ['a' => new BooleanType(), 'b' => new BooleanType()]); + + $this->assertSame($source, $run->source, 'nothing fired, so nothing was rebuilt'); + $this->assertFalse($run->changed); + $this->assertSame('no rewrites, nothing opaque', $run->report->describe()); + } + + #[Test] + public function untouched_siblings_keep_their_identity_when_one_child_is_rewritten(): void + { + $left = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))); + $right = new SymbolSource('b'); + $source = new InfixExpression($left, '&&', $right); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType(), 'b' => new BooleanType()]); + + $this->assertInstanceOf(InfixExpression::class, $run->source); + $this->assertNotSame($source, $run->source); + $this->assertSame($right, $run->source->right, 'the untouched subtree is the very same instance'); + $this->assertSame('a && b', $run->source->describe()); + $this->assertTrue($run->changed); + } + + #[Test] + public function bottom_up_application_collapses_a_nest_in_one_pass(): void + { + $source = new UnaryExpression('!', new UnaryExpression('!', new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))))); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]); + + $this->assertSame('a', $run->source->describe()); + $this->assertCount(2, $run->report->applied()); + } + + #[Test] + public function a_rewritten_expression_carries_the_original_scope(): void + { + $source = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]); + $program = $run->expression()->compile()->unwrap(); + + $this->assertTrue($program(['a' => true])->unwrap()->unwrap()); + $this->assertSame($run->original->declarations, $run->expression()->declarations); + } + + #[Test] + public function a_site_is_reported_with_its_path_before_and_after(): void + { + $source = new InfixExpression(new SymbolSource('a'), '&&', new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('b')))); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType(), 'b' => new BooleanType()]); + $applied = $run->report->applied(); + + $this->assertCount(1, $applied); + $this->assertSame(RewriteOutcome::Applied, $applied[0]->outcome); + $this->assertSame('$.right', $applied[0]->path); + $this->assertSame('axiom.rewrite.remove-double-negation', $applied[0]->rule); + $this->assertSame('!!b', $applied[0]->before); + $this->assertSame('b', $applied[0]->after); + $this->assertSame( + "applied axiom.rewrite.remove-double-negation at \$.right: !!b => b" + . "\n type preservation upheld: both compile to Boolean" + . "\n verdict preservation unchecked: the run was given no oracle for this claim", + $run->report->describe(), + ); + } + + #[Test] + public function a_broken_obligation_refuses_that_site_and_reports_it(): void + { + $source = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['count' => new NumberType()]); + + $this->assertSame($source, $run->source, 'a refused rewrite leaves the tree exactly as it was'); + $this->assertFalse($run->changed); + $this->assertSame([], $run->report->applied()); + + $refused = $run->report->refused(); + $this->assertCount(1, $refused); + $this->assertSame('$', $refused[0]->path); + $this->assertStringContainsString('type preservation broken: the original refuses and the replacement compiles', $refused[0]->describe()); + $this->assertStringContainsString('verdict preservation unchecked: the run was given no oracle for this claim', $refused[0]->describe()); + } + + #[Test] + public function a_refused_rule_lets_the_next_rule_take_the_site(): void + { + $source = new SymbolSource('a'); + $unsound = self::replaces('unsound', SymbolSource::class, new Coerce(new StringType(), new StaticSource('a string where a boolean was'))); + $sound = self::replaces('sound', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true))); + + $run = self::rewrite($source, [$unsound, $sound], ['a' => new BooleanType()]); + + $this->assertSame([RewriteOutcome::Refused, RewriteOutcome::Applied], array_map(fn(RewriteRecord $record): RewriteOutcome => $record->outcome, $run->report->records)); + $this->assertSame(['unsound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->refused())); + $this->assertSame(['sound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->applied())); + $this->assertSame('true (as boolean)', Describes::node($run->source)); + } + + #[Test] + public function the_first_sound_rewrite_ends_the_visit(): void + { + $first = self::replaces('first', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true))); + $second = self::replaces('second', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(false))); + + $run = self::rewrite(new SymbolSource('a'), [$first, $second], ['a' => new BooleanType()]); + + $this->assertCount(1, $run->report->records); + $this->assertSame('first', $run->report->applied()[0]->rule); + } + + #[Test] + public function a_rule_that_offers_nothing_is_passed_over(): void + { + /** @var non-empty-list> $visits */ + $visits = [SymbolSource::class]; + $silent = new StubRule('silent', $visits, static fn(Source $source): ?Source => null); + $source = new SymbolSource('a'); + + $run = self::rewrite($source, [$silent], ['a' => new BooleanType()]); + + $this->assertSame($source, $run->source); + $this->assertSame([], $run->report->records); + } + + #[Test] + public function a_rule_is_only_offered_the_exact_classes_it_visits(): void + { + $seen = []; + /** @var non-empty-list> $visits */ + $visits = [SymbolSource::class]; + $spy = new StubRule('spy', $visits, static function (Source $source) use (&$seen): ?Source { + $seen[] = $source::class; + + return null; + }); + + self::rewrite(new InfixExpression(new SymbolSource('a'), '&&', new StaticSource(true)), [$spy], ['a' => new BooleanType()]); + + $this->assertSame([SymbolSource::class], $seen); + } + + #[Test] + public function a_claim_the_rule_repeats_is_judged_once_and_the_rest_still_judged(): void + { + /** @var non-empty-list> $visits */ + $visits = [SymbolSource::class]; + $rule = new StubRule( + 'repeats', + $visits, + static fn(Source $source): Source => new Coerce(new BooleanType(), new StaticSource(true)), + [Preservation::CertifiedType, Preservation::Verdict], + ); + + $run = self::rewrite(new SymbolSource('a'), [$rule], ['a' => new BooleanType()]); + + $this->assertSame( + ['type preservation upheld: both compile to Boolean', 'verdict preservation unchecked: the run was given no oracle for this claim'], + array_map(fn(ObligationVerdict $verdict): string => $verdict->describe(), $run->report->applied()[0]->verdicts), + ); + } + + #[Test] + public function a_rule_that_offers_nothing_lets_the_next_rule_take_the_site(): void + { + /** @var non-empty-list> $visits */ + $visits = [SymbolSource::class]; + $silent = new StubRule('silent', $visits, static fn(Source $source): ?Source => null); + $sound = self::replaces('sound', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true))); + + $run = self::rewrite(new SymbolSource('a'), [$silent, $sound], ['a' => new BooleanType()]); + + $this->assertSame(['sound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->applied())); + } + + #[Test] + public function an_applied_site_and_a_refused_one_are_reported_side_by_side(): void + { + $source = new InfixExpression( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))), + '&&', + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))), + ); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType(), 'count' => new NumberType()]); + + $this->assertSame(['$.left'], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->applied())); + $this->assertSame(['$.right'], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->refused())); + } + + #[Test] + public function an_unregistered_host_shape_is_an_opaque_leaf_the_run_reports(): void + { + $hidden = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))); + $source = new InfixExpression(new SymbolSource('a'), '&&', new HostValueSource(new BooleanType(), $hidden)); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]); + + $this->assertSame($source, $run->source, 'an opaque node is never descended and never rewritten'); + $this->assertSame([], $run->report->applied()); + $this->assertCount(1, $run->report->opaque); + $this->assertSame('$.right', $run->report->opaque[0]->path); + $this->assertSame(HostValueSource::class, $run->report->opaque[0]->class); + $this->assertSame('HostValueSource', $run->report->opaque[0]->describe, 'a host node that cannot spell itself is named by its class'); + $this->assertStringContainsString('opaque ' . HostValueSource::class . ' at $.right: HostValueSource', $run->report->describe()); + } + + #[Test] + public function a_registered_host_shape_is_descended_and_rebuilt(): void + { + $descenders = SourceDescenders::core()->with(new BoxExtension()); + $source = new BoxSource(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a')))); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()], $descenders); + + $this->assertInstanceOf(BoxSource::class, $run->source); + $this->assertSame('box(a)', $run->source->describe()); + $this->assertSame('$.inner', $run->report->applied()[0]->path); + $this->assertSame([], $run->report->opaque); + } + + #[Test] + public function a_registered_host_shape_shares_structure_when_nothing_moved(): void + { + $descenders = SourceDescenders::core()->with(new BoxExtension()); + $source = new BoxSource(new SymbolSource('a')); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()], $descenders); + + $this->assertSame($source, $run->source); + } + + #[Test] + public function every_core_shape_is_descended_through(): void + { + $doubled = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))); + $source = new MatchExpression( + subject: new Coerce(new StringType(), new MemberAccessSource(new SymbolSource('customer'), 'name')), + arms: [ + new MatchArm(new LiteralPattern('ada'), new Ascription(new BooleanType(), $doubled)), + new MatchArm(new ExpressionPattern(new DefaultValue(new StaticSource('bob'), 'bob')), new StaticSource(false)), + new MatchArm(new WildcardPattern(), new InfixExpression($doubled, '||', new StaticSource(false))), + ], + ); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], [ + 'flag' => new BooleanType(), + 'customer' => new RecordType(['name' => new StringType()]), + ]); + + $this->assertSame([ + '$.arms[0].expression.source', + '$.arms[2].expression.left', + ], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->applied())); + $this->assertSame('match customer.name (as string) { \'ada\' => flag (is boolean), \'bob\' ?? \'bob\' => false, _ => flag || false }', $run->source->describe()); + } + + /** + * A rewrite under a node that only wraps its child — a coercion, an + * authored default, a member access — must rebuild the wrapper around the + * new child and keep everything else about it. + */ + #[Test] + public function a_wrapping_shape_rebuilds_around_a_rewritten_child(): void + { + $alias = self::replaces('alias', SymbolSource::class, new SymbolSource('b')); + $record = new RecordType(['name' => new StringType()]); + + $coerce = self::rewrite(new Coerce(new StringType(), new SymbolSource('a')), [$alias], ['a' => new StringType(), 'b' => new StringType()]); + $default = self::rewrite(new DefaultValue(new SymbolSource('a'), 0), [$alias], ['a' => new OptionType(new NumberType()), 'b' => new OptionType(new NumberType())]); + $member = self::rewrite(new MemberAccessSource(new SymbolSource('a'), 'name'), [$alias], ['a' => $record, 'b' => $record]); + + $this->assertSame('b (as string)', Describes::node($coerce->source)); + $this->assertSame('b ?? 0', Describes::node($default->source)); + $this->assertSame('b.name', Describes::node($member->source)); + } + + #[Test] + public function a_match_arm_and_its_pattern_keep_their_identity_when_nothing_moved(): void + { + $arm = new MatchArm(new ExpressionPattern(new StaticSource('ada')), new StaticSource(1)); + $source = new MatchExpression(new SymbolSource('name'), [$arm, new MatchArm(new WildcardPattern(), new StaticSource(0))]); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['name' => new StringType()]); + + $this->assertSame($source, $run->source); + } + + #[Test] + public function a_rewrite_inside_an_expression_pattern_rebuilds_the_arm(): void + { + $source = new MatchExpression( + subject: new SymbolSource('flag'), + arms: [ + new MatchArm(new ExpressionPattern(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag')))), new StaticSource(1)), + new MatchArm(new WildcardPattern(), new StaticSource(0)), + ], + ); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType()]); + + $this->assertSame('match flag { flag => 1, _ => 0 }', $run->source->describe()); + $this->assertSame('$.arms[0].pattern.source', $run->report->applied()[0]->path); + } + + #[Test] + public function an_unknown_pattern_shape_is_opaque_too(): void + { + $pattern = new class implements \Superscript\Axiom\Sources\MatchPattern {}; + $source = new MatchExpression(new SymbolSource('flag'), [new MatchArm($pattern, new StaticSource(1))]); + + $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType()]); + + $this->assertSame($source, $run->source); + $this->assertCount(1, $run->report->opaque); + $this->assertSame('$.arms[0].pattern', $run->report->opaque[0]->path); + } + + #[Test] + public function a_path_segment_names_a_property(): void + { + $this->assertSame('$.left.operand', SourcePath::root()->child('left')->child('operand')->describe()); + } + + #[Test] + public function an_oracle_the_run_is_given_answers_the_claim_it_discharges(): void + { + $rewriter = new Rewriter( + [new RemoveDoubleNegation()], + obligations: [new VerdictPreservation(new ArrayBindingsCorpus(['yes' => ['a' => true]]))], + ); + + $run = $rewriter->rewrite(new Expression( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))), + declarations: ['a' => new BooleanType()], + )); + + $this->assertSame( + ['type preservation upheld: both compile to Boolean', 'verdict preservation upheld: 1 corpus case(s) agree'], + array_map(fn(ObligationVerdict $verdict): string => $verdict->describe(), $run->report->applied()[0]->verdicts), + ); + } +} diff --git a/tests/Rewrite/Rules/RemoveDoubleNegationTest.php b/tests/Rewrite/Rules/RemoveDoubleNegationTest.php new file mode 100644 index 0000000..f7c80ed --- /dev/null +++ b/tests/Rewrite/Rules/RemoveDoubleNegationTest.php @@ -0,0 +1,155 @@ +rewrite(new UnaryExpression('!', new UnaryExpression('!', $operand))); + + $this->assertSame($operand, $rewritten); + } + + #[Test] + public function the_two_spellings_of_negation_cancel_each_other(): void + { + $operand = new SymbolSource('flag'); + + $this->assertSame($operand, (new RemoveDoubleNegation())->rewrite(new UnaryExpression('not', new UnaryExpression('!', $operand)))); + $this->assertSame($operand, (new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new UnaryExpression('not', $operand)))); + } + + #[Test] + public function a_single_negation_is_left_alone(): void + { + $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new SymbolSource('flag')))); + } + + #[Test] + public function another_operator_is_left_alone(): void + { + $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('-', new UnaryExpression('-', new SymbolSource('count'))))); + $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new UnaryExpression('-', new SymbolSource('count'))))); + $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('-', new UnaryExpression('!', new SymbolSource('flag'))))); + } + + #[Test] + public function another_node_shape_is_left_alone(): void + { + $this->assertNull((new RemoveDoubleNegation())->rewrite(new StaticSource(true))); + } + + #[Test] + public function a_dialect_declares_which_of_its_spellings_are_involutive(): void + { + $rule = new RemoveDoubleNegation(['!']); + + $this->assertNull($rule->rewrite(new UnaryExpression('not', new UnaryExpression('not', new SymbolSource('flag'))))); + $this->assertNotNull($rule->rewrite(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))))); + } + + #[Test] + public function it_visits_unary_expressions_and_claims_verdict_preservation(): void + { + $rule = new RemoveDoubleNegation(); + + $this->assertSame([UnaryExpression::class], $rule->visits()); + $this->assertSame([Preservation::Verdict], $rule->preserves()); + $this->assertSame('axiom.rewrite.remove-double-negation', $rule->identifier()); + } + + /** + * Absence is where a "harmless" simplification usually stops being one: + * the lifted `!` propagates it, so `!!` is the lift of the identity and + * an unanswered question stays unanswered on both sides of the rewrite. + */ + #[Test] + public function it_is_neutral_over_absence(): void + { + $comparison = new InfixExpression(new SymbolSource('roof'), '>', new StaticSource(0.25)); + $expression = new Expression( + source: new UnaryExpression('!', new UnaryExpression('!', $comparison)), + declarations: ['roof' => new Optional(new OptionType(new NumberType()))], + ); + + $run = (new Rewriter( + [new RemoveDoubleNegation()], + obligations: [new VerdictPreservation(new ArrayBindingsCorpus([ + 'above' => ['roof' => 0.3], + 'below' => ['roof' => 0.1], + 'unanswered' => [], + ]))], + ))->rewrite($expression); + + $this->assertSame('roof > 0.25', $run->source->describe()); + $this->assertSame('verdict preservation upheld: 3 corpus case(s) agree', $run->report->applied()[0]->verdicts[1]->describe()); + + $program = $run->expression()->compile()->unwrap(); + $this->assertTrue($program([])->unwrap()->isNone(), 'not-knowing, negated twice or not at all, is still not-knowing'); + } + + #[Test] + public function a_negation_over_something_that_is_not_boolean_is_refused_rather_than_simplified(): void + { + $expression = new Expression( + source: new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))), + declarations: ['count' => new NumberType()], + ); + + $run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression); + + $this->assertFalse($run->changed, 'the original never compiled; handing back a certified Number program would invent one'); + $this->assertCount(1, $run->report->refused()); + } + + #[Test] + public function a_boolean_expression_keeps_its_answers(): void + { + $expression = new Expression( + source: new InfixExpression( + new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))), + '&&', + new UnaryExpression('!', new SymbolSource('other')), + ), + declarations: ['flag' => new BooleanType(), 'other' => new BooleanType()], + ); + + $run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression); + $before = $expression->compile()->unwrap(); + $after = $run->expression()->compile()->unwrap(); + + foreach ([[true, true], [true, false], [false, true], [false, false]] as [$flag, $other]) { + $bindings = ['flag' => $flag, 'other' => $other]; + $this->assertSame($before($bindings)->unwrap()->unwrap(), $after($bindings)->unwrap()->unwrap()); + } + + $this->assertSame('flag && !other', $run->source->describe()); + } +} diff --git a/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php b/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php new file mode 100644 index 0000000..e7ccafe --- /dev/null +++ b/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php @@ -0,0 +1,105 @@ +assertSame($inner, (new RemoveRedundantDefault())->rewrite(new DefaultValue($inner, 0))); + $this->assertNull((new RemoveRedundantDefault())->rewrite($inner)); + } + + #[Test] + public function it_visits_defaults_and_claims_verdict_preservation(): void + { + $rule = new RemoveRedundantDefault(); + + $this->assertSame([DefaultValue::class], $rule->visits()); + $this->assertSame([Preservation::Verdict], $rule->preserves()); + $this->assertSame('axiom.rewrite.remove-redundant-default', $rule->identifier()); + } + + #[Test] + public function a_default_over_a_definite_source_is_removed(): void + { + $expression = new Expression( + source: new DefaultValue(new SymbolSource('amount'), 0), + declarations: ['amount' => new NumberType()], + ); + + $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression); + + $this->assertSame('amount', $run->source->describe()); + $this->assertSame('type preservation upheld: both compile to Number', $run->report->applied()[0]->verdicts[0]->describe()); + } + + #[Test] + public function a_default_that_can_actually_fire_is_refused(): void + { + $expression = new Expression( + source: new DefaultValue(new SymbolSource('amount'), 0), + declarations: ['amount' => new OptionType(new NumberType())], + ); + + $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression); + + $this->assertFalse($run->changed); + $this->assertSame( + 'type preservation broken: the original compiles to Number and the replacement to Number?', + $run->report->refused()[0]->verdicts[0]->describe(), + ); + } + + #[Test] + public function a_nested_redundant_default_is_removed_without_touching_the_useful_one(): void + { + $expression = new Expression( + source: new DefaultValue(new DefaultValue(new SymbolSource('amount'), 1), 0), + declarations: ['amount' => new OptionType(new NumberType())], + ); + + $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression); + + $this->assertSame('amount ?? 1', $run->source->describe(), 'the inner default is the one absence can reach'); + $this->assertSame(['$'], array_map(fn($record): string => $record->path, $run->report->applied())); + $this->assertSame(['$.source'], array_map(fn($record): string => $record->path, $run->report->refused())); + } + + #[Test] + public function the_program_answers_the_same_thing_either_way(): void + { + $expression = new Expression( + source: new DefaultValue(new SymbolSource('amount'), 0), + declarations: ['amount' => new NumberType()], + ); + + $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression); + + $before = $expression->compile()->unwrap(); + $after = $run->expression()->compile()->unwrap(); + + $this->assertSame(7, $before(['amount' => 7])->unwrap()->unwrap()); + $this->assertSame(7, $after(['amount' => 7])->unwrap()->unwrap()); + } +} diff --git a/tests/Rewrite/SourceDescendersTest.php b/tests/Rewrite/SourceDescendersTest.php new file mode 100644 index 0000000..81a70a3 --- /dev/null +++ b/tests/Rewrite/SourceDescendersTest.php @@ -0,0 +1,67 @@ +with(new BoxExtension()); + + $this->assertArrayHasKey(BoxSource::class, $descenders->sources); + $this->assertArrayHasKey(StaticSource::class, $descenders->sources, 'the core arms are always there'); + $this->assertArrayNotHasKey(BoxSource::class, SourceDescenders::core()->sources, 'joining derives a new registry'); + } + + #[Test] + public function an_extension_contributes_no_descent_arms_by_default(): void + { + $extension = new class extends Extension {}; + + $this->assertSame([], $extension->sourceDescenders()); + $this->assertSame(array_keys(SourceDescenders::core()->sources), array_keys(SourceDescenders::core()->with($extension)->sources)); + } + + #[Test] + public function two_extensions_claiming_one_class_is_a_configuration_error(): void + { + $this->expectException(InvalidArgumentException::class); + $this->expectExceptionMessage('Source class [' . BoxSource::class . '] has two descent arms; descent ownership is exact and extension order carries no precedence.'); + + SourceDescenders::core()->with(new BoxExtension(), new BoxExtension()); + } + + #[Test] + public function the_root_of_a_path_is_the_tree_itself(): void + { + $this->assertSame('$', SourcePath::root()->describe()); + } + + #[Test] + public function a_path_segment_cannot_be_empty(): void + { + $this->expectException(InvalidArgumentException::class); + $this->expectExceptionMessage('A source path segment names a property and cannot be empty.'); + + SourcePath::root()->child(''); + } +}