#! /usr/bin/perl -w

our @tokens;
our @premises;
our @theorems;
my $depth=0;

@steps = <>;
check_theorem_list(@steps);

sub check_theorem_list {
    my ($step, $statment);
    @theorems = ( [] ); 
MAIN:
    while ($step = shift) {
	$step =~ s/\s//g;
	next unless $step;
	if ($step eq "[") {
	    pretty_print("[\tpush\n");
	    $depth++;
	    $step = shift;
	    $step =~ s/\s//g;
	    $statement = parse($step);
	    pretty_print("$step\tpremise\n");
	    push @premises, $statement;
	    push @theorems, [ $statement ];	   
	    next;
	}
	if ($step eq "]") {
	    die "Already at the level of reality" unless $depth > 0; 
	    $depth--;
	    pretty_print("]\tpop\n");
	    $premise = pop @premises;
	    $step = shift;
	    $step =~ s/\s//g;
	    $statement = parse($step);
	    $conclusion = ${pop @theorems}[-1];
	    if (implication($premise,$conclusion,$statement)) {
		push @{$theorems[-1]}, $statement;
		pretty_print("$step\tfantasy rule\n");
		next;
	    }
	    die "Error: $step is not ${premise}?$conclusion!";
	}
	$statement = parse($step);
	# Check for all kinds of deductions
	my $rule = "";
	if ($depth > 0) {
	    for (@{$theorems[-2]}) {  # Accidentally allows the stripping of double-negatives
		if (rec_eq($_, $statement)) {
		    $rule = "carry-over";
		    last;
		}
	    }
	}
	$rule = check_for_deductions($statement, @{$theorems[-1]}) unless $rule;
	if ($rule) {
	    pretty_print("$step\t$rule\n");
	    # push onto the list of theorems
	    push @{$theorems[-1]}, $statement;
	    next;
	}
	# Give up 
	die "Can't find a rule to derive $step";
    }
}

sub pretty_print {
    my $string = shift;
    my $tab = "  " x $depth;
    print "$tab$string";
}

sub implication {
    my ($premise, $conclusion, $imp) = @_;
    return "" unless $imp->{type} eq '?';
    return rec_eq($imp->{left}, $premise) && rec_eq($imp->{right}, $conclusion)
}



sub joining {
    my ($compound, $left, $right) = @_;
    return "" unless $compound->{type} eq '&';
    return rec_eq($compound->{left}, $left) || rec_eq($compound->{right}, $right);
}
sub separation {
    my ($compound, $part) = @_;
    return "" unless $compound->{type} eq '&';
    return rec_eq($compound->{left}, $part) || rec_eq($compound->{right}, $part);
}


sub contrapositive {
    my ($positive, $contra) = @_;
    return "" unless $positive->{type} eq '?' && $contra->{type} eq '?';
    my ($left, $right) = @{$contra}{'left', 'right'};
    return "" unless $left->{type} eq '~' && $right->{type} eq '~';
    return rec_eq($left->{formula}, $positive->{right}) &&
	rec_eq($right->{formula}, $positive->{left});
}

sub deMorgan {
    my ($and, $nor) = @_;
    return "" unless $and->{type} eq "&"
	&& $and->{left}{type} eq '~' && $and->{right}{type} eq '~'
	&& $nor->{type} eq '~';
    my $or = $nor->{formula};
    return  $or->{type} eq '|' 
	&& rec_eq($and->{left}{formula}, $or->{left})
	&& rec_eq($and->{right}{formula}, $or->{right});
}

sub switcheroo {
    my ($or, $implies) = @_;
    return "" unless $or->{type} eq '|' && $implies->{type} eq '?' 
	&& $implies->{left}{type} eq '~';
    return  
	rec_eq($implies->{left}{formula},$or->{left}) &&
	rec_eq($implies->{right}, $or->{right});
}

