#! /usr/local/bin/perl5.7.2
# Polish Algorithm ("coiteration") of a term-pair or a list of term-pairs for various laws
# coiteration can be done plain or coded (coding is designed for left distributivity)
# terms are 0-1 strings in right polish notation, 0 = multiplication, 1 = variable of the terms
# written by Oliver Deiser, 2008, version = $version

use strict;
use warnings;
use utf8;
use FileHandle; STDOUT->autoflush();
use FileHandle; TABLE->autoflush();

my $prog = "comparison.pl";        # name of program
my $version = "1.0";
my $answer;                      # user input plain menu
my $cu = "u";                    # coded or uncoded comparison
my $file;                        # user file to read terms from
my $fi = "n";                    # output in file, 'y' or 'n';
my $sel;                         # user input (select);
my $width = 95;                  # used in program descrition and codesandlengthinfo
my $info = 0;                    # options on printing information during runtime
my $delay = 0;                   # output delay
my $poscoding = "n";             # possibility of coding
my $nextcode;                    # next free code number
my $f = 0;                       # a flag
my $bound = 0;                   # bound for comparison, 0 is unbounded
my $dep;                         # depth for systematic analysis
my $law = 0;                     # law for comarison, default is left distributivity (0)
my @varcodes;                    # user defined codes ('c' or 'C' option)
my @code;                        # @code has codes recursve in names, e.g. $code[20] = g60a70
my @result;                      # resulting terms and number of steps
my @examples;                    # list of examples
my @termlist;
my %names;                       # codes have alphanumerical names (or unicode, use perl 5.6.1 or later)
my %invnames;                    # inverse hash of %names
my %lecode;                      # length of codes
my %laws;                        # laws;
%laws = (0, "abc** = ab*ac**", 1, "abc** = ab*bc**", 2, "abc** = ab*ca**",
	 3, "abc** = ab*cb**", 4, "abc** = ab*cc**", 5, "abc** = ab*aac***");

$info = $ARGV[0] if (defined($ARGV[0]));       # comand line arguments for info and delay
$delay = $ARGV[1] if (defined($ARGV[1]));

R:                               # label for restart; no reset for $law, $bound, $delay, ...
@code = ();
$code[0] = 0;                    # 0 is multiplication
$code[1] = 1;                    # 1 is the variable (or constant) of the terms
$lecode{0} = $lecode{1} = 1;
$nextcode = 2;
$cu = "u";
$poscoding = "n";
$f = 0;
%names = names();
%invnames = reverse %names;

I: print "\nEnter:\n  't' to specify two terms,\n",                               ## main options
 "  'T' to read term-pairs from a file,\n",
 "  'e' for a list of examples (depending on the current law),\n",
 "  's' for a systematic analysis,\n",
 "  'l' to specify the law (default is left distributivity),\n",
 "  'o' to (re-)set output options,\n",
 "  'b' to enter an upper bound for the comparison,\n",
 "  'c' to enter codes,\n",
 "  'C' to read codes from a file,\n",
 "  'i' for information on this program and command line usage,\n",
 "  'm' for more about the problem and left distributivity,\n",
 "  'x' for exit.\n";
IN: print "\nYour choice: ";
chomp($answer = <STDIN>);

if ($answer eq "i") { info(); goto I if <STDIN> }                        ### answer i
elsif ($answer eq "t") {                                                 ### answer t
 ($termlist[0][0], $termlist[0][1]) = gettwoterms();
 }
elsif ($answer eq "T") {                                                 ### answer T
  $file = questfilename();
  @termlist = extractterms($file);
  $sel = questpair(@termlist);
  unless ($sel eq "a") {
    my @tl;
    ($tl[0][0], $tl[0][1]) = ($termlist[$sel][0], $termlist[$sel][1]);
    @termlist = @tl;
  }
}
elsif ($answer eq "e") {                                                  ### answer e
  @examples = examples();
  $sel = questexample();
  ($termlist[0][0], $termlist[0][1]) = ($examples[3*$sel], $examples[3*$sel + 1]);
  if ($law == 4) {
    if ($sel == 4) { showdivergence("110001100110"); }
    elsif ($sel == 5) { showdivergence("1100"); }
    elsif ($sel == 6) { showdivergence("110110001101100110110000"); }
  }
  elsif ($law == 5) {
    if ($sel == 3) { showdivergencelist("110", "a10", "bbab00", "ab0000", "bbaaad00000",
          "baaa000", "aaa000000", "bbaaaaa1a00000000000", "ab000", "bab00", "bbaad00", "bbajad000",
	  "bbab0aadaaad0000") }
  }
}
elsif ($answer eq "s") { $f = 1 }                                         ### answer s
elsif ($answer eq "l") {                                                  ### answer l
  $law = questlaw();
  goto I;
}
elsif ($answer eq "o") { ($info, $delay, $fi) = questoutput(); goto I; }
elsif ($answer eq "b") { $bound = questbnd(); goto I; }
elsif ($answer eq "c") { @varcodes = questvarcodes(); goto I; }
elsif ($answer eq "C") { $file = questfilecodes(); @varcodes = extractcodes($file) ; goto I; }
elsif ($answer eq "m") { about(); goto I; }
elsif ($answer eq "x") { print "\nGood bye!\n\n"; exit; }
else { goto IN; }

if ($law =~ m/[02]/ or ($law == 5 and $sel != 3)) { $poscoding = "y"; }
if ($f == 0) { runlist(@termlist); }
if ($f == 1) { rundepth(); }

E: print STDOUT "Continue ('y'/'n') ? ";
chop($answer = <STDIN>);
goto E unless ($answer eq "y" or $answer eq "n");
if ($answer eq "y") { goto R; }
else { print STDOUT "\nGood bye!\n\n"; exit; }

