/*
 * $RCSfile$
 *
 * Deduktions-Programm in JavaScript
 *
 * $Revision$
 *
 * $Author$
 *
 * $Date$
 *
 * $Log$
 *
 */

/*
 * Klasse:     Urteil
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    subjekt
 *    praedikat
 *    copula
 *    ok
 *
 * Methoden:
 *    toString ()
 *    equals (ur)
 *    reverse ()
 */
function Urteil (str)
{
   var Ausdruck = /(\w+)\s+(\/?[<>\-~])\s+(\w+)/;

   if (Ausdruck.test (str))
   {
      Ausdruck.exec(str);
      this.subjekt = RegExp.$1;
      this.praedikat = RegExp.$3;
      this.copula = RegExp.$2;
      this.ok = true;
   }
   else this.ok = false;

   this.toString = function ()
   {
      return (this.subjekt + ' ' + this.copula + ' ' + this.praedikat);
   }

   this.equals = function (ur)
   {
      if ((this.subjekt==ur.subjekt)
         && (this.praedikat==ur.praedikat)
         && (this.copula==ur.copula))
         return true;

      return false;
   }

   this.reverse = function ()
   {
      var str = this.copula,
          vor = (str.length==2)?'/':'',
          tmp = str.charAt (str.length-1),
          ret = new Urteil ('');

      ret.subjekt = this.praedikat;
      ret.praedikat = this.subjekt;

      if (tmp=='<')        ret.copula = vor + '>';
      else if (tmp=='>')   ret.copula = vor + '<';
      else                 ret.copula = vor + tmp;

      ret.ok = this.ok;

      return ret;
   }
}

/*
 * Klasse:     Syllogismus
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    name
 *    copula1
 *    copula2
 *    folgerung
 *
 * Methoden:
 *    folgere
 */
function Syllogismus (nm, cop1, cop2, folg)
{
   this.name = nm;
   this.copula1 = cop1;
   this.copula2 = cop2;
   this.folgerung = folg;

   this.reverse = function (str)
   {
      var vor = (str.length==2)?'/':'',
          tmp = str.charAt (str.length-1);

      if (tmp=='<')        return vor + '>';
      else if (tmp=='>')   return vor + '<';
      else                 return vor + tmp;
   }

   this.copula1_ = this.reverse (this.copula1);
   this.copula2_ = this.reverse (this.copula2);
   //this.folgerung_ = this.reverse (this.folgerung);

   this.folgere = function (ur1, ur2)
   {
      var ret = new Urteil ('');

      // Wenn beide Urteile einen Mittelbegriff an passender Stelle haben
      if (ur1.praedikat==ur2.subjekt)
      {
         if ((ur1.copula==this.copula1)
            && (ur2.copula==this.copula2))
         {
            // Anwendung der positiven Version
            ret.subjekt = ur1.subjekt;
            ret.praedikat = ur2.praedikat;
            ret.copula = this.folgerung;
            ret.ok = true;
         }
         else if ((ur1.copula==this.copula1_)
            && (ur2.copula=='/'+this.folgerung))
         {
            // Anwendung der ersten Umkehrung
            ret.subjekt = ur1.subjekt;
            ret.praedikat = ur2.praedikat;
            ret.copula = '/' + this.copula2;
            ret.ok = true;
         }
         else if ((ur1.copula=='/'+this.folgerung)
            && (ur2.copula==this.copula2_))
         {
            // Anwendung der zweiten Umkehrung
            ret.subjekt = ur1.subjekt;
            ret.praedikat = ur2.praedikat;
            ret.copula = '/' + this.copula1;
         }
      }

      return ret;
   }
}

/*
 */
