/* 
  This is the interpreter of the word equations that checks whether, given an equation T and a computation path W,
  the equation T becomes a tautology after applying the computation.
  The entry point of the interpreter considers a computation path as a parameter given a fixed equation.
  As a result, a supercompiler constructs a simple program generating all solutions of the equation. 

  The resulting program for the equation x A y = y B x, for example, returns False on all the paths.
*/

/******************************************************************************************************/
/*                         The initial program (the interpreter)                                      */
/******************************************************************************************************/

/*
  Функция Eq принимает аргументы: (#e.Rules)(e.LHS)(e.RHS). 
  Параметр e.Rules --- путь по дереву решений уравнения. 
  e.LHS и e.RHS --- левая и правая часть уравнения, имеют одинаковый синтаксис.
  e.LHS ::= Symbol e.LHS || (var 'e' s.Name) e.LHS || пустая строка
*/

$ENTRY Go
  { (e.Rules)
	= <Eq (e.Rules) <Sim ((var 'e' x) A (var 'e' y))((var 'e' y) B (var 'e' x))>>;
  }

/*
Функция Eq осуществляет развертку уравнения согласно заданному пути и имеет входной формат: (#e.Rules)(e.LHS)(e.RHS). 
Параметр e.Rules – путь по дереву решений уравнения, 
  e.LHS и e.RHS – левая и правая части уравнения e.LHS = e.RHS имеют одинаковый синтаксис;
  e.LHS ::= Symbol e.LHS || (var s.Name) e.LHS || EMPTY 
*/
Eq {
/* 1. Если обе части уравнения пусты, получено тривиальное тождество и развертка завершается. 
  Считаем, что список правил, которые нужно применить к этому тождеству, также пуст. */
	(/* EMPTY */)(/*EMPTY*/)(/*EMPTY*/) = True;
/* 2а+4a+6a. Какова бы ни была правая часть уравнения, если левая начинается с е-переменной x, и правило преобразования есть x -> empty,
  тогда строим присваивание этой переменной значения, равного пустой строке, и осуществляем подстановку данного присваивания. */	
	((s.x TO empty) e.R1)(e.LHS)((var 'e' s.x) e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.x)(/* EMPTY */))(/*EMPTY*/)(e.LHS)>)
			(<subst (assign (var 'e' s.x)(/* EMPTY */))(/*EMPTY*/)(e.RHS)>)
		>>;
/* 2б+4б+6б. Какова бы ни была левая часть уравнения, если правая начинается с е-переменной x, и правило преобразования есть x -> empty, 
  тогда строим присваивание этой переменной значения, равного пустой строке, и осуществляем подстановку дного присваивания. */	
	((s.x TO empty) e.R1)((var 'e' s.x) e.LHS)(e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.x)(/* EMPTY */))(/*EMPTY*/)(e.LHS)>)
			(<subst (assign (var 'e' s.x)(/* EMPTY */))(/*EMPTY*/)(e.RHS)>)
		>>;
/* 3a. Если левая часть уравнения начинается с e-переменной x, а правая – с буквы s.Sym, 
  и правило преобразования есть x -> s.Sym x, осуществляем подстановку x := s.Sym++x. 
  После этого вызываем функцию упрощения уравнения (Sim). */
	((s.x TO s.Sym s.x) e.R1)((var 'e' s.x) e.LHS)(s.Sym e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.x)(s.Sym (var 'e' s.x)))((var 'e' s.x))(e.LHS)>)
			(<subst (assign (var 'e' s.x)(s.Sym (var 'e' s.x)))(/*EMPTY*/)(e.RHS)>)
		>>;
/* 3б. Если правая часть уравнения начинается с e-переменной x, а левая – с буквы s.Sym, 
  и правило преобразования есть x -> s.Sym x, осуществляем подстановку x := s.Sym++x. 
  После этого вызываем функцию упрощения уравнения (Sim). */
	((s.x TO s.Sym s.x) e.R1)(s.Sym e.LHS)((var 'e' s.x) e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.x)(s.Sym (var 'e' s.x)))(/*EMPTY*/)(e.LHS)>)
			(<subst (assign (var 'e' s.x)(s.Sym (var 'e' s.x)))((var 'e' s.x))(e.RHS)>)
		>>;