###############################################################################################################
# subs: runlist, rundepth
# coit, coitstep, coitmove, rewrite, reallength, codesandlength, sleeps, termtest, lefttermsearch,
# termenum, plain coit, plaincoitstep, plaincoitmove, info, quests, buildins0-4, reading

sub runlist {                                                                ### comparison in case t and e, i.e.
  my @termlist = @_;
  my $l = scalar(@termlist);
  my $i;
  $cu = questcoded() if ($poscoding eq "y");
  select TABLE if ($fi eq "y");

  for ($i = 0; $i < $l; $i++) {
    if ($info =~ m/[1,2]/) { print "\n", "-" x $width; }
    @result = coit($termlist[$i][0], $termlist[$i][1]) if ($cu eq "c");
    @result = plaincoit($termlist[$i][0], $termlist[$i][1], $fi) if ($cu eq "u");
    print "\n" if ($cu eq "u" and $info =~ m/[2]/);
    if ($i == 0) { print "\n", "-" x $width; }                   # print result and statistics
    print "\nWe compared the terms  $termlist[$i][0]  and  $termlist[$i][1] using the law $laws{$law}.\n";

    unless ($result[0] eq "c") {
      print "The Polish Algorithm terminated after $result[2] steps!\n";
      codesandlengthinfo () if ($cu eq "c");                 # print info on codes, length, real length of result
      if ($cu eq "u") {
	print "Result:\n  $result[0]\n  $result[1]\n";
	print "-" x $width, "\n";
      }
    }
    else {
      print "The Polish Algorithm didn't terminate after $bound steps.\n";
      print "-" x $width, "\n";
    }
  }
  print "\n";
}

sub rundepth {
  my ($k, $i, $k1, $k2, $l, $z, $c);
  my @anz;
  my @termenum;
  my $co = 0;
  my @complexterms;

  $dep = questdepth();
  $cu = questcoded() if ($poscoding eq "y");
  @termenum = termenum($dep);                       # generate termlist of depth $dep
  $l = scalar(@termenum);
  if ($fi eq "y") {
    print TABLE "List of terms to be compared:\n\n";
    for ($k = 0; $k < $l; ++$k) { print TABLE "$k:  $termenum[$k]\n"; }
    print TABLE "\n";
  }
  if ($l < 1000) { print STDOUT "\nI have $l runs to do. Please wait.\n\n"; }
  else { print STDOUT "\nI have $l runs to do. Maybe it's time for a coffee...\n\n"; }
  print STDOUT "0 ";
  for ($k1 = 1; $k1 < $l; ++$k1) {
   print STDOUT "$k1 ";
    for ($k2 = $k1 + 1; $k2 < $l; ++$k2) {
      if ($fi eq "y") {
	print TABLE "-" x $width;
	print TABLE "Terms: $k1, $k2\t",
	  "i.e. we compare:  $termenum[$k1],  $termenum[$k2]\n";
      }
      if ($fi eq "y") { select TABLE; }
      @result = coit($termenum[$k1], $termenum[$k2]) if ($cu eq "c");
      @result = plaincoit($termenum[$k1], $termenum[$k2], $fi) if ($cu eq "u");

      if ($result[0] eq "c") {
	$complexterms[$co][0] = $termenum[$k1];
	$complexterms[$co][1] = $termenum[$k2];
	$co++;
	if ($fi eq "y") { print TABLE "\tToo complex.\n\n"; }
      }
      else { 
	$i = $result[2];
	if ($fi eq "y") { print TABLE "\tAlgorithm terminated after $i step(s).\n\n"; }
	++$anz[$i];
      }
    }
 }
  select STDOUT;
  print "\n";
  if ($fi eq "y") {
    print "\nI created a list of all possible coiterations of ld-terms of depth $dep.\n";
    print "It's in the file table.txt\n\n";
    close(TABLE);
  }
  $c = 0;
  $l = scalar(@anz);
  print "\nHere is the graph of the function\n\nF(n) = number of term-pairs which terminate in exactely n steps.\n";
  print "\n(We omit pairs (t, t) and we count (t, s) and (s, t) as one pair for different terms t, s.)\n\n";
  for ($z = 0; $z < $l; ++$z) {
    if (defined($anz[$z])) {
      print "$z : $anz[$z];\n";
      $c += $anz[$z];
    }
  }
  print "Total number of term-pairs compared (depth $dep): $c\n\n";
  $z = scalar(@complexterms);
  if ($z > 0) {
    print "I skipped the following pairs, which need more than $bound steps:\n\n"; 
    for ($i = 0; $i < $z; $i++) {
      print "$complexterms[$i][0]  $complexterms[$i][1]\n";
    }
    print "\n";
  }

  N: print "Do you want to save this list (and the term-pairs skipped)? ('y'/'n') ";
  chop($answer = <STDIN>);
  goto N unless ($answer eq "y" or $answer eq "n");
  if ($answer eq "y") {
    open(TABLE, ">>table.txt");
    print TABLE "Step-function for depth $dep:\n";
    for ($z = 0; $z < $l; ++$z) { if (defined($anz[$z])) { print TABLE "$z : $anz[$z];\n"; } }
    print TABLE "Total number of term-pairs compared: $c\n\n";
    $z = scalar(@complexterms);
    if ($z > 0) {
      print TABLE "I skipped the following pairs, which need more than $bound steps:\n\n"; 
      for ($i = 0; $i < $z; $i++) {
	print TABLE "$complexterms[$i][0]  $complexterms[$i][1]\n";
      }
    }
    print "\no.k., I appended the list to the file table.txt\n\n";
  }
  close(TABLE);
}

