/*
**	axioms.c
**
*/

#include <X11/Intrinsic.h>
#include <X11/Shell.h>
#include <X11/Command.h>
#include <X11/Dialog.h>
#include <X11/StringDefs.h>
#include <X11/List.h>
#include <X11/Form.h>
#include "xmagic.h"
#include <stdio.h>

#define  XtNinput	"input"

#define  OK		0
#define  DONE		5
#define  NO_FAIR	1
#define  F_LOGIC	2
#define  ILLEGAL	3
#define  ACCEPTD	4

char     *axiom [] =    {" 1: p v ~p",
			 " 2: (p & ~p) -> q",
			 " 3: (p & ~p) -> (q v ~q)",
		         " 4: (p & (p -> q)) -> q",
		         " 5: p -> (q -> p)",
		         " 6: p -> (q -> q)",
		         " 7: p -> (p -> p)",
		         " 8: (p -> ~p) -> ~p",
		         " 9: (t -> p) -> p; <=> ((p -> p) -> q) -> q",
			 "10: p -> (t -> p)",
			 "11: p v (p -> q)",
			 "12: T ->. F -> F",
			 "13: (q -> p) -> ((p -> q) -> (p -> q))",
			 "14: (p -> q) -> ((q -> r) -> (p -> r))",
			 "15: p -> ((p -> q) -> q)",
			 "16: (p -> (p -> q)) -> (p -> q)",
			 "17: (p -> (q -> r)) -> (q -> (p -> r))",
			 "18: ((p -> q) & (q -> r)) -> (p -> r)",
			 "19:                                        ",
			 "20:                                        ",
			 "21:                                        ",
			 "22:                                        ",
			 "23:                                        ",};

int      last_state [NO_OF_AXIOMS] = {0,};
Widget	 global_axiom_dialog, global_axiom_dialog_pop_up;

void make_add_axioms (the_shell)

Widget	the_shell;

{
	Widget	def_axiom_dialog, axiom_dialog_pop_up, the_form,
		axiom_label, axiom_list;
	extern void make_axiom_dialog (), make_axioms ();

	axiom_dialog_pop_up = XtCreatePopupShell ("xmagic: define axiom",
				topLevelShellWidgetClass, the_shell, NULL,
				0);
	global_axiom_dialog_pop_up = axiom_dialog_pop_up;
	make_axiom_dialog (axiom_dialog_pop_up, &def_axiom_dialog);
	global_axiom_dialog = def_axiom_dialog;
	the_form = XtCreateManagedWidget ("the_form", formWidgetClass,
			the_shell, NULL, 0);
	make_axioms (the_form, &axiom_label, &axiom_list, NULL, 4, NULL, 4);
}
	

void make_switch (parent_widget, 
		switch_widget, switch_name, switch_list, switch_calls, active,
		left_neighbour, left_distance, top_neighbour, top_distance)

Widget		parent_widget, *switch_widget, left_neighbour, top_neighbour;
String		switch_name;
XtCallbackRec	switch_calls [];
String		switch_list [];
int		left_distance, top_distance;
Boolean		active;

