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