Skip to content

Commit

Permalink
add proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
Baptouuuu committed Nov 4, 2023
1 parent 5eeac32 commit 130afca
Show file tree
Hide file tree
Showing 7 changed files with 288 additions and 9 deletions.
51 changes: 51 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,57 @@ name: CI
on: [push, pull_request]

jobs:
blackbox:
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macOS-latest]
php-version: ['8.2', '8.3']
dependency-versions: ['lowest', 'highest']
name: 'BlackBox'
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Setup PHP
uses: shivammathur/setup-php@v2
with:
php-version: ${{ matrix.php-version }}
extensions: mbstring, intl
coverage: none
- name: Composer
uses: "ramsey/composer-install@v2"
with:
dependency-versions: ${{ matrix.dependencies }}
- name: BlackBox
run: php blackbox.php
coverage:
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macOS-latest]
php-version: ['8.2', '8.3']
dependency-versions: ['lowest', 'highest']
name: 'Coverage'
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Setup PHP
uses: shivammathur/setup-php@v2
with:
php-version: ${{ matrix.php-version }}
extensions: mbstring, intl
coverage: xdebug
- name: Composer
uses: "ramsey/composer-install@v2"
with:
dependency-versions: ${{ matrix.dependencies }}
- name: BlackBox
run: php blackbox.php
env:
ENABLE_COVERAGE: 'true'
- uses: codecov/codecov-action@v1
with:
token: ${{ secrets.CODECOV_TOKEN }}
psalm:
runs-on: ubuntu-latest
strategy:
Expand Down
2 changes: 1 addition & 1 deletion .php-cs-fixer.dist.php
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<?php

return Innmind\CodingStandard\CodingStandard::config([
'tests',
'proofs',
'src',
]);
27 changes: 27 additions & 0 deletions blackbox.php
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
<?php
declare(strict_types = 1);

require 'vendor/autoload.php';

use Innmind\BlackBox\{
Application,
Runner\Load,
Runner\CodeCoverage,
};

Application::new($argv)
->when(
\getenv('ENABLE_COVERAGE') !== false,
static fn(Application $app) => $app
->codeCoverage(
CodeCoverage::of(
__DIR__.'/src/',
__DIR__.'/proofs/',
)
->dumpTo('coverage.clover')
->enableWhen(true),
)
->scenariiPerProof(1),
)
->tryToProve(Load::everythingIn(__DIR__.'/proofs/'))
->exit();
179 changes: 179 additions & 0 deletions proofs/functional.php
Original file line number Diff line number Diff line change
@@ -0,0 +1,179 @@
<?php
declare(strict_types = 1);

use Innmind\Mantle\{
Forerunner,
Source\Predetermined,
Task,
};
use Innmind\OperatingSystem\Factory;
use Innmind\TimeContinuum\Earth\Period\Second;
use Innmind\Filesystem\Name;
use Innmind\Url\Path;
use Innmind\Immutable\Sequence;
use Innmind\BlackBox\Set;
use Innmind\BlackBox\Tag;