{
	int	i;
	Arg	switch_args [30];
	static String
		switch_translations = "<Btn1Down>,<Btn1Up>:	Set() Notify()";
	static XtTranslations	
		translation_table;
		
	translation_table = XtParseTranslationTable (switch_translations);
	i = 0;
	XtSetArg (switch_args [i], XtNtranslations, 
					(XtArgVal) translation_table);
	i++;
	XtSetArg (switch_args [i], XtNcallback, (XtArgVal) switch_calls);
	i++;
	XtSetArg (switch_args [i], XtNverticalList, (XtArgVal) True);
	i++;
	XtSetArg (switch_args [i], XtNdefaultColumns, (XtArgVal) 1);
	i++;
	XtSetArg (switch_args [i], XtNlist, (XtArgVal) switch_list);
	i++;
	XtSetArg (switch_args [i], XtNnumberStrings, (XtArgVal) 1);
	i++;
	XtSetArg (switch_args [i], XtNborderWidth, (XtArgVal) 0);
	i++;
	XtSetArg (switch_args [i], XtNinternalHeight, (XtArgVal) 0);
	i++;
	XtSetArg (switch_args [i], XtNsensitive, (XtArgVal) active);
	i++;
	XtSetArg (switch_args [i], XtNfromVert, (XtArgVal) top_neighbour);
	i++;
	XtSetArg (switch_args [i], XtNvertDistance, (XtArgVal) top_distance);
	i++;
	XtSetArg (switch_args [i], XtNfromHoriz, (XtArgVal) left_neighbour);
	i++;
	XtSetArg (switch_args [i], XtNhorizDistance, (XtArgVal) left_distance);
	i++;
	*switch_widget = XtCreateManagedWidget (switch_name, listWidgetClass, 
				parent_widget, switch_args, i);
}


Widget	global_axiom_widget [5], global_axiom_button;
static  Widget
	axiom_widget [NO_OF_AXIOMS];

void make_axioms (parent_widget, label_widget, axiom_form, 
		left_neighbour, left_distance, top_neighbour, top_distance)

Widget		parent_widget, *label_widget, *axiom_form,
		left_neighbour, top_neighbour;
int		left_distance, top_distance;

/*
**	This function makes the whole stack of one-element-long lists
*/

{
	void	axiom_action (), axiom_button_action (), go_away_action ();
	int	i;
	Arg	label_args [30], form_args [30];
	Widget	axiom_button, go_away_button;
	static XtCallbackRec
		axiom_calls [] = {{axiom_action, NULL}, {NULL, NULL},},
		axiom_button_calls [] =
				 {{axiom_button_action, NULL}, {NULL, NULL},},
		go_away_button_calls [] =
				 {{go_away_action, NULL}, {NULL, NULL},};
	char 	axiom_name [256] [NO_OF_AXIOMS];
	
	i = 0;
	XtSetArg (label_args [i], XtNlabel, (XtArgVal) "add axioms:");
	i++;
	XtSetArg (label_args [i], XtNborderWidth, (XtArgVal) 0);
	i++;
	XtSetArg (label_args [i], XtNfromVert, (XtArgVal) top_neighbour);
	i++;
	XtSetArg (label_args [i], XtNvertDistance, (XtArgVal) top_distance);
	i++;
	XtSetArg (label_args [i], XtNfromHoriz, (XtArgVal) left_neighbour);
	i++;
	XtSetArg (label_args [i], XtNhorizDistance, (XtArgVal) left_distance);
	i++;
	*label_widget = XtCreateManagedWidget ("add axioms:",
			labelWidgetClass, parent_widget, label_args, i);

	i = 0;
	XtSetArg (form_args [i], XtNfromVert, (XtArgVal) *label_widget);
	i++;
	XtSetArg (form_args [i], XtNfromHoriz, (XtArgVal) left_neighbour);
	i++;
	XtSetArg (form_args [i], XtNhorizDistance, (XtArgVal) left_distance);
	i++;
	XtSetArg (form_args [i], XtNdefaultDistance, (XtArgVal) 2);
	i++;
	*axiom_form = XtCreateManagedWidget ("axiom_form", formWidgetClass,
				parent_widget, form_args, i);

	sprintf (&(axiom_name [0][0]), "axiom_%d", 0);
	make_switch (*axiom_form, 
		&axiom_widget [0], &(axiom_name [0][0]), &(axiom [0]), 
		axiom_calls, True, NULL, 0, NULL, 1);

	for (i = 1; i < BUILT_IN_AXIOMS; i++) {
		sprintf (&(axiom_name [0][i]), "axiom_%d", i);
		make_switch (*axiom_form,
			&axiom_widget [i], &(axiom_name [0][i]), 
			&(axiom [i]), axiom_calls, True,
			NULL, 0, axiom_widget [i-1], 0);
	}
	for (i = BUILT_IN_AXIOMS; i < NO_OF_AXIOMS; i++) {
		sprintf (&(axiom_name [0][i]), "axiom_%d", i);
		make_switch (*axiom_form,
			&axiom_widget [i], &(axiom_name [0][i]),
			&(axiom [i]), axiom_calls, False,
			NULL, 0, axiom_widget [i-1], 0);
		global_axiom_widget [i-BUILT_IN_AXIOMS] = axiom_widget [i];
	}


	make_button (parent_widget, 
			&axiom_button, "axiom_button", "define axiom",
			axiom_button_calls,
			*label_widget, 19, top_neighbour, top_distance);
	global_axiom_button = axiom_button;

	make_button (parent_widget,
			&go_away_button, "go_away_button", "close window",
			go_away_button_calls,
			axiom_button, 19, top_neighbour, top_distance);
}

