import	java.io.*;

/*
 *	Interface de base pour les arbres, on aura autant de dérivés que types d'opérateurs,
 *	et un pour les littéraux (pas de sous arbre, mais un index dans une table de chaînes).
 */

interface Arbre
{
	public void affiche ();		// affiche l'arbre.
	public Arbre getTerm1 ();	// retourne le premier terme.
	public Arbre getTerm2 ();	// retourne le deuxième terme.
}

/*
 *	Classe définissant les variables littérales.
 *	Le nom est stocké dans une table de hachage pour une
 *	recherche rapide.
 */

class Variable implements Arbre
{
	static final int	HSIZE = 1024;	// taille de la table de hachage.
	static Variable []	_hashtable = new Variable [HSIZE];

	private String	_nom;	// le nom de la variable.

	// construit un arbre du genre littéral à partir d'une chaîne de caractères.
	public Variable (String nom)
	{
		_nom = nom;
		name2var (nom, this);	// la mettre dans la table.
	}
	// affiche une variable.
	public void affiche ()
	{
		System.out.print (_nom);
	}
	// ne retourner aucun terme.
	public Arbre getTerm1 () { return null; }
	public Arbre getTerm2 () { return null; }
	// récupère une variable par son nom.
	public static Variable name2var (String nom)
	{
		return name2var (nom, null);
	}
	// affiche le contenu de la table de hachage.
	public static void affiche_htable ()
	{
		for (int i = HSIZE; --i >= 0;)
			if (_hashtable [i] != null)
				System.out.println (_hashtable [i]._nom + " [" + i + "]");
	}
	// cherche à partir du nom (et met si var != null) une variable dans la table.
	private static Variable name2var (String nom, Variable var)
	{
		int	h = hash (nom);

		for (int i = HSIZE; --i >= 0;) {	// au pire explorer toute la table.
			if (_hashtable [h] == null) {
				if (var == null)
					return null;	// pas trouvé.
				// a mettre dans la table.
				_hashtable [h] = var;
				return var;
			}
			if (_hashtable [h]._nom.equals (nom))
				return _hashtable [h];
	
			h = (h + 41) % HSIZE;	// collision: voir 41 cases plus loin.
		}
		return null;	// plus de place dans la table.
	}

	// fonction de hachage.
	private static int hash (String nom)
	{
		int	h = 11;						// n'importe quoi de non nul.
		byte []	tab = nom.getBytes ();	// tableau d'octets (comme en C).

		for (int i = 0; i < tab.length; ++i)
			h = ((h * 17) ^ (int) tab [i]) % HSIZE;
		if (h < 0)
			h += HSIZE;
		return h;
	}
}

/*
 *	Arbre de type (! terme)
 */

class Non implements Arbre
{
	private Arbre	_t;		// le terme à nier.

	public Non (Arbre t)
	{
		_t = t;
	}
	public void affiche ()
	{
		System.out.print ("!");
		_t.affiche ();
	}
	// retourne le premier terme.
	public Arbre getTerm1 () { return _t; }
	// retourne null (il n'y a pas de deuxième terme!)
	public Arbre getTerm2 () { return null; }
}

/*
 *	Arbre général a deux termes. (term1 op term2)
 */

abstract class Arbre2
{
	private Arbre	_p;			// premier terme.
	private Arbre	_q;			// deuxième terme.
	private String	_opstring;	// forme externe de l'opérateur.

	public Arbre2 (Arbre p, Arbre q, String op)
	{
		_p = p;
		_q = q;
		_opstring = op;
	}
	// affiche un tel arbre.
	public void affiche ()
	{
		System.out.print ("(");
		_p.affiche ();
		System.out.print (_opstring);
		_q.affiche ();
		System.out.print (")");
	}
	// retourne le premier terme.
	public Arbre getTerm1 () { return _p; }
	// retourne le deuxième terme.
	public Arbre getTerm2 () { return _q; }
}

/*
 *	Arbre de type (term1 -> terme2)
 */

class Implique extends Arbre2 implements Arbre
{
	public Implique (Arbre p, Arbre q) { super (p, q, " -> "); }
}

/*
 *	Arbre de type (term1 <-> terme2)
 */

class Equiv extends Arbre2 implements Arbre
{
	public Equiv (Arbre p, Arbre q) { super (p, q, " <-> "); }
}

/*
 *	Arbre de type (term1 & terme2)
 */

class Et extends Arbre2 implements Arbre
{
	public Et (Arbre p, Arbre q) { super (p, q, " & "); }
}

/*
 *	Arbre de type (term1 | terme2)
 */

class Ou extends Arbre2 implements Arbre
{
	public Ou (Arbre p, Arbre q) { super (p, q, " | "); }
}

/*
 *	Analyseur lexical et syntaxique.
 */


/*
 *	Exceptions.
 */

// erreur générique.

class ParseException extends Exception
{
	public ParseException (String s)
	{
		super (s);
	}
}

// erreur de syntaxe
class SyntaxErrorException extends ParseException
{
	public SyntaxErrorException (String s) {
		super (s);
	}
}

// symbole mal formé.
class BadTokenException extends ParseException
{
	public BadTokenException (String s)
	{
		super (s);
	}
}

/*
 *	Classe définissant une unité lexicale.
 */

class Token
{
	public static final int	EOF = -1;
	public static final int	ET = 0;
	public static final int	OU = 1;
	public static final int	IMPL = 2;
	public static final int	EQUIV = 3;
	public static final int	NON = 4;
	public static final int	LPAR = 5;
	public static final int	RPAR = 6;
	public static final int	VARIABLE = 7;