function Dedu (grele, praem)
{
   this.addPraem = function (ur)
   {
      if (!ur.ok) return false;

      //if (!this.reflexOk && (ur.subjekt==ur.praedikat)) return false;

      var i, ur_ = ur.reverse ();
      for (i=0; i<this.praem.length; i++)
      {
         if (ur.equals (this.praem[i])) return false;
         //if (ur_.equals (this.praem[i])) return false;
      }

      this.praem[this.praem.length] = ur;
      this.praem[this.praem.length] = ur_;

      return true;
   }

   this.syllogismen = new Array ();

   // die Regeln
   this.syllogismen[this.syllogismen.length]
      = new Syllogismus ( 'Regel 1.1', '-', '~', '<');
   this.syllogismen[this.syllogismen.length]
      = new Syllogismus ( 'Regel 1.2a', '<', '-', '-');
   this.syllogismen[this.syllogismen.length]
      = new Syllogismus ( 'Regel 1.2b', '>', '~', '~');
   this.syllogismen[this.syllogismen.length]
      = new Syllogismus ( 'Regel 1.3', '<', '<', '<');

   this.folgere = function ()
   {
      var dt = new Date ();

      this.proto += 'beginne Folgerungen...\n';

      var anzahl, ersterNeuer, tmp = -1, laeufe=0;
      do {
         // derzeitige Anzahl aller Praemissen
         anzahl = this.praem.length;
         ersterNeuer = tmp;

         this.proto += (1+laeufe) + '. Durchlauf (Anzahl=' + anzahl
                       + ', 1. Neuer=' + ersterNeuer + ')\n';

         var i, j, k, folg;
         for (i=0; i<anzahl-1; i++)
         {
            for (j=Math.max(ersterNeuer, i+1+(i%2)); j<anzahl; j++)
            {
               //this.proto += 'alle Syllogismen mit ' + i + ' und ' + j + '\n';

               for (k=0; k<this.syllogismen.length; k++)
               {
                  /*
                  this.proto += '  versuche ' + this.syllogismen[k].name
                                + ' mit ' + this.praem[i]
                                + ' und ' + this.praem[j]
                                + '\n';
                  */

                  folg = this.syllogismen[k].folgere (this.praem[i], this.praem[j]);
                  if (this.addPraem (folg))
                  {
                     if (anzahl+2==this.praem.length) tmp = anzahl;
                     this.konkl += folg + '\n';
                     this.proto += folg + ', weil (' + this.praem[i] + ') und ('
                                   + this.praem[j] + ') nach '
                                   + this.syllogismen[k].name + '\n';
                  }

                  folg = this.syllogismen[k].folgere (this.praem[j], this.praem[i]);
                  if (this.addPraem (folg))
                  {
                     if (anzahl+2==this.praem.length) tmp = anzahl;
                     this.konkl += folg + '\n';
                     this.proto += folg + ', weil (' + this.praem[j] + ') und ('
                                   + this.praem[i] + ') nach '
                                   + this.syllogismen[k].name + '\n';
                  }
               }
            }
         }

         laeufe++;
         //this.proto += 'Ende des ' + laeufe + '. Durchlaufs\n';

      } while (anzahl<this.praem.length);

      this.sek = ((new Date ()).getTime () - dt.getTime ()) / 1000;
      this.proto += 'Fertig. (' + laeufe + ' Durchlaeufe)\n';
   }

   this.setPraem = function (str)
   {
      this.praem = new Array ();
      this.konkl = '';
      this.proto = '';
      this.sek = 0;

      this.proto += 'lese Praemissen...\n';

      var arr = str.replace (/\r/g, '\n').replace (/\n+/g, '\n').split ('\n');

      var i;
      for (i=0; i<arr.length; i++)
      {
         if (arr[i].length==0) continue;

         this.proto += 'Praemisse "' + arr[i] + '": ';

         var ur = new Urteil (arr[i]);

         if (ur.ok)
         {
            this.addPraem (ur);
            this.proto += 'ok.\n';
         }
         else this.proto += 'Fehler!\n';
      }
   }

   this.ausgabe = function ()
   {
      var i;
      this.konkl = '';
      for (i=0; i<this.praem.length; i++)
         this.konkl += this.praem[i].toString () + '\n';
   }

   if (arguments.length>0)
   {
      this.setPraem (praem);
      this.folgere ();
      this.ausgabe ();
   }
}