Fix fuel implementation in PHP
This commit is contained in:
@@ -87,7 +87,7 @@ function cmdRun(string $bundlePath, array $args): void
|
||||
debugTime('built expression');
|
||||
|
||||
fwrite(STDERR, "Reducing kernel application...\n");
|
||||
$result = reduce($expr, 1_000_000);
|
||||
$result = reduce($expr, 1_000_000_000);
|
||||
debugTime('reduced kernel application');
|
||||
|
||||
[$kind, $value, $rest] = unwrapResult($result);
|
||||
|
||||
@@ -21,6 +21,14 @@ $GLOBALS['ARB_B'] = [0 => 0];
|
||||
$GLOBALS['ARB_NEXT'] = 1;
|
||||
$GLOBALS['ARB_CONS_CACHE'] = [];
|
||||
|
||||
function spendFuel(int &$fuel): void
|
||||
{
|
||||
if ($fuel <= 0) {
|
||||
throw new \RuntimeException('fuel exhausted');
|
||||
}
|
||||
$fuel--;
|
||||
}
|
||||
|
||||
function newNode(int $tag, int $a, int $b = 0): int
|
||||
{
|
||||
$id = $GLOBALS['ARB_NEXT']++;
|
||||
@@ -100,12 +108,12 @@ function newAppFast(int $f, int $x, array &$TAG, array &$A, array &$B): int
|
||||
return $id;
|
||||
}
|
||||
|
||||
function apply_(int $a, int $b, int $fuel = 1_000_000): int
|
||||
function apply_(int $a, int $b, int $fuel = 100_000_000_000_000_000): int
|
||||
{
|
||||
return reduce(app($a, $b), $fuel);
|
||||
}
|
||||
|
||||
function reduce(int $term, int $fuel = 1_000_000): int
|
||||
function reduce(int $term, int $fuel = 100_000_000_000_000_000): int
|
||||
{
|
||||
return whnf($term, $fuel);
|
||||
}
|
||||
@@ -167,6 +175,7 @@ function whnf(int $term, int &$fuel): int
|
||||
if ($left === 0) {
|
||||
$term = $right;
|
||||
if ($orig !== $term) { $TAG[$orig] = 4; $A[$orig] = $term; $B[$orig] = 0; }
|
||||
spendFuel($fuel);
|
||||
continue;
|
||||
}
|
||||
|
||||
@@ -178,6 +187,7 @@ function whnf(int $term, int &$fuel): int
|
||||
$TAG, $A, $B
|
||||
);
|
||||
if ($orig !== $term) { $TAG[$orig] = 4; $A[$orig] = $term; $B[$orig] = 0; }
|
||||
spendFuel($fuel);
|
||||
continue;
|
||||
}
|
||||
|
||||
@@ -195,6 +205,7 @@ function whnf(int $term, int &$fuel): int
|
||||
if ($arg === 0) {
|
||||
$term = $A[$left];
|
||||
if ($orig !== $term) { $TAG[$orig] = 4; $A[$orig] = $term; $B[$orig] = 0; }
|
||||
spendFuel($fuel);
|
||||
continue;
|
||||
}
|
||||
|
||||
@@ -202,6 +213,7 @@ function whnf(int $term, int &$fuel): int
|
||||
if ($atag === 1) {
|
||||
$term = newAppFast($B[$left], $A[$arg], $TAG, $A, $B);
|
||||
if ($orig !== $term) { $TAG[$orig] = 4; $A[$orig] = $term; $B[$orig] = 0; }
|
||||
spendFuel($fuel);
|
||||
continue;
|
||||
}
|
||||
|
||||
@@ -213,6 +225,7 @@ function whnf(int $term, int &$fuel): int
|
||||
$TAG, $A, $B
|
||||
);
|
||||
if ($orig !== $term) { $TAG[$orig] = 4; $A[$orig] = $term; $B[$orig] = 0; }
|
||||
spendFuel($fuel);
|
||||
continue;
|
||||
}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user