return static function() {
yield test(
'Halting multiple tasks',
static function($assert) {
$expect = $assert->time(static function() {
Forerunner::of(Factory::build())(null, Predetermined::of(
static fn($os) => $os->process()->halt(Second::of(1)),
static fn($os) => $os->process()->halt(Second::of(1)),
static fn($os) => $os->process()->halt(Second::of(1)),
));
});
$expect
->inLessThan()
->seconds(2);
$expect
->inMoreThan()
->seconds(1);
},
);

yield proof(
'Carry value via the source',
given(
Set\Type::any(),
Set\Type::any(),
),
static function($assert, $initial, $modified) {
$returned = Forerunner::of(Factory::build())(
$initial,
static fn($_, $__, $continuation) => $continuation->terminate(),
);
$assert->same($initial, $returned);

$returned = Forerunner::of(Factory::build())(
$initial,
static fn($carry, $__, $continuation) => $continuation
->carryWith($initial)
->terminate(),
);
$assert->same($initial, $returned);

$returned = Forerunner::of(Factory::build())(
$initial,
static fn($carry, $__, $continuation) => $continuation
->carryWith($modified)
->terminate(),
);
$assert->same($modified, $returned);
},
);

yield test(
'The source is run asynchronously',
static function($assert) {
$expect = $assert->time(static function() {
Forerunner::of(Factory::build())(
false,
static fn($started, $os, $continuation, $results) => match ([$started, $results->size()]) {
[false, 0] => $continuation
->launch(Sequence::of(
Task::of(static function($os) {
$os->process()->halt(Second::of(1));
$os->process()->halt(Second::of(1));
}),
Task::of(static function($os) {
$os->process()->halt(Second::of(1));
$os->process()->halt(Second::of(1));
}),
Task::of(static function($os) {
$os->process()->halt(Second::of(1));
$os->process()->halt(Second::of(1));
}),
))
->carryWith(true),
[true, 0] => (static function($os, $continuation) {
// this halt is executed at the same time at the
// second one in each task
$os->process()->halt(Second::of(1));

return $continuation;
})($os, $continuation),
default => $continuation->terminate(),
},
);
});
$expect
->inLessThan()
->seconds(3);
$expect
->inMoreThan()
->seconds(2);
},
);

yield test(
'Streams are handled asynchronously',
static function($assert) {
$lines = [];
Forerunner::of(Factory::build())(null, Predetermined::of(
static function($os) use ($assert, &$lines) {
$file = $os
->filesystem()
->mount(Path::of('./'))
->get(Name::of('composer.json'))
->match(
static fn($file) => $file,
static fn() => null,
);
$assert->not()->null($file);
$lines[] = $file
->content()
->lines()
->first()
->match(
static fn($line) => $line->toString(),
static fn() => null,
);
$lines[] = $file
->content()
->lines()
->filter(static fn($line) => !$line->str()->empty())
->last()
->match(
static fn($line) => $line->toString(),
static fn() => null,
);
},
static function($os) use ($assert, &$lines) {
$file = $os
->filesystem()
->mount(Path::of('./'))
->get(Name::of('LICENSE'))
->match(
static fn($file) => $file,
static fn() => null,
);
$assert->not()->null($file);
$lines[] = $file
->content()
->lines()
->first()
->match(
static fn($line) => $line->toString(),
static fn() => null,
);
$lines[] = $file
->content()
->lines()
->filter(static fn($line) => !$line->str()->empty())
->last()
->match(
static fn($line) => $line->toString(),
static fn() => null,
);
},
));
$assert->same(
['{', 'MIT License', 'SOFTWARE.', '}'],
$lines,
);
},
)->tag(Tag::wip);
};
20 changes: 20 additions & 0 deletions src/Source/Context.php
Original file line number Diff line number Diff line change
Expand Up @@ -70,12 +70,32 @@ public static function of(Source $source, mixed $carry): self

/**
* @param Sequence<R> $results
*
* @return self<C, R>
*/
public function withResults(Sequence $results): self
{
return new self($this->source, $this->continuation, $results);
}

/**
* @template R1
* @template R2
*
* @param callable(Source<C, R>, C): R1 $resume
* @param callable(C): R2 $terminate
*
* @return R1|R2
*/
public function match(callable $resume, callable $terminate): mixed
{
/** @psalm-suppress MixedArgument */
return $this->continuation->match(
fn($carry) => $resume($this->source, $carry),
static fn($carry) => $terminate($carry),
);
}

/**
* @return Continuation<C, R>
*/
Expand Down
3 changes: 1 addition & 2 deletions src/Tasks.php
Original file line number Diff line number Diff line change
Expand Up @@ -112,9 +112,8 @@ public function continue(OperatingSystem $os): self
$source = $source->flatMap(static fn($task) => match (true) {
$task instanceof Task\Terminated && $task->returned() instanceof Context => $task
->returned()
->continuation()
->match(
static fn() => Either::right($task->returned()),
static fn($source, $carry) => Either::right(Context::of($source, $carry)),
static fn($carry) => Either::left($carry),
),
default => Either::right($task),
Expand Down
15 changes: 9 additions & 6 deletions src/Wait.php
Original file line number Diff line number Diff line change
Expand Up @@ -116,12 +116,15 @@ public function __invoke(): array
static fn() => null,
);
/** @psalm-suppress InvalidArgument */
$watch = $this
->os
->sockets()
->watch($timeout)
->forRead(...$forRead->toList())
->forWrite(...$forWrite->toList());
$watch = $this->os->sockets()->watch($timeout);
$watch = $forRead->sort(fn($a, $b) => 0)->match(
static fn($read, $rest) => $watch->forRead($read, ...$rest->toList()),
static fn() => $watch,
);
$watch = $forWrite->sort(fn($a, $b) => 0)->match(
static fn($write, $rest) => $watch->forWrite($write, ...$rest->toList()),
static fn() => $watch,
);

$ready = $watch();
$took = $this->os->clock()->now()->elapsedSince($started);
Expand Down

0 comments on commit 130afca

Please sign in to comment.