2.10.6. ПЕРЕСТРОЙКИ Тропа S : P R имеет следующий смысл. Следует вычислить источник S и сопоставить полученное объектное выражение Oe с образцом P. В результате получится, вообще говоря, несколько вариантов сопоставления. Затем следует попытаться найти самый первый из вариантов сопоставления, для которого вычисление хвоста R завершается успешно. Если хвост R является огражденной пустой тропой (всегда вырабатывающей пустое выражение), он может быть опущен. Для описания семантики перестройки нам понадобится следующее обозначение. Запись
EnvList,m,St ||- Q => X,St'
означает, что если тропа Q находится на уровне m, то результатом ее вычисления для списка сред EnvList является X.
Env,m,St |- Q => Oe,St'
----------------------------------
[Env]^EnvList,m,St ||- Q => Oe,St'
Env,m,St |- Q => $fail(0),St'
EnvList,m,St' ||- Q => X,St"
---------------------------------
[Env]^EnvList,m,St ||- Q => X,St"
Env,m,St |- Q => $fail(k+1),St'
------------------------------------------
[Env]^EnvList,m,St ||- Q => $fail(k+1),St'
Env,m,St |- Q => $error(Oe),St'
------------------------------------------
[Env]^EnvList,m,St ||- Q => $error(Oe),St'
[],m,St ||- Q => $fail(0),St.
Теперь мы можем описать семантику перестройки.
S : P =>=> S : P ,
Env,0,St |- S => Oe,St'
Env |- Oe : P => EnvList
EnvList,m,St' ||- R => X,St"
----------------------------
Env,m,St |- S : P R => X,St"
Env,0,St |- S => $fail(k),St'
-----------------------------------
Env,m,St |- S : P R => $fail(0),St'
Env,0,St |- S => $error(Oe),St'
-------------------------------------
Env,m,St |- S : P R => $error(Oe),St'
Например, вычисление приведенной ниже тропы заканчивается
неуспехом. При этом печатается цепочка литер 'CBA':
'ABC' : $r e sX e, <Print sX> $fail