void make_axiom_dialog (parent_widget, axiom_dialog)

Widget	parent_widget, *axiom_dialog;

{
	int 		i;
	Arg		dialog_args [30];
	char		axiom_value [256];
	extern	void	add_action (), close_action ();
	Widget		button_18, button_19, button_20, button_21,
			button_22, go_away_button;
	static	XtCallbackRec
			button_18_calls [] = {{add_action, (caddr_t) 18},
						{NULL, NULL},},
			button_19_calls [] = {{add_action, (caddr_t) 19},
					{NULL, NULL},},
			button_20_calls [] = {{add_action, (caddr_t) 20},
						{NULL, NULL},},
			button_21_calls [] = {{add_action, (caddr_t) 21},
						{NULL, NULL},},
			button_22_calls [] = {{add_action, (caddr_t) 22},
						{NULL, NULL},},
			close_window_calls []
					   = {{close_action, NULL},
						{NULL, NULL},};

/*
**	Initialize axiom_value to be empty
*/
	axiom_value [0] = '\0';
/*
**	Set up other arguments to XtCreateManagedWidget
*/
	i = 0;
	XtSetArg (dialog_args [i], XtNlabel, (XtArgVal) 
			"define axiom:                                      ");
	i++;
	XtSetArg (dialog_args [i], XtNvalue, (XtArgVal) axiom_value);
	i++;
	XtSetArg (dialog_args [i], XtNinput, (XtArgVal) True);
	i++;

	*axiom_dialog = XtCreateManagedWidget ("axiom_dialog",
				dialogWidgetClass, parent_widget,
				dialog_args, i);
	
	make_button (*axiom_dialog, &button_18, "18", "19", button_18_calls,
			NULL, 4, NULL, 4);
	make_button (*axiom_dialog, &button_19, "19", "20", button_19_calls,
			NULL, 4, NULL, 4);
	make_button (*axiom_dialog, &button_20, "20", "21", button_20_calls,
			NULL, 4, NULL, 4);
	make_button (*axiom_dialog, &button_21, "21", "22", button_21_calls,
			NULL, 4, NULL, 4);
	make_button (*axiom_dialog, &button_22, "22", "23", button_22_calls,
			NULL, 4, NULL, 4);

	make_button (*axiom_dialog, &go_away_button, "close window",
			"close window", close_window_calls,
			NULL, 4, NULL, 4);
}

static void close_action (the_button, client_data, call_data)

Widget	the_button;
caddr_t	client_data, call_data;

{
	XtPopdown (global_axiom_dialog_pop_up);
	XtSetSensitive (global_axiom_button, True);
}

static void go_away_action (the_button, client_data, call_data)

Widget	the_button;
caddr_t	client_data, call_data;

{
	extern Widget	global_super_axiom_button;
			/* defined in xmagic.c */

	XtPopdown (the_global_pop_up);
	XtSetSensitive (global_super_axiom_button, True);
}

int		pre_axiom_count = 0, def_axiom_count = 0;
static int	def_axiom_index [DEF_AXIOMS];
static char	def_axiom_formula [DEF_AXIOMS][256];

void axiom_action (the_switch, client_data, the_item)