sub coit {
  my $it1 = $_[0];            # left term
  my $it2 = $_[1];            # right term
  my $i;                      # number of steps
  my $l1;                     # length left term
  my $l2;                     # length right term
  my $l1real;                 # real length left term
  my $l2real;                 # real length right term
  my $z = 0;                  # position of first difference
  my $stepcor = 0;            # step correction = -1 when decoding
  my $side;                   # active side
  my $newcode = 0;            # = codenumber when a new coded was used in the last step
  my $it1m;                   # backup $it1
  my $it2m;                   # backup $it2
  $nextcode = 2;
  @code = (0, 1);
  $lecode{0} = $lecode{1} = 1;

  for ($i = 0; ; ++$i) {
    if ($bound > 0) { return "c" if ($i > $bound); }
    if ($stepcor == 0) {
      $it1m = $it1;
      $it2m = $it2;
      $z = 0;
      if ($info =~ m/[1,2,3,4,5]/) {
	$l1real =  reallength($it1);
	$l2real =  reallength($it2);
	sleeps($delay) if ($delay > 0);
	print "\n" unless ($info eq "-1");
	print "STEP $i:";
	print "\n" unless ($info eq "-1");
	if ($info =~ m/2/) { print "  $it1\n  $it2\n"; }
	if ($delay == -1 ) { my $input = <STDIN>; } 
     }
    }
    while (substr($it1, $z, 1) eq substr($it2, $z, 1) and substr($it1, $z, 1) ne "") { ++$z; }
    $l1 = length($it1);
    $l2 = length($it2);
    if ($z >= $l1 or $z >= $l2) {         # return if terms are comparable
      print "\n  done!\n" if ($info =~ m/[1,2]/);
      return ($it1, $it2, $i);
    }
    if ($info =~ m/1/ and $stepcor == 0) {
       print "  Length: $l1 $l2  First disagreement: $z   Real length: $l1real $l2real\n";
    }
    ($it1, $it2, $stepcor, $side, $newcode) = coitstep($it1, $it2, $z);
    $i -= $stepcor;
    if ($stepcor == 0) {      # rewriting terms after decoding and move
      if ($info =~ m/3/) {
	print "  Expanding yields:\n\n  $it1\n  $it2\n\n";
      }
      if ($side == 1) {
	$it2 = $it2m;
	if ($newcode > 0) { $it2 =~ s/$code[$newcode]/$names{$newcode}/g; $newcode = 0; }
	$it1 = rewrite($it1);
      }
      else {
	$it1 = $it1m;
	if ($newcode > 0) { $it1 =~ s/$code[$newcode]/$names{$newcode}/g; $newcode = 0; }
	$it2 = rewrite($it2);
      }
      if ($info =~ m/3/) {
	print "  Rewriting acording to our codes yields:\n";
      }
    }
  }
}

sub coitstep { 
  my $it1 = $_[0];                      # left term
  my $it2 = $_[1];                      # rigth term
  my $diff = $_[2];                     # first position of difference
  my $diff1 = substr($it1, $diff, 1);   # character at $diff left
  my $diff2 = substr($it2, $diff, 1);   # character at $diff right
  my $stepcor;                      # stepcorrection
  my $side;
  my $newcode;

  if ($diff1 eq "0") {
    $side = 2;
    $stepcor = 0;
   ($it2, $newcode) = coitmove($it2, $diff);        # move side with entry ne 0
    print "  Right side is active.\n" if ($info =~ m/5/);
  }
  elsif ($diff2 eq "0") {
    $side = 1;
    $stepcor = 0;
    ($it1, $newcode) = coitmove($it1, $diff);
    print "  Left side is active.\n" if ($info =~ m/5/);
  }
  else { $stepcor = 1;                                        # decode $diff's if both $diff's ne 0
	 my $num1 = $invnames{$diff1};
	 my $num2 = $invnames{$diff2};
	 if ($num1 > $num2) {
	   $it1 = substr($it1, 0, $diff) . $code[$num1] . substr($it1, $diff + 1); }
	 else {
	   $it2 = substr($it2, 0, $diff) . $code[$num2] . substr($it2, $diff + 1); }
	 if ($info =~ m/3/) {
	   print "\n  -- decoding $diff1, $diff2  at position $diff\t\t\n";
	   if ($info =~ m/4/) { print "\n  $it1\n  $it2\n"; }
	 }
       }
  return ($it1, $it2, $stepcor, $side, $newcode);
}