	int		_type;	// type de token.
	String	_s;		// valeur.

	public Token (int t, String s)
	{
		_type = t;
		_s = s;
	}
}

/*
 *	les analyseurs lexical et syntaxique.
 */

public class Parser
{
	Token			_ringur;	// token à relire.
	int				_save;		// caractère à relire.
	DataInputStream	_in;		// flot d'entrée.

	// constructeur à partir d'un flot d'entrée.
	public Parser (DataInputStream in)
	{
		_save = -1;
		_ringur = null;
		_in = in;
	}

	/*
	 *	Analyseur syntaxique LL(1) récursif descendant.
	 *	principe:
	 *		- une fonction par règle de la grammaire (ici un case par règle).
	 *		- chaque fonction 'sait' quoi faire au vu d'un token (le prochain).
	 *
	 *	e ::=	variable
	 *	   |	'!' e
	 *	   |	'(' e ')'
	 *	   |	'(' e '&' e ')'
	 *	   |	'(' e '|' e ')'
	 *	   |	'(' e '<->' e ')'
	 *	   |	'(' e '->' e ')'
	 */

	public Arbre parseExpr () throws ParseException
	{
		Token	t = nextToken ();
		Arbre	a;

		switch (t._type) {
			case Token.VARIABLE:
				return new Variable (t._s);

			case Token.NON:
				return new Non (parseExpr ());

			case Token.LPAR:
				a = parseExpr ();
				t = nextToken ();
				switch (t._type) {
					case Token.RPAR:
						return a;	// expression parenthésée.

					case Token.ET:
						a = new Et (a, parseExpr ());
						break;

					case Token.OU:
						a = new Ou (a, parseExpr ());
						break;

					case Token.EQUIV:
						a = new Equiv (a, parseExpr ());
						break;

					case Token.IMPL:
						a = new Implique (a, parseExpr ());
						break;

					default:
						throw new SyntaxErrorException ("Malformed expression");
				}
				t = nextToken ();
				if (t._type != Token.RPAR)
					throw new SyntaxErrorException (") expected");
				return a;

			default:
				throw new SyntaxErrorException ("'!', '(', or 'variable' expected");
		}
	}

	/*
	 *	Analyseur lexical
	 *		nextToken:	qui retourne le prochain mot.
	 *		pushToken:	qui remet un mot dans le flux d'entrée.
	 */

	// Réingurgite l'unité lexicale (profondeur 1 car l'anayseur syntaxique est LL(1)).
	public void pushToken (Token t)
	{
		_ringur = t;
	}
	// Lit un octet sur le flot d'entrée.
	private byte readByte () throws IOException
	{
		// avait-on lu un caractère de trop la fois précédente?
		if (_save != -1) {
			byte	b = (byte) _save;
			_save = -1;
			return b;
		}
		return _in.readByte ();
	}
	// Retourne l'unité lexicale suivante (l'exception est déclenchée en cas
	// d'unité mal formée).
	public Token nextToken () throws BadTokenException
	{
		byte	b;
		byte []	tab = new byte [512];
		int		i;

		// en avait-on lu un de trop la dernière fois ?
		if (_ringur != null) {
			Token	t = _ringur;
			_ringur = null;
			return t;
		}
		try {
			for (;;) switch (b = readByte ())
			{
				default:
					// tout accumuler dans tab, jusqu'à un séparateur.
					for (i = -1;
							b != ' ' &&
							b != '\n' &&
							b != '\t' &&
							b != '(' &&
							b != ')' &&
							b != '-' &&
							b != '&' &&
							b != '|' &&
							b != '<' &&
							b != '!'; b = readByte ())
						tab [++i] = b;
					_save = (int) b;	// sauver le caractère lu en trop.
					return new Token (Token.VARIABLE, new String (tab, 0, i+1));
				case ' ':
				case '\n':
				case '\t':
					continue;	// ignorer les espaces.

				case '(':	return new Token (Token.LPAR, null);
				case ')':	return new Token (Token.RPAR, null);
				case '!':	return new Token (Token.NON, null);
				case '&':	return new Token (Token.ET, null);
				case '|':	return new Token (Token.OU, null);
				case '<':
					if (readByte () != (byte) '-' ||
						readByte () != (byte) '>')
					{
						throw new BadTokenException ("<-> expected.");
					}
					return new Token (Token.EQUIV, null);
				case '-':
					if (readByte () != (byte) '>')
					{
						throw new BadTokenException ("-> expected.");
					}
					return new Token (Token.IMPL, null);
			
			}
		} catch (IOException e) {
			// fin de fichier.
			return new Token (Token.EOF, null);
		}
	}
}

/*
 *	Test du lecteur de formules.
 */

class Test {
	public static void main (String [] args)
	{
		// lire l'entrée standard (System.in)
		Parser	p = new Parser (new DataInputStream (System.in));
		Arbre	a;
		Token	t;

		for (;;) {	// pour recommencer en cas d'erreur de syntaxe.
			System.out.print ("? ");
			try {
				for (;;) {
					a = p.parseExpr ();
					System.out.print ("=> ");
					a.affiche ();
					if (a instanceof Et) {
						System.out.println ("\nc'est un ET");
						a.getTerm1 ().affiche ();
						System.out.println ();
						a.getTerm2 ().affiche (); 
					}
					System.out.print ("\n? ");
					t = p.nextToken ();
					if (t._type == Token.EOF)
						return;
					p.pushToken (t);
				}
			} catch (ParseException e) {
				// en cas d'erreur de syntaxe afficher le message correspondant.
				System.err.println (e);
				continue;	// ne pas se laisser abattre!
			}
		}
	}
}