/* 5a. Если левая часть уравнения начинается с переменной x, а правая – с переменной y, и правило преобразования есть x -> y x, 
  осуществляем подстановку x:= y++x. После этого вызываем функцию упрощения уравнения. */
	((s.x TO s.y s.x) e.R1)((var 'e' s.x) e.LHS)((var 'e' s.y) e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.x)((var 'e' s.y) (var 'e' s.x)))((var 'e' s.x))(e.LHS)>)
			(<subst (assign (var 'e' s.x)((var 'e' s.y) (var 'e' s.x)))(/*EMPTY*/)(e.RHS)>)
		>>;
/* 5б. Если левая часть уравнения начинается с переменной x, а правая – с переменной y, и правило преобразования есть y -> x y, 
  осуществляем подстановку y:= x++y. После этого вызываем функцию упрощения уравнения. */
	((s.y TO s.x s.y) e.R1)((var 'e' s.x) e.LHS)((var 'e' s.y) e.RHS)
		= <Eq (e.R1) <Sim 
			(<subst (assign (var 'e' s.y)((var 'e' s.x)(var 'e' s.y)))(/*EMPTY*/)(e.LHS)>)
			(<subst (assign (var 'e' s.y)((var 'e' s.x) (var 'e' s.y)))((var 'e' s.y))(e.RHS)>)
		>>;
/* 7. Во всех прочих случаях считаем, что шаг решения уравнения невозможен. */
	(e.R1)e.Other = False;
}


/* Функция подстановки в выражение имеет входной формат:
   (assign (var s.name) (e.Val))(e.Result)(e.StringToSubstituteIn).
   Реализована хвостовой рекурсией: накапливает строку после подстановки в аргументе e.Result и возвращает ее всю целиком. */
subst {
	(assign t.var (e.val))(e.Result) (/*EMPTY*/) = e.Result;
/* Правило подстановки, не накладывающее запрет на обобщение. */
	(assign (var s.type s.n) (e.val))(e.Result) ((var s.type s.n) e.Rest) = <subst (assign (var s.type s.n) (e.val))(e.Result e.val) (e.Rest)>;
	(assign t.var (e.val))(e.Result) (t.other e.Rest) = <subst (assign t.var (e.val))(e.Result t.other) (e.Rest)>;
}

/* Функция упрощения удаляет одинаковые термы с левой и правой стороны уравнения. Имеет входной формат ((e.LHS)(e.RHS))^*. */
Sim {
  /* 1a. Удаление одинаковых букв слева и справа. */
	(s.x e.LHS)(s.x e.RHS)
		= <Sim (e.LHS)(e.RHS)>;
  /* 1б. Удаление одинаковых переменных. */
	((var s.type s.n) e.LHS)((var s.type s.n) e.RHS)
		= <Sim (e.LHS)(e.RHS)>;
  /* 2а. Уравнение преобразовано к тривиальному тождеству – возвращаем это тождество. */
	(/* EMPTY */)(/* EMPTY */)
		= (/* EMPTY */)(/* EMPTY */);
  /* 2б. Уравнение преобразовано к тривиальному противоречию (поскольку предложение 2б находится ниже, 
    чем предложение 1а, то s.x не совпадает с s.y) – возвращаем противоречивое уравнение и стираем все остальные уравнения в списке. */
	(s.x e.LHS)(s.y e.RHS)
		= (s.x)(s.y);
  /* 3. Результат преобразования уравнения не является тривиальным противоречием, и сокращать больше нечего – 
  возвращаем уравнение. */
	(e.x)(e.y)
		= (e.x)(e.y);
}

/***********************************************/
/*          the residual program               */
/***********************************************/

/*
$ENTRY Go {
 (e.x1) =  <Eq_2 e.x1>;
}


Eq_2 {
 (y TO empty) e.x1 =  <Eq_0 e.x1>;
 (x TO empty) e.x1 =  <Eq_1 e.x1>;
 (x TO y x) (x TO empty) e.x1 =  False;
 (x TO y x) (x TO B x) e.x1 =  <Eq_2 e.x1>;
 (x TO y x) e.x1 =  False;
 (y TO x y) (y TO empty) e.x1 =  False;
 (y TO x y) (y TO A y) e.x1 =  <Eq_2 e.x1>;
 (y TO x y) e.x1 =  False;
 e.x1 =  False;
}


Eq_0 {
 (x TO empty) e.x1 =  False;
 (x TO B x) e.x1 =  <Eq_0 e.x1>;
 e.x1 =  False;
}


Eq_1 {
 (y TO empty) e.x1 =  False;
 (y TO A y) e.x1 =  <Eq_1 e.x1>;
 e.x1 =  False;
}

*/