sub coitmove {        # expands terms acording to the Polish Algorithm
  my $t = $_[0];      # term
  my $p = $_[1];      # position
  my $pd;
  my $i;
  my $lop;            # length of active term
  my $x;              # character of a string
  my $d;              # balance of 0 and others in building subterms
  my $k;
  my $beg;            # result (expanded term) will be $beg . $ins . $res
  my $ins;
  my $res = "";
  my $newcode = 0;
  my @u;              # $u[0] is active term, $t = ... $u[0] $u[1] 0 $u[2] 0 $u[3] ... 0 $u[n] 0 0 ...
  my $n;
  my $c;
  my $z;

  ($u[1], $i) = lefttermsearch($t, $p);
  $beg = substr($t, 0, $p - $i);
  ($u[0], $i) = lefttermsearch($beg, $p - $i);
  $lop = length($u[0]);                         # length of active term
  if ($info =~ m/1/) {
    if ($info =~ m/[3,4]/) { print "\n  Decoding done. Active term is: $u[0]"; }
    else { print "  active term (after decoding): $u[0]"; } 
    if ($lop != 1) {
      my $newcode = $names{$nextcode};
      print "  =:  $names{$nextcode}  (new code)";
    }
    print "\n";
  }
  unless ($lop == 1) {                        # $lop == 1 iff active term is a code
    $newcode = $nextcode;
    $code[$nextcode] = $u[0];                 # new code for active term otherwise
    $u[0] = $names{$nextcode};
    $lecode{$u[0]} = reallength($code[$nextcode]); 
    ++$nextcode;

    if ($nextcode >= 62) {                    # unicode, use perl 5.6.1 or higher
      my $nc = 100 + $nextcode;               # new codenames, old one are below 161 in chr()
      $names{$nextcode} = chr($nc);
      $invnames{chr($nc)} = $nextcode;
    }
  }
  for ($n = 2; ; $n++) {                      # computing @u
    for ($z = 0; ; $z++) {
      if (substr($t, $p + $z, 1) eq "0") { --$d; }
      else { ++$d; }
      last if ($d == 0);
    }
    $u[$n] = substr($t, $p, $z);
    $p = $p + $z + 1;
    last if (substr($t, $p, 1) eq "0");
  }
  $res = substr($t, $p + 1) if ($p + 1 < length($t));

  if ($info =~ 6) {
    my $lu = scalar(@u);
    print "  u-vector (length $lu):  @u\n"; }

  if ($law == 0) { $ins = buildins0(@u); }
  elsif ($law == 1) { $ins = buildins1(@u); }
  elsif ($law == 2) { $ins = buildins2(@u); }
  elsif ($law == 3) { $ins = buildins3(@u); }
  elsif ($law == 4) { $ins = buildins4(@u); }
  elsif ($law == 5) { $ins = buildins5(@u); }
  else { die "Unknown law.\n"; }
  return ($beg . $ins . $res, $newcode);                  # expanded term
}

sub rewrite {                       # rewrite terms recursively acording to codes
my $w = $_[0];
my $n = scalar(@code);
my $z;
for ($z = 2; $z < $n; ++$z) { $w =~ s/$code[$z]/$names{$z}/g; }
return $w;
}

sub reallength {                    # real length of a coded term
my $t = $_[0];
my $l = length($t);
my $k;
my $s;
my $lreal = 0;
for ($k = 0; $k < $l; ++$k) {
    $s = substr($t, $k, 1);
    $lreal += $lecode{$s};
  }
return $lreal;
}

sub codesandlengthinfo {            # information on the codes used and on the real length of the result
my $z;
my $l1;
my $l2;
print "\nWe used the codes:\n";
for ($z = 2; $z < $nextcode; ++$z) {
  print " $names{$z}  :=  $code[$z] \t(code number $z)   Real length:  $lecode{$names{$z}}\n";
}
print "\nResulting terms:\n Left:   $result[0]\n Right:  $result[1]\n";
$l1 = reallength($result[0]);
$l2 = reallength($result[1]);
print "\nReal length of resulting terms:\n Left:   $l1\n Right:  $l2\n";
print "-" x $width;
}

sub sleeps {
my $z;
my $a = $_[0] * 100000;
for ($z = 0; $z <= $a; ++$z) { }
}


sub termtest {                  # termtest, returns 1 if $_[0] is a term, 0 otherwise
my $term = $_[0];
my $lh = length($term);
my $i;
my $d = 0;

for ($i = 0; $i < $lh; $i++) {
  if (substr($term, $i, 1) eq 0) { $d--; }
  elsif (substr($term, $i, 1) eq 1) { $d++; }
  else { $d = 0 }
  return 0 if ($d <= 0);
}
if ($d == 1) { return 1; }
else { return 0; }
}


sub lefttermsearch {
  my $t = $_[0];
  my $p = $_[1];
  my $i;
  my $d = 0;
  for ($i = 1; ; $i++) {
    if (substr($t, $p - $i, 1) eq "0") { $d--; }
    else { $d++; };
    last if ($d == 1);
  }
  return (substr($t, $p - $i, $i), $i);
}

sub termenum {
  my ($dep, $i, $term1, $term2, $termlist);
  my @terms;
  my @termenum;
  my %complex;

  $dep = $_[0];
  $termlist = "1";
  $complex{"1"} = 1;

  for($i = 2; $i <= $dep; ++$i) {
    @terms = split(" ", $termlist);
    foreach $term1 (@terms) {
       foreach $term2 (@terms) {
	 if ($complex{$term1} + $complex{$term2} == $i) {
	   unless (defined($complex{$term1 . $term2 ."0"})) {
	     $termlist .= " $term1" . $term2. "0";
	     $complex{$term1 . $term2 . "0"} = $i;
	   } 
	 }
       }
     }
  }
  @termenum = split(" ", $termlist);
  return (@termenum);
}

sub plaincoit {
  my $it1 = $_[0];            # left term
  my $it2 = $_[1];            # right term
  my $i;                      # number of steps
  my $z = 0;
  my $l1;
  my $l2;

  for ($i = 0; ; ++$i) {
    if ($bound > 0) { return "c" if ($i > $bound); }
    while (substr($it1, $z, 1) eq substr($it2, $z, 1) and substr($it1, $z, 1) ne "") { ++$z; }
    $l1 = length($it1);
    $l2 = length($it2);
    if ($info =~ m/[1,2,3,4,5]/) {
      sleeps($delay) if ($delay > 0);
      if ($delay == -1 ) { my $input = <STDIN>; }
      print "\n" unless ($info eq "1");
      print "STEP $i:  ";
      print "\n" unless ($info eq "1");

      if ($info =~ m/2/) {
	if (@varcodes) {
	  my $it1s = $it1;
	  my $it2s = $it2;
	  my $i;
	  for ($i = 0; $i < scalar(@varcodes); $i++) {
	    $it1s =~ s/$varcodes[$i][0]/$varcodes[$i][1]/g;
	    $it2s =~ s/$varcodes[$i][0]/$varcodes[$i][1]/g;
	  }
	  print "  $it1s\n  $it2s\n";
	}
	else { print "  $it1\n  $it2\n"; }
      }
      if ($info =~ m/1/) {
	my $fr;
	if ($l1 <= $l2) { $fr = $z / $l1; } else { $fr = $z / $l2; }
	print "  LTH:  $l1  $l2   AGMT: $z   FRAC: $fr\t";
      }
    }
    if ($z >= $l1 or $z >= $l2) {         # return if terms are comparable
      return ($it1, $it2, $i);
    }
    if ($_[2] eq "y") {
      print TABLE "Step $i:\n  $it1\n  $it2\n";
    }
    # unless ($bound == 0) {    #old option for bound of type 2
    #   return "c" if ($l1 > $bound or $l2 > $bound);
    # }
   ($it1, $it2) = plaincoitstep($it1, $it2, $z);
  }
}

