354 lines
7.4 KiB
PHP
354 lines
7.4 KiB
PHP
<?php
|
|
|
|
namespace alveolata\term;
|
|
|
|
// require_once(DIR_ALVEOLATA . '/definitions.php');
|
|
require_once(DIR_ALVEOLATA . '/log/functions.php');
|
|
require_once(DIR_ALVEOLATA . '/list/functions.php');
|
|
require_once(DIR_ALVEOLATA . '/term/interface.php');
|
|
require_once(DIR_ALVEOLATA . '/term/implementation-variable.php');
|
|
require_once(DIR_ALVEOLATA . '/term/implementation-function.php');
|
|
require_once(DIR_ALVEOLATA . '/term/functions.php');
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
class struct_substitution
|
|
{
|
|
|
|
/**
|
|
* @var map<string,interface_term>
|
|
* @author Christian Fraß
|
|
*/
|
|
public $mapping;
|
|
|
|
|
|
/**
|
|
* @param map<string,interface_term>
|
|
* @author Christian Fraß
|
|
*/
|
|
public function __construct(
|
|
array $mapping
|
|
)
|
|
{
|
|
$this->mapping = $mapping;
|
|
}
|
|
|
|
}
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
function _substitution_clone(
|
|
struct_substitution $substitution
|
|
) : struct_substitution
|
|
{
|
|
$mapping_ = [];
|
|
foreach ($substitution->mapping as $name => $term) {
|
|
$mapping[$name] = $term->clone_();
|
|
}
|
|
return (new struct_substitution($mapping_));
|
|
}
|
|
|
|
|
|
/**
|
|
* @return set<string>
|
|
* @author Christian Fraß
|
|
*/
|
|
function _substitution_domain(
|
|
struct_substitution $substitution
|
|
) : array
|
|
{
|
|
return array_keys($substitution->mapping);
|
|
}
|
|
|
|
|
|
/**
|
|
* @param set<string> $names
|
|
* @author Christian Fraß
|
|
*/
|
|
function _substitution_restricted(
|
|
struct_substitution $substitution,
|
|
array $set
|
|
) : struct_substitution
|
|
{
|
|
$mapping = [];
|
|
foreach ($substitution->mapping as $name => $term) {
|
|
if (in_array($name, $set)) {
|
|
$mapping[$name] = $term;
|
|
}
|
|
}
|
|
return (new struct_substitution($mapping));
|
|
}
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
function substitution_instance(
|
|
struct_substitution $substitution,
|
|
interface_term $term
|
|
) : interface_term
|
|
{
|
|
if ($term instanceof class_variable) {
|
|
$variable = $term;
|
|
return (
|
|
array_key_exists($variable->name, $substitution->mapping)
|
|
? $substitution->mapping[$variable->name]
|
|
: $term->clone_()
|
|
);
|
|
}
|
|
else if ($term instanceof class_function) {
|
|
$function = $term;
|
|
return (
|
|
new class_function(
|
|
$function->head,
|
|
\alveolata\list_\map(
|
|
$function->arguments,
|
|
function ($argument) use (&$substitution) {
|
|
return substitution_instance($substitution, $argument);
|
|
}
|
|
)
|
|
)
|
|
);
|
|
}
|
|
else {
|
|
throw (new \Exception('invalid term'));
|
|
}
|
|
}
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
function _substitution_compose(
|
|
struct_substitution $substitution1,
|
|
struct_substitution $substitution2
|
|
) : struct_substitution
|
|
{
|
|
$substitution3 = _substitution_clone($substitution1);
|
|
$domain1 = _substitution_domain($substitution1);
|
|
// überschreiben der vorhandenen Zuordnungen und entfernen der Identitäten
|
|
{
|
|
foreach ($domain1 as $name) {
|
|
$term = substitution_instance($substitution2, $substitution1->mapping[$name]);
|
|
if (equal(new class_variable($name), $term)) {
|
|
unset($substitution3->mapping[$name]);
|
|
}
|
|
else {
|
|
$substitution3->mapping[$name] = $term;
|
|
}
|
|
}
|
|
}
|
|
// hinzufügen der neuen Ersetzungen
|
|
{
|
|
$domain2 = _substitution_domain($substitution2);
|
|
foreach ($domain2 as $name) {
|
|
if (! in_array($name, $domain1)) {
|
|
$substitution3->mapping[$name] = $substitution2->mapping[$name];
|
|
}
|
|
}
|
|
}
|
|
return $substitution3;
|
|
}
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
function _substitution_empty(
|
|
) : struct_substitution
|
|
{
|
|
return (new struct_substitution([]));
|
|
}
|
|
|
|
|
|
/**
|
|
* ermittelt die anzuwendenen Substiutionen und die neuen Term-Paare für ein gegebenes Term-Paar
|
|
*
|
|
* @param record<first:interface_term,second:interface_term> $pair
|
|
* @return record<substitutions:list<struct_substitution>,pairs:list<record<first:interface_term,second:interface_term>>>
|
|
*/
|
|
function _unificationstep(
|
|
array $pair
|
|
) : array
|
|
{
|
|
$nothing = [
|
|
'substitutions' => [],
|
|
'pairs' => [],
|
|
];
|
|
if ($pair['first'] instanceof class_variable) {
|
|
$x_variable = $pair['first'];
|
|
if ($pair['second'] instanceof class_variable) {
|
|
$y_variable = $pair['second'];
|
|
return [
|
|
'substitutions' => \alveolata\list_\map(
|
|
[
|
|
['from' => $x_variable, 'to' => $y_variable],
|
|
['from' => $y_variable, 'to' => $x_variable],
|
|
],
|
|
function (array $satz) : struct_substitution {
|
|
$mapping = [];
|
|
if (! ($satz['from']->name === $satz['to']->name)) {
|
|
$mapping[$satz['from']->name] = $satz['to'];
|
|
}
|
|
else {
|
|
// do nothing
|
|
}
|
|
return (new struct_substitution($mapping));
|
|
}
|
|
),
|
|
'pairs' => [],
|
|
];
|
|
}
|
|
else {
|
|
if (contains($pair['second'], $x_variable)) {
|
|
return $nothing;
|
|
}
|
|
else {
|
|
return [
|
|
'substitutions' => [
|
|
new struct_substitution([$x_variable->name => $pair['second']]),
|
|
],
|
|
'pairs' => [],
|
|
];
|
|
}
|
|
}
|
|
}
|
|
else if ($pair['first'] instanceof class_function) {
|
|
$x_function = $pair['first'];
|
|
if ($pair['second'] instanceof class_variable) {
|
|
return [
|
|
'substitutions' => [_substitution_empty()],
|
|
'pairs' => ['first' => $pair['second'], 'second' => $pair['first']],
|
|
];
|
|
}
|
|
else if ($pair['second'] instanceof class_function) {
|
|
$y_function = $pair['second'];
|
|
if ($x_function->head === $y_function->head) {
|
|
if (count($x_function->arguments) === count($y_function->arguments)) {
|
|
return [
|
|
'substitutions' => [_substitution_empty()],
|
|
'pairs' => \alveolata\list_\zip(
|
|
$x_function->arguments,
|
|
$y_function->arguments,
|
|
false
|
|
),
|
|
];
|
|
}
|
|
else {
|
|
throw (new \Exception('ungleiche Anzahl an Argumenten bei Funktionen mit gleichem Kopf'));
|
|
}
|
|
}
|
|
else {
|
|
return $nothing;
|
|
}
|
|
}
|
|
else {
|
|
throw (new \Exception('ungültiger Term'));
|
|
}
|
|
}
|
|
else {
|
|
throw (new \Exception('ungültiger Term'));
|
|
}
|
|
}
|
|
|
|
|
|
/**
|
|
* ermittelt die Menge aller allgemeinsten unifiers
|
|
*
|
|
* @param list<record<first:interface_term,second:interface_term>> $problem
|
|
* @param int [$depth]
|
|
* @return list<struct_substitution>
|
|
* @author Christian Fraß
|
|
*/
|
|
function unifiers(
|
|
array $problem,
|
|
int $depth = 0
|
|
) : array
|
|
{
|
|
$solution = null;
|
|
if (empty($problem)) {
|
|
$solution = [_substitution_empty()];
|
|
}
|
|
else {
|
|
$components = [
|
|
'head' => $problem[0],
|
|
'rest' => array_slice($problem, 1),
|
|
];
|
|
$step = _unificationstep($components['head']);
|
|
$solution = \alveolata\list_\reduce(
|
|
$step['substitutions'],
|
|
[],
|
|
function (array $solution_, struct_substitution $substitution) use ($depth, &$components, &$step) {
|
|
$rest = \alveolata\list_\map(
|
|
$components['rest'],
|
|
function ($pair) use (&$substitution) {
|
|
return [
|
|
'first' => substitution_instance($substitution, $pair['first']),
|
|
'second' => substitution_instance($substitution, $pair['second']),
|
|
];
|
|
}
|
|
);
|
|
$subsolution = unifiers(
|
|
\alveolata\list_\concat($step['pairs'], $rest),
|
|
$depth+1
|
|
);
|
|
return \alveolata\list_\concat(
|
|
$solution_,
|
|
\alveolata\list_\map(
|
|
$subsolution,
|
|
function ($substitution_) use (&$substitution) {
|
|
return _substitution_compose($substitution, $substitution_);
|
|
}
|
|
)
|
|
);
|
|
}
|
|
);
|
|
}
|
|
\alveolata\log\debug(
|
|
'unification',
|
|
[
|
|
'problem' => implode(
|
|
' + ',
|
|
\alveolata\list_\map(
|
|
$problem,
|
|
function ($pair) {
|
|
return sprintf(
|
|
'[%s ~ %s]',
|
|
to_string($pair['first']),
|
|
to_string($pair['second'])
|
|
);
|
|
}
|
|
)
|
|
),
|
|
'solution' => $solution,
|
|
]
|
|
);
|
|
return $solution;
|
|
}
|
|
|
|
|
|
/**
|
|
* @author Christian Fraß
|
|
*/
|
|
function unifier(
|
|
interface_term $x,
|
|
interface_term $y
|
|
) : struct_substitution
|
|
{
|
|
return (
|
|
unifiers(
|
|
[
|
|
[
|
|
'first' => $x,
|
|
'second' => $y
|
|
]
|
|
]
|
|
)[0]
|
|
);
|
|
}
|
|
|
|
|