Widget			the_switch;
caddr_t			client_data;
XtListReturnStruct	*the_item;

{
	char		the_line [256];
	extern void	ring (), send_to_magic ();
	extern int	receive_all ();
	int		i, j;
	extern String	extra_string;


	for (i = 0; i < NO_OF_AXIOMS; i++) { 
		if (strcmp (the_item->string, axiom [i]) == 0) {
			if (last_state [i] == 0) {
				XtListHighlight (the_switch, the_item->list_index);
				if (i <= 17) {
					sprintf (the_line, "A\n%d\n", i+1);
					pre_axiom_count++;
				}
				else {
					sprintf (the_line, "A\n19\n%s\n",
					  &def_axiom_formula [i -
						BUILT_IN_AXIOMS][0]);
					def_axiom_index [i - BUILT_IN_AXIOMS] =
					  def_axiom_count++;
				}
				send_to_magic (the_line);
#ifdef DEBUG
				fprintf (stderr, the_line); fflush (stderr);
#endif
				if (receive_all () == ILLEGAL) {
					ring ();
					XtListUnhighlight (the_switch, 
						the_item->list_index); 
					last_state [i] = 0;
					if (i <= 17)
						pre_axiom_count--;
					else {
						def_axiom_index [i - 
						   BUILT_IN_AXIOMS] = 0;
						def_axiom_count--;
					send_to_magic ("N\n");
					receive_all ();
					}
				}
				else {
					last_state [i] = 1; 
					if (i > 17) {
					  strcpy (&def_axiom_formula [i - 
					    BUILT_IN_AXIOMS][0], extra_string);
					  sprintf (axiom [i], "%d: %s\0", 
					    i + 1, &def_axiom_formula 
					    [i - BUILT_IN_AXIOMS][0]);
					  XawListChange (global_axiom_widget [i
					    - BUILT_IN_AXIOMS], &(axiom[i]), 1,
					    0, True);
					  XawListHighlight (the_switch,
					    the_item->list_index);

					}
				}
			}
			else {
				XtListUnhighlight (the_switch);
				if (i <= 17) {
					if (pre_axiom_count < 2)
						sprintf (the_line, 
						   "D\na\n");
					else
						sprintf (the_line, 
						   "D\na\n%d\n", i+1);
					pre_axiom_count--;
				}
				else {
					if (def_axiom_count < 2)
						sprintf (the_line, 
						   "D\nc\n");
					else {
					  sprintf (the_line, "D\nc\n%d\n", 
					      def_axiom_index [i - 
					      BUILT_IN_AXIOMS] + 1);
					  for (j = 0; j < DEF_AXIOMS; j++) 
					      if (def_axiom_index [j] > 
					        def_axiom_index [i - 
					        BUILT_IN_AXIOMS])
					      def_axiom_index [j] --;
					}
					def_axiom_count--;
				}
				send_to_magic (the_line);
#ifdef DEBUG
				fprintf (stderr, the_line); fflush (stderr);
#endif
				last_state [i] = 0; 
				receive_all (); 
			}
		}
	}
}

void axiom_button_action (the_button, client_data, call_data)

Widget	the_button;
caddr_t	client_data, call_data;

{
	XtSetSensitive (the_button, False);
	XtPopup (global_axiom_dialog_pop_up, XtGrabNone);
}

Boolean	axioms_up = False;

void main_axiom_button_action (the_button, client_data, call_data)

Widget	the_button;
caddr_t client_data, call_data;

{	
	extern Boolean axioms_up;

	XtSetSensitive (the_button, False);
	XtPopup (the_global_pop_up, XtGrabNone);
	axioms_up = True;
}

void add_action (the_dialog, axiom_number, c2)

Widget the_dialog;
int axiom_number; 
caddr_t c2;