sub plaincoitstep {
  my $it1 = $_[0];                      # left term
  my $it2 = $_[1];                      # rigth term
  my $diff = $_[2];                     # first position of difference
  my $diff1 = substr($it1, $diff, 1);   # character at $diff left
  my $diff2 = substr($it2, $diff, 1);   # character at $diff right

  if ($diff1 eq "0") {
    $it2 = plaincoitmove($it2, $diff, 2);         # move side with entry ne 0 
    print "  Right side is active.\n" if ($info =~ m/5/);
  }
  else {
    $it1 = plaincoitmove($it1, $diff, 1);
    print "  Left side is active.\n" if ($info =~ m/5/);
  }
  return ($it1, $it2);
}

sub plaincoitmove {
  my $t = $_[0];      # term
  my $p = $_[1];      # 1-position, 0 after the expansion 
  my $beg = "";
  my $ins = "";
  my $res = "";
  my $i;
  my $c;
  my $d = 0;
  my $z;
  my $n;
  my $s;
  my @u;
  my $lop;

  ($u[1], $i) = lefttermsearch($t, $p);
  $beg = substr($t, 0, $p - $i);
  ($u[0], $i) = lefttermsearch($beg, $p - $i);
  $lop = length($u[0]);

  if ($info =~ m/[1]/) {
    print "LTH OF ACTIVE TERM: $lop\n"; 
  }
  for ($n = 2; ; ++$n) {
    for ($z = 0; ; ++$z) {
      if (substr($t, $p + $z, 1) eq "1") { ++$d; }
      else { --$d; }
      last if ($d == 0);
    }
    $u[$n] = substr($t, $p, $z);
    $p += $z + 1;
    last if (substr($t, $p, 1) eq "0");
  }
  $res = substr($t, $p + 1) if ($p + 1 < length($t));

  if ($info =~ 6) {
    my $lu = scalar(@u);
    print "  u-vector (length $lu):  @u\n"; }

  if ($law == 0) { $ins = buildins0(@u); }
  elsif ($law == 1) { $ins = buildins1(@u); }
  elsif ($law == 2) { $ins = buildins2(@u); }
  elsif ($law == 3) { $ins = buildins3(@u); }
  elsif ($law == 4) { $ins = buildins4(@u); }
  elsif ($law == 5) { $ins = buildins5(@u); }
  else { die "Unknown law.\n"; }

  return ($beg . $ins . $res);
}

sub questdepth {
  my $dep;
 M: print "\nDepth of terms (number of 1's; should be between 2 and 9): ";   # depth
  chop($dep = <STDIN>);
  goto M unless ($dep >= 2);
  return $dep;
}

sub questcoded {
  my $cu;
 M: print "Coded or uncoded comparison ('c'/'u') or info ('i'): ";
  chop($cu = <STDIN>);
  if ($cu eq "i") {
    print "You can choose between coded and uncoded comparison.\n";
    print "The coding gives names to active terms.\n";
  }
  goto M unless ($cu eq "c" or $cu eq "u");
  return($cu);
}

sub questfile {
  my $fi;
 M: print "Shall I create a file displaying the comparsions ('y'/'n') or info ('i') ? ";
  chop($fi = <STDIN>);
  if ($fi eq "i") {
    print "Caution: File will have several MB if depth >= 7)\n";
    print "Try it first for small depth.\n\n";
  }
  goto M unless ($fi eq "y" or $fi eq "n");
  if ($fi eq "y") {
    print "o.k., the outout file will be table.txt in this directory.\n";
    open(TABLE, ">table.txt");
    my $head = "COITERATION (POLISH ALGORITHM) FOR TERMS OF DEPTH $dep\n";
    print TABLE "\t", $head;
    print TABLE "\t", "-" x (length($head) - 1), "\n\n\n";
    print TABLE "We display the comparison process for each nontrivial pair of terms in the list below.\n\n\n"; 
  }
  return ($fi);
}

sub questfilename {
  my $file;
 T:  print "Name of the file or 'i' for info: ";
  chop($file = <STDIN>);
  if ($file eq "i") {
    print "Enter a existing file name, e.g. myexamples.txt. I will read the lines of this file,\n",
      "and extract the first two terms of each line, if they exist.\n",
      "I can then run the algorithm on the whole list or on a single pair.\n\n";
    goto T;
  }
  open (FILE, "<$file") or die "Can't open/find file $file.\n";
  return($file);
}

sub questexample {
  my $i;
  for ($i = 0; $i < scalar(@examples)/3; $i++) {
    print "\nExample $i:\t\t\t$examples[3*$i + 2]\n";
    print "  Left term:  $examples[3*$i]\n  Right term: $examples[3*$i + 1]\n";
  }
  M: print "\nEnter the number of the example you want to run: ";
  chomp($i = <STDIN>);
  goto M if ($i =~ m/\D/ or $i*3 >= scalar(@examples));
  return $i;
}

