*$MST_FROM_ENTRY;
*$MATCHING ForRepeatedSpecialization;
*$STRATEGY Applicative;

/* Основной интерпретатор уравнений в словах, суперкомпиляция которого успешно строит граф решений для квадратичных уравнений. */
/*
  Параметр e.Rules --- путь по дереву решений уравнения. 
  Исходное уравнение, передаваемое в функцию Encode имеет синтаксис (e.LHS '=' e.RHS), где e.LHS и e.RHS имеют одинаковый синтаксис, 
  определенный следующими правилами. 
  e.LHS ::= s.Symbol' 'e.LHS || s.VarName's 'e.LHS || s.Symbol|| s.VarName's'|| пустая строка
  s.Symbol --- буква 'A'...'H' (переопределяется функцией Alphabet).
  s.VarName --- буква 'x', 'y', 'z', 'w', 'v', 'u' (переопределяется функцией Variables).
  s.VarName++'s' --- кодировка для e-переменных (типа строка).
*/

$ENTRY Go
  { (e.Rules)
	= <Eq (e.Rules)<Sim <Encode ('xs ys A B A A A B = A B A A A B xs ys')>>>; /* квази-квадратичное, квадратичное */ 
*	= <Eq (e.Rules)<Sim <Encode ('xs zs ys A B A A A B = A B A A A B xs zs ys')>>>; /* квази-квадратичное, квадратичное */ 
*	= <Eq (e.Rules)<Sim <Encode ('xs A A B A B ys A B = A B ys zs A B A B xs')>>>; /* квадратичное */  /* проверить вручную! */
*	= <Eq (e.Rules) <Sim <Encode ('xs A ys = ys A xs')>>>; /* квадратичное */
*	= <Eq (e.Rules) <Sim <Encode ('xs ys zs = zs ys xs')>>>; /* квадратичное бескоэффициентное */
*	= <Eq (e.Rules) <Sim <Encode ('xs = xs ys')>>>; /* квадратичное некорректное */
*	= <Eq (e.Rules) <Sim <Encode (' = xs xs ys xs')>>>; /* линейное слева с разделенными переменными -1 */
*	= <Eq (e.Rules) <Sim <Encode ('xs ys = zs zs zs')>>>; /* линейное слева с разделенными переменными -2*/
  }

Const__ { e.x = e.x;}

/* Главная функция перекодировки уравнения из пользовательского формата во внутренний формат интерпретатора. */
Encode {
	(e.Left'='e.Right) = (<Translate e.Left>)(<Translate e.Right>);
}

/* Список всех литералов, которые могут выступать в качестве имен переменных. */
Variables {
	= 'xyzwvu';
}

/* Список всех литералов, которые могут выступать в качестве букв алфавита констант. */
Alphabet {
	= 'ABCDEFGH'; 
}

IfInSet {
	s.Term (s.Term e.Rest) = 'T';
	s.Term ( ) = 'F';
	s.Term (s.OtherTerm e.Rest) = <IfInSet s.Term (e.Rest)>;
}

Translate {
	/* EMPTY */ = /* EMPTY */;
	' 'e.x = <Translate e.x>;
	e.x' ' = <Translate e.x>;
	Started (e.Result) 'TF'(e.variables)(e.alphabet)s.Name's'
		= e.Result (var 'e' s.Name);
	Started (e.Result) 'TF'(e.variables)(e.alphabet)s.Name
		=  e.Result (var 's' s.Name);
	Started (e.Result)'FT'(e.variables)(e.alphabet)s.Name
		= e.Result s.Name;
	Started (e.Result)'TF'(e.variables)(e.alphabet)s.Name's ' s.Next e.Rest
		= <Translate Started (e.Result (var 'e' s.Name))
			<IfInSet s.Next(e.variables)><IfInSet s.Next(e.alphabet)>(e.variables)(e.alphabet) s.Next e.Rest>;
	Started (e.Result)'TF'(e.variables)(e.alphabet)s.Name' 's.Next e.Rest
		= <Translate Started (e.Result (var 's' s.Name))
			<IfInSet s.Next(e.variables)><IfInSet s.Next(e.alphabet)>(e.variables)(e.alphabet)s.Next e.Rest>;
	Started (e.Result)'FT'(e.variables)(e.alphabet)s.Name' 's.Next e.Rest
		= <Translate Started (e.Result s.Name)
			<IfInSet s.Next(e.variables)><IfInSet s.Next(e.alphabet)>(e.variables)(e.alphabet)s.Next e.Rest>;
	s.Term e.Rest = <Translate Started ( ) 
		<IfInSet s.Term(<Variables>)><IfInSet s.Term(<Alphabet>)>
		(<Variables>)(<Alphabet>) s.Term e.Rest>;
}

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