*$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-переменных (типа строка).

  Задача суперкомпиляции --- проверить, возможно ли при определенном данным интерпретатором порядке развертки (слева направо) то,
  что значение переменной ys будет определено до того, как будет определено значение переменной xs.
  Остаточная программа, приведенная ниже, показывает, что это невозможно.

	$ENTRY Go {
    	  (e.101) =  False;
	}
*/

$ENTRY Go
  { (e.Rules)
	= <Eq (e.Rules ('xs -> empty'))<Sim <Encode ('xs ys A B A A A B = A B A A A B xs ys')>>>; /* квази-квадратичное, квадратичное */ 
  }

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);
}