sub names {                      # nice alphanumeric codes in the beginning, cont. autom. if ness. (unicode)
 my %names;
 my $i;
 for ($i = 0; $i < 10; $i++) { $names{$i} = chr(48 + $i); }              # 0..9
 for ($i = 0; $i < 26; $i++) { $names{$i + 10} = chr(97 + $i); }        # a..z
 for ($i = 0; $i < 26; $i++) { $names{$i + 36} = chr(65 + $i); }        # A..Z
 return %names;
}


sub examples {  
  my @examples;
  if ($law == 0) {
    print "Some examples of term pairs for left distributivity  $laws{$law}\n";
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "1110101100100", "1101011101000",         "a typical example of depth 7",
    "1110101110000", "1101010111000",         "the most complex example of depth 7",
    "111010101110000", "110101011110000",     "complex example of depth 8",
    "111010101110000", "110101010111000",     "the most complex example of depth 8",
    "11101010101100111010110001000", "11011001111010011001010101110001000",
 	     "just a typical example with longer terms...",
    "111010101110000", "11010101111010000",   "very complex depth 8/9 example, needs about 9 million steps!");
  }
  if ($law == 1) {
    print "Some examples of term pairs for central duplication  $laws{$law}\n";
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "111010101110000", "110101010111000",     "this was the complex 8-example for left distributivity",
    "1110101110000",  "1101110101000",           "most complex example of depth 7",
    "111010101110000",  "110111010101000",       "most complex example of depth 8",
    "11101010101100111010110001000", "11011001111010011001010101110001000", "typical example with longer terms");
  }
  if ($law == 2) { 
    print "Some examples of term pairs for the law $laws{$law}\n";   
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "111010101110000", "110101010111000",     "depth 8-example",
    "1111101010000", "1101011101000",         "the only, but very complex example of depth 7 ",
    "1111110100000", "110110011110000",       "complex depth 8 example", 
    "11101010101100111010110001000", "11011001111010011001010101110001000", "typical example with longer terms");
   }
 if ($law == 3) {
    print "Some examples of term pairs for the law $laws{$law}\n";
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "111010101110000", "110101010111000",     "this was the complex 8-example for left distributivity",
    "1111100010100", "1101110100100",         "most complex example of depth 7",
    "111110010011000", "110111010100100",     "complex example of depth 8",
    "111111000011000", "110111111000000",     "most complex example of depth 8",
    "11101010101100111010110001000", "11011001111010011001010101110001000", "typical example with longer terms");
  }
  if ($law == 4) {
    print "Some examples of term pairs for right duplikation  $laws{$law}\n";
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "111010101110000", "110101010111000",     "example which is complicated for left distributivity",
    "11111001000",  "1101011110000",  "counterexample for termination of the algorithm",
    "11111001000",  "1101011110000",  "same example, but demonstrating divergence",
    "11110100100",  "110101111010000", "another counterexample where you can see divergence",
    "1111110010000", "110101111100000", "and one more",
    "11101010101100111010110001000",  "11011001111010011001010101110001000", "typical example with longer terms");
  }
  if ($law == 5) {
    print "Some examples of term pairs for double left distributivity  $laws{$law}\n";
    @examples = (                  # format: "left term", "right term", "comment". Specify "" for no comment!
    "11100", "110111000",                     "very simple example",
    "110111000", "111011000",                 "example as in Dehornoy's book",
    "1110100", "11010111000",         "first counterexample for divergence",
    "1110100", "11010111000",         "same example, but demonstrating divergence",
    "11101011000", "11010111000",     "one more counterexample");
  }

  return(@examples);
}

sub gettwoterms {
  my @terms;
  my $i;
  print "Enter two terms. Start a term with 'D:' to get the result of the dilatation operation.\n";
  for ($i = 0; $i < 2; $i++) {
    if ($i == 0) { print "Left Term:  "; }
    else { print "Right term: "; }
    chomp($terms[$i] = <STDIN>);

   if (substr($terms[$i], 0, 2) eq "D:") {
      if (termtest(substr($terms[$i], 2)) == 0) { print "Termtest failed!\n"; $i--; next; }
      $terms[$i] = deltaop(substr($terms[$i], 2));
      print "this is: $terms[$i]\n";
    }
    if (termtest($terms[$i]) == 0) { print "Termtest failed!\n"; $i--; next; }
  }
  print "o.k.\n";
  return($terms[0], $terms[1]);
}

sub extractcodes {
  my $file = $_[0];
  my $i;
  my @sp;
  my @varcodes;
  open (FILE, "$file") or die "can't open $file\n";
  my @lines = <FILE>;
  for ($i = 0; $i < scalar(@lines); $i++) {
    @sp = split(" ", $lines[$i]);
    next if (scalar(@sp < 2));
    $varcodes[$i][0] = $sp[0];
    $varcodes[$i][1] = $sp[1];
  }
  $varcodes[$i][0] = "exit";
  print "\no.k. I will use the coding (syntax: string code):\n";
  for ($i = 0; $i + 1 < scalar(@varcodes); $i++) {
    print "$varcodes[$i][0]\t $varcodes[$i][1]\n";
  }
  print "\n";
  return @varcodes;
}

sub extractterms {
  my $file = $_[0];
  open (FILE, "$file") or die "can't open $file\n";
  my @lines = <FILE>;
  my @termlist;
  my $i;
  my $j;
  my $j2;
  my $a;
  my $b;
  my $n = 0;
  my $sel;
  my $te;
  Q: for ($i = 0; $i < scalar(@lines); $i++) {
    my @ar = split(" ", $lines[$i]);
    for ($j = 0; $j < scalar(@ar) - 1; $j++) {
      if (termtest($ar[$j]) == 1) {
	$te = $ar[$j];
	for ($j2 = $j + 1; $j2 < scalar(@ar); $j2++) {
	  if (termtest($ar[$j2]) == 1) {
	    ($termlist[$n][0], $termlist[$n][1]) = ($te, $ar[$j2]);
	    $n++;
	    next Q;
	  }
	}
      }
    }
  }
  return(@termlist);
}