sub check_recursively {
    my ($test, $one, $two) = @_;
    return 1 if $test->($one, $two) || $test->($two, $one);
    return "" unless $one->{type} eq $two->{type};
    for ($one->{type}) {
	if (/^atom/) {
	    return $one->{name} eq $two->{name};
	}
	if (/^~/) {
	    return check_recursively($test, $one->{formula}, $two->{formula})
	}
	else {
	    # only one interchange allowed per step
	    return check_recursively($test, $one->{left}, $two->{left}) && 
		rec_eq($one->{right}, $two->{right}) || 
		rec_eq($one->{left}, $two->{left}) && 
		check_recursively($test, $one->{right}, $two->{right});
	}
	    
    }
}

sub strip_double_negatives {
    my $statement = shift;
    for ($statement->{type}) {
	if (/^atom/) {
	    return $statement;
	}
	elsif (/^~/) {
	    if ($statement->{formula}{type} eq '~') {
		return strip_double_negatives($statement->{formula}{formula});
	    }
	    else {
		return {type => '~', formula => strip_double_negatives($statement->{formula}) };
	    }
	}
	else {
	    return {type => $statement->{type},
		    left => strip_double_negatives($statement->{left}),
		    right => strip_double_negatives($statement->{right})
		    }
	}
		
    }	
}

sub check_for_deductions {
    my $statement = shift;
    for my $old (@_) {
	return "repetition" if rec_eq($old, $statement);
	return "separation" if separation($old, $statement);
	return "contrapositive" if check_recursively(\&contrapositive, $old, $statement);
	return "switcheroo" if check_recursively(\&switcheroo, $old, $statement);
	return "de Morgan's rule" if check_recursively(\&deMorgan,$statement, $old);
	return "double-tilde" if rec_eq(strip_double_negatives($old), 
					strip_double_negatives($statement));
    }
    for $left (@_) {
	for $right (@_) {
	    return "detachment" if implication($left, $statement, $right);
	    return "joining" if joining($statement, $left, $right);
	}
    }
}

sub parse_atom {
    my ($first, $atom, $next);
    $first = shift @tokens;
    if ($first =~ /P|Q|R/) {
	 $atom = $first;
    }
    else { unshift @tokens, $first; return "" }
    for ($next = shift @tokens; $next && $next eq "\'"; $next = shift @tokens) {
	$atom .= $next;
    }
    unshift @tokens, $next if $next;
    return $atom;
}

sub parse_formula {
    if ($tokens[0] eq '~') {
	shift @tokens;
	my $negation = parse_formula();
	return { type => '~', formula => $negation }
    }
    if ($tokens[0] eq '<') {
	shift @tokens;
	my $left = parse_formula( );
	my $connector = shift @tokens;
	my $right = parse_formula( );
	return "" unless (my $t = shift @tokens) eq '>';
	return { type => $connector, left => $left, right => $right};
    }
    my $atom = parse_atom( );
    return { type => "atom", name => $atom } if $atom;
    return "";
}

sub rec_eq {
    my ($a, $b) = @_;
    my ($ta, $tb) = ($a->{type}, $b->{type});
    return '' unless $ta eq $tb;
    for ($ta) {
	if (/^atom/) {
	    return $a->{name} eq $b->{name};
	}
	elsif (/^~/) {
	    return rec_eq($a->{formula}, $b->{formula});
	}
	else {
	    return rec_eq($a->{left}, $b->{left}) && rec_eq($a->{right}, $b->{right});
	}
    }
}
sub parse {
    my $string = shift;
    $string =~ s/\s//g;
    @tokens = split "", $string;
    return parse_formula();
}

sub mp {
    my ($ant, $imp) = @_;
    return "" unless ref $imp && rec_eq($ant, $imp->{left}) && $imp->{connector} eq "?";
    return $imp->{right};
}

sub unparse {
    my $formula = shift;
    return $formula unless ref $formula;
    return unparse($formula->{left}) . $formula->{connector} . unparse($formula->{right});
}

1;