{
	char	the_line [256];
	int	j;
	extern String
		extra_string;
/*
**	sprintf (the_line, "define new axiom = %d: %s\n", axiom_number,
**		XtDialogGetValueString (global_axiom_dialog));
**	send_to_magic (the_line);
**	receive_all ();
*/
	strcpy (&def_axiom_formula [axiom_number - BUILT_IN_AXIOMS][0], 
		XtDialogGetValueString (global_axiom_dialog));
	sprintf (axiom [axiom_number], "%d: %s\0", axiom_number + 1, 
		&def_axiom_formula [axiom_number - BUILT_IN_AXIOMS][0]);
	XtListChange (global_axiom_widget [axiom_number - BUILT_IN_AXIOMS],
		&(axiom [axiom_number]), 1, 0, True);
	XtSetSensitive (global_axiom_widget [axiom_number - BUILT_IN_AXIOMS], 
		True);
	if (last_state [axiom_number] == 1) {
		/*
		**	Then we must delete the old axiom and put the
		**	new one in its place! This is the same stuff
		**	As in axiom_action ().
		*/

		XtListHighlight (global_axiom_widget [axiom_number -
			BUILT_IN_AXIOMS], 0);

		/*
		**	Delete the axiom
		*/
		
		if (def_axiom_count < 2)
			sprintf (the_line, "D\nc\n");
		else {
			sprintf (the_line, "D\nc\n%d\n", 
				def_axiom_index [axiom_number -
				BUILT_IN_AXIOMS] + 1);
			for (j = 0; j < DEF_AXIOMS; j++)
				if (def_axiom_index [j] >
				    def_axiom_index [axiom_number -
				    BUILT_IN_AXIOMS])
					def_axiom_index [j] --;
		}
		def_axiom_count --;
		send_to_magic (the_line);
		receive_all ();

		/*
		**	Add the axiom
		*/

		sprintf (the_line, "A\n19\n%s\n", &def_axiom_formula
			[axiom_number - BUILT_IN_AXIOMS][0]);
		def_axiom_index [axiom_number - BUILT_IN_AXIOMS] = 
			def_axiom_count++;
		send_to_magic (the_line);
		if (receive_all () == ILLEGAL) {
			XtListUnhighlight (global_axiom_widget [axiom_number -
				BUILT_IN_AXIOMS], 0);
			ring ();
			def_axiom_count--;
			def_axiom_index [axiom_number - BUILT_IN_AXIOMS] = 0;
			last_state [axiom_number] = 0;
			send_to_magic ("N\n");
			receive_all ();
		} else {
			strcpy (&def_axiom_formula [axiom_number - 
				BUILT_IN_AXIOMS][0], extra_string);
			sprintf (axiom [axiom_number], "%d: %s\0", 
				axiom_number + 1, &def_axiom_formula 
				[axiom_number - BUILT_IN_AXIOMS][0]);
			XawListChange (global_axiom_widget [axiom_number
			    - BUILT_IN_AXIOMS], &(axiom[axiom_number]), 1,
			    0, True);
			XawListHighlight (global_axiom_widget [axiom_number -
				BUILT_IN_AXIOMS], 0);

		}
	}
}

void update_axioms ()
{
	int	i;
	extern	Widget axiom_widget [NO_OF_AXIOMS];

	for (i = 0; i < BUILT_IN_AXIOMS; i++) {
		switch (last_state [i]) {
		case 1: XtListHighlight (axiom_widget [i], 0);
			break;
		case 0: XtListUnhighlight (axiom_widget [i], 0);
			break;
		}
	}
}

void reset_axioms ()
{
	int 		i;
	extern int	last_state [NO_OF_AXIOMS];
	extern int	def_axiom_index [DEF_AXIOMS];
	extern int	def_axiom_count;

	/*
	**	Switch off all the user-defined axioms
	**	visually and internally
	*/

	for (i = BUILT_IN_AXIOMS; i < NO_OF_AXIOMS; i++) {
		XtListUnhighlight (axiom_widget [i], 0);
		last_state [i] = 0;
		def_axiom_index [i - BUILT_IN_AXIOMS] = 0;
	}
	def_axiom_count = 0;
}