sub questpair {
  my @termlist = @_;
  my $i;
  my $sel;
  if (scalar(@termlist) == 0) { print "No term-pairs found in $file"; exit; }
  else {
    print  "Term-pairs extracted from $file:\n\n";
    for ($i = 0; $i < scalar(@termlist); $i++) {
      print "$i:  $termlist[$i][0]  $termlist[$i][1]\n";
    }
    S: print "\nEnter number of pair you want to run or 'a' to run the whole list: ";
    chop($sel = <STDIN>); 
    unless ($sel eq "a" or (0 <= $sel and $sel < scalar(@termlist))) { goto S; }
  }
  return $sel;
}

sub questlaw {
 my $law;
 print "\nI can do the canonical comparison process for the following laws:\n\n";
 print "0:  $laws{0}\t\tleft distributivity or ac-law (default)\n",
   "1:  $laws{1}\t\tcentral duplication or bc-law\n",
   "2:  $laws{2}\t\touter duplication or ca-law\n",
   "3:  $laws{3}\t\tmiddle distributivity or cb-law\n",
   "4:  $laws{4}\t\tright duplication or cc-law\n",
   "5:  $laws{5}\t\tdouble left distributivity or a(ac)-law\n";
 M: print "\nSelect the law number [0-5]: ";
 chop($law = <STDIN>);
 goto M unless (length($law) == 1 and $law =~ m/[012345]/);
 print "\no.k. law is set to $laws{$law}.\n";
 return($law);
}

sub questoutput {
  my $info;
  my $delay;
  my $fi;
  print "\nInformation during runtime (any subset of 123456, written as a string): ";
  chop($info = <STDIN>);
  print "Delay (positive number or '-1'): ";
  chop($delay = <STDIN>);
 M: print "Print output to a file ('y'/'n')? ";
  chop($fi = <STDIN>);
  goto M unless ($fi eq "y" or $fi eq "n");
  if ($fi eq "y") {
    print "\no.k., the output file will be table.txt in this directory.\nDelay is set to 0.\n";
    open(TABLE, ">table.txt");
    $delay = 0;
  }
    return ($info, $delay, $fi);
}

sub questbnd {
  my $bound;
 M: print "Bound for comparison (enter integer, '0' for unbounded, 'i' for info): ";
  chop($bound = <STDIN>);
  if ($bound eq "i") {
    print "\nThe comparison will be stopped after your-bound many steps.\n";
    print "Small values can be useful to produce a list of complex termpairs of a certain depth.\n\n";
    goto M;
  }
  goto M unless ($bound >= 0);
  return($bound);

}

sub questvarcodes {
my $i;
my @varcodes;
print "\nEnter string and codes (i.e. a rewriting list)\nEnter 'exit' for string when finished.\n\n";
for ($i = 0; ; $i++) {
    print "String $i: ";
    chop($varcodes[$i][0] = <STDIN>);
    return (@varcodes) if ($varcodes[$i][0] eq "exit");
    print "Code $i:   ";
    chop($varcodes[$i][1] = <STDIN>); }
}

sub questfilecodes {
  my $file;
 T:  print "Name of the file or 'i' for info: ";
  chop($file = <STDIN>);
  if ($file eq "i") {
    print "\nEnter a existing file name, e.g. mycodes.txt. I will read the lines of this file,\n",
      "and extract the first two strings of each line.\n",
      "The syntax of a line should be: string code.\n",
      "E.g.: a line '111001 a' will produce an output where every string 111001 is replaced by a.\n",
      "The two lines '110 a' and 'a1a b' will produce an output where first every string 110\n",
      "is replaced by a, and then every string a1a in the result will be replaced by b.\n\n"; 
    goto T;
  }
  open (FILE, "<$file") or die "Can't open/find file $file.\n";
  return($file);
}

sub buildins0 {                 # abc** = ab*ac**
  my @u = @_;
  my ($ins, $n, $c);

  $ins = $u[1] . "0";
  $c = scalar(@u);
  for ($n = 2; $n < $c; ++$n) {
    $ins .= $u[0] . $u[$n] . "00";
 }
  return($ins);
}

sub buildins1 {                 # abc** = ab*cb**
  my @u = @_;
  my @i;
  my ($ins, $n, $c);

  $c = scalar(@u);
  $i[1] = $u[1];
  for ($n = 2; $n < $c - 1; $n++) {
    $i[$n] = $i[$n - 1] . $u[$n] . "0";
  }
  $ins = $u[1] . "0";
  for ($n = 2; $n < $c; $n++) {
    $ins .= $i[$n - 1] . $u[$n] . "00";
    }
  return($ins);
}

sub buildins2 {                 # abc** = ab*ca**
  my @u = @_;
  my ($ins, $n, $c);

  $ins = $u[1] . "0";
  $c = scalar(@u);
  for ($n = 2; $n < $c; ++$n) {
    $ins .= $u[$n] . $u[0] . "00";
 }
  return($ins);
}

sub buildins3 {                 # abc** = ab*cb**
  my @u = @_;
  my @i;
  my ($ins, $n, $c);

  $c = scalar(@u);
  $i[1] = $u[1];
  for ($n = 2; $n < $c - 1; $n++) {
    $i[$n] = $i[$n - 1] . $u[$n] . "0";
  }
  $ins = $u[1] . "0";
  for ($n = 2; $n < $c; $n++) {
    $ins .= $u[$n] . $i[$n - 1] . "00";
    }
  return($ins);
}

sub buildins4 {                 # abc** = ab*cc**
  my @u = @_;
  my ($ins, $n, $c);

  $ins = $u[1] . "0";
  $c = scalar(@u);
  for ($n = 2; $n < $c; ++$n) {
    $ins .= $u[$n] . $u[$n] . "00";
 }
  return($ins);
}

sub buildins5 {                 # abc** = ab*ac**
  my @u = @_;
  my ($ins, $n, $c);

  $ins = $u[1] . "0";
  $c = scalar(@u);
  for ($n = 2; $n < $c; ++$n) {
    $ins .= $u[0] . $u[0] . $u[$n] . "000";
 }
  return($ins);
}

sub showdivergence {
  my $s = $_[0];
  print "The divergence will be demonstrated by coding the string $s as a dot '.'\n";
  print "Press 'enter' to start.\n";
  if (<STDIN>) { 
    $varcodes[0][0] = $s;
    $varcodes[0][1] = ".";
    $varcodes[1][0] = "exit";
  }
  $info = 2;
  $delay = 20 if ($delay == 0);
}

sub showdivergencelist {
  my @li = @_;
  my ($i, $s);
  for ($i = 0; $i < scalar(@li); $i++) {
    $varcodes[$i][0] = $li[$i];
    $varcodes[$i][1] = chr(97 + $i);
  }
  $varcodes[$i][0] = "exit";
  print "The divergence will be demonstrated using the following codes:\n\n";

  for ($i = 0; $i < scalar(@li); $i++) {
    print "  $varcodes[$i][1] := $varcodes[$i][0]\n";
  }
  print "\nPress 'enter' to start.\n";
  if (<STDIN>) {
    $info = 2;
    $delay = 15 if ($delay == 0);
  }
}

sub about {
  print "\n";
  print "*" x $width, "\n";
  print "Left distributivity is the law a(bc) = (ab)(ac).\n",
        "In right Polish notation this reads: abc** = ab*ac**.\n",
        "The interest in this identity arose from set theory:\n",
        "The first solution of the word problem for (LD) used very strong large cardinal axioms.\n",
	"This solution is due to Patrick Dehornoy and Richard Laver, around 1989.\n",
        "Later Dehornoy found a second proof using braid groups.\n",
        "The Polish Algorithm is a canonical algorithm to compare two given terms:\n",
	"One corrects the least difference in each step by expanding the terms, until - if ever -\n",
	"one side is an initial segment of the other.\n",
	"Termination of the Polish Algorithm for (LD) is an open problem,\n",
	"and this program hopes to be useful towards a solution.\n",
	"For more on the subject see the following great book:\n",
	"Patrick Dehornoy: Braids and Self-Distributivity, Birkhaeuser, 2000.\n";
  print "*" x $width, "\n\n";
}

sub info {                  # description of program and usage/options
    print "\n\n";
    print "*" x $width, "\n";
    print "This is a perl-program running the canonical algorithm of iterating away the first difference\n";
    print "of finite terms satisfying various laws (like left distributivity).\n";
    print "Version $version. Written by Oliver Deiser. Last modified: September 2008. Use perl5.6.1 or higher.\n";
    print "*" x $width, "\n\n";
    print "Terms are in right Polish notation, written as 01-strings,\n";
    print "where 1 represents the variable and 0 represents multiplication.\n";
    print "Terms are can be coded during runtime to improve performance in some cases.\n";
    print "Currently supported laws are: abc** = ab*ac**,\n";
    print "abc** = ab*bc**, abc** = ab*ca**, abc** = ab*cb**, abc** = ab*cc**, abc** = ab*aac***.\n";
    print "\nUsage and options: perl $prog \[0123456] [number]\n";
    print "\n[0123456] specifies the information printed during runtime. [number] delays output.\n";
    print "0 means no output during runtime\n";
    print "1 displays length of terms and agreement at each step\n";
    print "2 displays terms at each step\n";
    print "3 displays decoding information and terms before rewriting\n";
    print "4 displays long decoding information (needs 3 to be active)\n";
    print "5 states which side is active\n";
    print "6 displays the vector of terms used to compute the one-step expansion\n";
    print "[number]: System counts to [number] * 100000 after each step if [number] > 0.\n";
    print "If [number] is -1, then the system waits after each step. Press <ENTER> to continue.\n";
    print "\nExamples of use:\n  perl $prog 0 0 or just\n",
      "  perl $prog     for best performance concerning termination.\n";
    print "  perl $prog 123456 -1  for detailed output waiting for <ENTER> after each step.\n";
    print "  perl $prog 12 20  for an output with medium information and delay.\n\n";
    print "Result will be displayed after termination with any options.\n";
    print "Outout options can also be specified during runtime.\n";
    print "There is also the option to redirect the output to a file in the 'o' submenu.\n";
    print "*" x $width, "\n";
}

sub t1t2 {
  my $t = $_[0];
  my $l = length($t);
  my ($t1, $t2, $i);

  if ($l == 1) { return($t, 0); }
  else {
    ($t2, $i) = lefttermsearch($t, $l - 1);
    }
  $t1 = substr($t, 0, $l - $i - 1);
  return($t1, $t2);
}

sub sternop {
  my $t0 = $_[0];
  my $t = $_[1];
  my ($t1, $t2);
  ($t1, $t2) = t1t2($t);
  if ($t2 eq "0") { return($t0 . $t . "0"); }
  else { return(sternop($t0, $t1) . sternop($t0, $t2) . "0"); }
}

sub deltaop {
  my $t = $_[0];
  my $l = length($t);
  return($t) if ($l == 1);
  my ($t1, $t2, $a, $b, $c);
  ($t1, $t2) = t1t2($t);
  $a = deltaop($t1);
  $b = deltaop($t2);
  $c = sternop($a, $b);
  return($c);
}