/*
 * $RCSfile: venn.js,v $
 *
 * einfaches Venn-Programm in JavaScript
 *
 * $Revision: 1.16 $
 *
 * $Author: Det $
 *
 * $Date: 2005/07/30 12:28:49 $
 *
 * $Log: venn.js,v $
 * Revision 1.16  2005/07/30 12:28:49  Det
 * Bugfix in FeldListe.oder: Die letzten Zellen der zweiten
 * Liste wurden ignoriert.
 *
 * Revision 1.15  2003/05/19 09:58:55  dm
 * Bugfix in Zeile 226 (Fkt. VennStack): Die Klammern bei
 * einem 'new Array()' fehlten. (Nur zufaellig entdeckt; es
 * hat offenbar keinen Browser gestoert.)
 *
 * Revision 1.14  2003/05/14 14:00:44  dm
 * Anpassung an den eigenartigen Umgang von Opera mit RegExp.$n
 *
 * Revision 1.13  2003/05/14 12:24:59  dm
 * Syntaxfehler erscheinen jetzt im Protokoll statt als Alerts
 *
 * Revision 1.12  2003/03/25 09:48:27  dm
 * Bugfix beim Anwenden der Individual-Regel: Diese
 * Regel muss ggf. mehrfach angewendet werden (siehe
 * Beispiel 6 in venn.html).
 *
 * Revision 1.11  2003/03/23 12:38:31  dm
 * Bugfix beim Eintrag von Individual-Praemissen;
 * Bugfix beim Testen von partikulaeren und Individual-
 * Konklusionen;
 * Bug beim Anwenden der Individual-Regel erkannt
 *
 * Revision 1.10  2003/03/20 12:20:08  dm
 * Optimierung bei "Individualbegriffe als Konklusionen"
 *
 * Revision 1.9  2003/03/20 11:16:30  dm
 * Kommentare werden ab jetzt mit // eingeleitet.
 *
 * Revision 1.8  2003/03/20 00:35:17  dm
 * Individualbegriffe als Konklusionen (experimentell)
 *
 * Revision 1.7  2003/03/19 16:15:24  dm
 * Individualbegriffe als Praemissen
 *
 * Revision 1.6  2003/03/18 12:41:21  dm
 * Bugfix VennListe.nicht; dazu VennStack.n eingefuehrt;
 * Kommentare bei Grundelementen und auf eigenen Zeilen erlaubt;
 * Optimierung beim Check von partikulaeren Konklusionen
 *
 * Revision 1.5  2003/03/18 10:46:41  dm
 * Parser.parse wurde fuer jedes Urteil mehrfach aufgerufen;
 * hinter Praemissen und Konklusionen sind jetzt durch
 * ein $ abgetrennte Kommentare erlaubt;
 * Sekundenzähler eingebaut
 *
 * Revision 1.4  2003/03/18 09:53:03  dm
 * Bugfix in FeldListe.oder; dazu Array.append hinzugefuegt
 *
 * Revision 1.3  2003/03/18 00:48:25  dm
 * Kommentare zu den Klassen ergaenzt
 *
 * Revision 1.2  2003/03/18 00:23:05  dm
 * einfacher Konklusionentest fertig.
 *
 * Revision 1.1  2003/03/17 10:20:26  dm
 * Initial revision
 *
 */

/* Erweiterung der Klasse Array
 *
 * Methoden:
 *    indexOf
 *    append
 */
Array.prototype.indexOf = function (obj) 
{
   var i;
   var start = (arguments.length==2)?arguments[1]:0;

   /*
   if (obj.equals)
      for (i=start; i<this.length; i++)
         if (obj.equals (this[i]))  return i;

   else if (obj.compare)
      for (i=start; i<this.length; i++)
         if (obj.compare (this[i]) == 0)  return i;

   else
   */
      for (i=start; i<this.length; i++)
         if (obj == this[i])  return i;

   return -1;
}
Array.prototype.append = function (obj)
{
   if (this[this.length-1] != obj)
      this[this.length] = obj;
}

/* Klasse:     FeldListe
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    liste
 *
 * Methoden:
 *    und
 *    oder
 *    nicht
 *    toString
 */
function FeldListe (str, n)
{
   this.und = function (vArr)
   {
      var i, j, treffer = -1;
      var ret = new FeldListe ();

      for (i=0; i<this.liste.length; i++)
      {
         j = vArr.liste.indexOf (this.liste[i], treffer+1);
         if (j > -1)
         {
            ret.liste[ret.liste.length] = this.liste[i];
            treffer = j;
         }
      }

      return ret;
   }

   this.oder = function (vArr)
   {
      var i, j, aktuell = -1;
      var ret = new FeldListe ();

      for (i=0; i<this.liste.length; i++)
      {
         for (j=aktuell+1; vArr.liste[j] < this.liste[i]; j++)
            ret.liste.append (vArr.liste[j]);

         aktuell=j-1;

         ret.liste.append (this.liste[i]);
      }

      for (j=aktuell+1; j<vArr.liste.length; j++)
         ret.liste.append (vArr.liste[j]);

      return ret;
   }

   this.nicht = function (n)
   {
      var i, j, letzter = -1;
      var ende = Math.pow (2, n);
      var ret = new FeldListe ();

      for (i=0; i< this.liste.length; i++)
      {
         for (j=letzter+1; j<this.liste[i]; j++)
            ret.liste[ret.liste.length] = j;
         letzter = j;
      }

      for (j=letzter+1; j<ende; j++)
         ret.liste[ret.liste.length] = j;

      return ret;
   }

   this.toString = function ()
   {
      return this.liste.join ('|');
   }


   this.liste = new Array ();

   if (arguments.length > 0)
   {
      if (str == 'W')
      {
      }
      else if (str == 'M')
      {
         var i, lng = Math.pow (2, n);

         for (i=0; i<lng; i++)
            this.liste[this.liste.length] = i;
      }
      else
      {
         var i, j, lng = Math.pow (2, n);
         var beg = parseInt (str);
         var per = Math.pow (2, beg);

         for (i=0; i<lng; )
         {
            for (j=0; j<per; j++)
            {
               i++
            }
            for (j=0; j<per; j++)
            {
               this.liste[this.liste.length] = i;
               i++
            }
         }
      }
   }
}

/* Klasse:     VennStack
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    stack
 *
 * Methoden:
 *    push
 *    pop
 *    und
 *    oder
 *    nicht
 */
function VennStack (n)
{
   this.stack = new Array ();
   this.n = n;

   this.push = function (obj)
   {
      this.stack[this.stack.length] = obj;
   }

   this.pop = function ()
   {
      ret = this.stack[this.stack.length-1];
      this.stack = this.stack.slice (0, this.stack.length-1);
      return ret;
   }

   this.und = function ()
   {
      var a = this.pop (),
          b = this.pop ();
      this.push (b.und (a));
   }

   this.oder = function ()
   {
      var a = this.pop (),
          b = this.pop ();
      this.push (b.oder (a));
   }

   this.nicht = function ()
   {
      var a = this.pop ();
      this.push (a.nicht (this.n));
   }
}

/* Klasse:     SyntaxError
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    name
 *    message
 *
 * Methoden:
 *    toString
 */
function SyntaxError (txt)
{
   this.name = 'SyntaxError';
   this.message = 'Fehler: ' + txt;

   this.toString = function ()
   {
      return this.message;
   }
}

/* Klasse:     VennParser
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    zeile
 *    token
 *    upn
 *    grele
 *
 * Methoden:
 *    addGrele
 *    setGrele
 *    expected
 *    getToken
 *    match
 *    bfactor
 *    notfactor
 *    bterm
 *    bexp
 *    blurteil
 *    parse
 *    compile
 */
function VennParser ()
{
   this.zeile = '';	// Die aktuelle Zeile.
   this.token = '';	// Das nächste zu verarbeitende Token.
   this.upn = '';    // Ausgabe in UPN
   this.grele = new Array ();

   this.addGrele = function (str)
   {
      str = str.replace (/\s*/g,'');
      //str = str.replace (/^\s*/,'').replace (/\s*$/,'');

      if (this.grele.indexOf (str) == -1)
         this.grele[this.grele.length] = str;
   }

   this.setGrele = function (str)
   {
      this.grele = new Array ();

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

      var i;
      for (i=0; i<arr.length; i++)
      {
         arr[i] = arr[i].replace (/\s*\/\/.*$/, '');

         if (arr[i].length == 0) continue;

         this.addGrele (arr[i]);
      }
   }

   /*
    * bl-urteil  ::= b-exp < b-exp | b-exp * b-exp | b-exp ^I
    * b-exp      ::= b-term [ OR b-term ]*
    * b-term     ::= not-factor [ AND not-factor ]*
    * not-factor ::= [ NOT ]* b-factor
    * b-factor   ::= b-lit | ( b-exp )
    */

   this.expected = function (txt)
   {
      var fehler = new SyntaxError (txt + ' erwartet, "'
                                    + this.token + '" gefunden!');
      throw fehler;
   }

   this.getToken = function ()
   {
      if (this.zeile == '')
      {
         this.token = '';
         return false;
      }
      else
      {
         var ausdruck = /\s*(\w+|[<\*\-&#\(\)]|\^\s*I)\s*(.*)/;

         ausdruck.exec (this.zeile);

         //Diese Variante funktioniert nicht in Opera:
         //
         //this.token = RegExp.$1.replace (/\s+/g, '');
         //this.zeile = RegExp.$2;
         //
         //Daher also etwas umstaendlicher:

         var str1 = RegExp.$1,
             str2 = RegExp.$2;

         this.token = str1.replace (/\s+/g, '');

         this.zeile = str2;
      }

      //alert ('"' + this.token + '", "' + this.zeile + '"');
      return true;
   }

   this.match = function (c)
   {
      if (this.token != c) this.expected ('"' + c + '"');
      this.getToken ();
   }

   this.bfactor = function ()
   {
      var n = this.grele.indexOf (this.token);

      if (this.token == '0')
      {
         this.match ('0');
         this.upn += ' W';
      }
      else if (this.token == '1')
      {
         this.match ('1');
         this.upn += ' M';
      }
      else if (-1 != n)
      {
         this.match (this.token);
         this.upn += ' ' + n;
      }
      else if (this.token == '(')
      {
         this.match ('(');
         this.bexp ();
         this.match (')');
      }
      else
      {
         this.expected ('bfactor');
      }
   }

   this.notfactor = function ()
   {
      var n = 0;
      while (this.token == '-')
      {
         this.match ('-');
         n++;
      }

      this.bfactor ();

      if (n%2 == 1) this.upn += ' -';
   }

   this.bterm = function ()
   {
      this.notfactor ();

      while (this.token == '&')
      {
         this.match ('&');
         this.notfactor ();
         this.upn += ' &';
      }
   }

   this.bexp = function ()
   {
      this.bterm ();

      while (this.token == '#')
      {
         this.match ('#');
         this.bterm ();
         this.upn += ' #';
      }
   }

   this.blurteil = function ()
   {
      this.bexp ();

      if (this.token == '<')
      {
         this.match ('<');
         this.bexp ();
         this.upn += ' - & <';
      }
      else if (this.token == '*')
      {
         this.match ('*');
         this.bexp ();
         this.upn += ' & *';
      }
      else if (this.token == '^I')
      {
         this.match ('^I');
         this.upn += ' I';
      }
      else
      {
         this.expected ('Copula');
      }

      if (this.token != '')
      {
         var fehler = new SyntaxError ('Zeichen nach Urteil: "' + this.token + '"');
         throw fehler;
      }
   }

   this.parse = function (txt)
   {
      this.zeile = txt;
      this.getToken ();
      this.upn = '';

      try
      {
         this.blurteil ();
      }
      catch (e)
      {
         if (e.name == 'SyntaxError')  return e.message; // + '\n(' + this.upn + ')';
         else return ('unbekannter Fehler!\n' + e);
      }

      // einige Optimierungen :-)
      this.upn = this.upn.replace (/ - -/g, '');
      this.upn = this.upn.replace (/ M -/g, ' W');
      this.upn = this.upn.replace (/ W -/g, ' M');
      this.upn = this.upn.replace (/ M &/g, '');
      this.upn = this.upn.replace (/ W #/g, '');

      this.upn = this.upn.substr (1);

      return this.upn;
   }

   this.compile = function (str)
   {
      var beg, st = new VennStack (this.grele.length);
      var ret;
      this.zeile = str;

      while (this.getToken ())
      {
         if (this.token == '&')
         {
            st.und ();
            //alert ('und: ' + st.stack[st.stack.length-1].liste.join ('|'));
         }
         else if (this.token == '#')
         {
            st.oder ();
            //alert ('oder: ' + st.stack[st.stack.length-1].liste.join ('|'));
         }
         else if (this.token == '-')
         {
            st.nicht ();
            //alert ('nicht: ' + st.stack[st.stack.length-1].liste.join ('|'));
         }
         else if (this.token == 'M')
         {
            beg = new FeldListe (this.token, this.grele.length);
            st.push (beg);
            //alert (st.stack[st.stack.length-1].liste.join ('|'));
         }
         else if (this.token == 'W')
         {
            beg = new FeldListe (this.token, this.grele.length);
            st.push (beg);
            //alert (st.stack[st.stack.length-1].liste.join ('|'));
         }
         else if (this.token == '<')
         {
            ret = st.pop ();
            ret.copula = this.token;
         }
         else if (this.token == '*')
         {
            ret = st.pop ();
            ret.copula = this.token;
         }
         else if (this.token == 'I')
         {
            ret = st.pop ();
            ret.copula = this.token;
         }
         else
         {
            beg = new FeldListe (this.token, this.grele.length);
            st.push (beg);
            //alert ('beg: ' + st.stack[st.stack.length-1].liste.join ('|'));
         }
      }

      return ret;
   }
}

/* Klasse:     Venn
 * Vorfahre:   (-)
 *
 * Eigenschaften:
 *    diagramm
 *    parser
 *    praem
 *    indiv
 *    anzPart
 *    konkl
 *    proto
 *
 * Methoden:
 *    setGrele
 *    setPraem
 *    setKonkl
 *    check
 */
function Venn ()
{
   this.diagramm = new Array ();
   this.parser = new VennParser ();

   this.setGrele = function (grele)
   {
      this.parser.setGrele (grele);
      this.proto += this.parser.grele.length + ' Grundelemente\n';
      this.diagramm = new Array (Math.pow (2, this.parser.grele.length));

      var i;
      for (i=0; i<this.diagramm.length;i++)
         this.diagramm[i] = 0;
   }

   this.setPraem = function (praem)
   {
      this.praem = new Array ();
      this.indiv = new Array ();
      this.anzPart = 0;
      this.praem.ok = true;

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

      var i, tmp;
      for (i=0; i<arr.length; i++)
      {
         arr[i] = arr[i].replace (/\s*\/\/.*$/, '');

         if (arr[i].length == 0) continue;

         tmp = this.parser.parse (arr[i]);

         if (tmp.indexOf ('Fehler') != -1)
         {
            this.praem.ok = false;
            this.proto += 'Fehler in Prämisse "' + arr[i] + '":\n' + tmp + '\n';
            //alert (tmp);
         }
         else
            this.praem[this.praem.length] = tmp;
      }

      this.proto += this.praem.length + ' Praemissen\n';
   }

   this.setKonkl = function (konkl)
   {
      this.konkl = new Array ();
      this.konkl.ok = true;

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

      var i, tmp;
      for (i=0; i<arr.length; i++)
      {
         arr[i] = arr[i].replace (/\s*\/\/.*$/, '');

         if (arr[i].length == 0) continue;

         tmp = this.parser.parse (arr[i]);

         if (tmp.indexOf ('Fehler') != -1)
         {
            this.konkl.ok = false;
            this.proto += 'Fehler in Konklusion "' + arr[i] + '":\n' + tmp + '\n';
            //alert (tmp);
         }
         else
            this.konkl[this.konkl.length] = tmp;
      }

      this.proto += this.konkl.length + ' Konklusion'
                    + (this.konkl.length==1?'':'en')
                    + '\n';
   }

   this.check = function ()
   {
      this.proto = '';
      this.sek = new Date ();

      if (arguments.length == 3)
      {
         this.setGrele (arguments[0]);
         this.setPraem (arguments[1]);
         this.setKonkl (arguments[2]);
      }
      else if (arguments.length == 2)
      {
         this.setPraem (arguments[0]);
         this.setKonkl (arguments[1]);
      }
      else if (arguments.length == 1)
      {
         this.setKonkl (arguments[0]);
      }

      if (this.praem.ok)
      {
         var i, j, bit, urteil;

         // Praemissen im Diagramm eintragen
         for (i=0; i<this.praem.length; i++)
         {
            urteil = this.parser.compile (this.praem[i]);
            /*
            this.proto += i + ': ' + this.praem[i] +'\n'
                          + urteil.liste.join ('|')
                          + urteil.copula + '\n';
            */

            if (urteil.copula == '<')
            {
               bit = 1;
            }
            else if (urteil.copula == '*')
            {
               this.anzPart++;
               bit = Math.pow (2, this.anzPart);
            }
            else if (urteil.copula == 'I')
            {
               this.anzPart++;
               bit = Math.pow (2, this.anzPart);
               urteil.sternBit = bit;
               this.indiv[this.indiv.length] = urteil;
            }
            else
            {
               alert ('Urteil ohne Copula!?!');
            }

            for (j=0; j<urteil.liste.length; j++)
               this.diagramm[urteil.liste[j]] |= bit;
         }

         if (this.indiv.length > 0)
         {
            this.proto += this.indiv.length + ' Individualbegriff'
                        + (this.indiv.length==1?'\n':'e\n');

            // Individualbegriffs-Regel anwenden:

            // Diese Schleife muß gegebenfalls mehrfach durchlaufen werden:
            // Wenn eine Streichung eines Feldes bei einem Durchlauf einen
            // Stern löscht, dann kann möglicherweise beim nächsten Durchlauf
            // erneut diese Regel angewendet werden!

            var changed;
            do
            {
               changed = false;

               // für alle Individualbegriffe
               for (i=0; i<this.indiv.length; i++)
               {
                  // suche alle Sterne, die sich innerhalb des Indiviuums befinden

                  var part = 0;

                  for (j=0; j<this.indiv[i].liste.length; j++)
                     if (this.diagramm[this.indiv[i].liste[j]]
                         != (this.diagramm[this.indiv[i].liste[j]] | 1))
                        part = part | this.diagramm[this.indiv[i].liste[j]];

                  // entferne alle Sterne, die auch außerhalb des I.s vorkommen

                  urteil = this.indiv[i].nicht (this.parser.grele.length);

                  for (j=0; j<urteil.liste.length; j++)
                     if (this.diagramm[urteil.liste[j]]
                         != (this.diagramm[urteil.liste[j]] | 1))
                        part = part & (-1 ^ this.diagramm[urteil.liste[j]]);

                  // für alle verbliebenen Sterne:
                  for (bit=2; bit<=part; bit*=2)
                  {
                     if (part != (part | bit)) continue;

                     // streiche alle Felder innerhalb des I.s,
                     // die diesen Stern nicht enthalten
                     for (j=0; j<this.indiv[i].liste.length; j++)
                        if (this.diagramm[this.indiv[i].liste[j]]
                            != (this.diagramm[this.indiv[i].liste[j]] | bit))
                           if (this.diagramm[this.indiv[i].liste[j]]
                               != (this.diagramm[this.indiv[i].liste[j]] | 1))
                           {
                              this.diagramm[this.indiv[i].liste[j]] |= 1;
                              changed = true;
                           }
                  }
               }
            } while (changed);
         }

         this.proto += '\n';

         if (this.konkl.ok)

         {
            var folgt;

            //this.proto += this.diagramm.join ('|') + '\n';

            // Konklusionen prüfen
            for (i=0; i<this.konkl.length; i++)
            {
               urteil = this.parser.compile (this.konkl[i]);
               /*
               this.proto += 'Konkl.' + (i+1) + ': ' + this.konkl[i] + '\n'
                             + urteil.liste.join ('|')
                             + urteil.copula + '\n';
               */

               if (urteil.copula == '<')
               {
                  folgt = true;

                  for (j=0; j<urteil.liste.length && folgt; j++)
                     if (this.diagramm[urteil.liste[j]]
                         != (this.diagramm[urteil.liste[j]] | 1))
                        folgt = false;
               }
               else if (urteil.copula == '*')
               {
                  var part = 0;

                  // Welche "Sterne" kommen in einem Feld der
                  // Konklusion vor?
                  for (j=0; j<urteil.liste.length; j++)
                     if (this.diagramm[urteil.liste[j]]
                         != (this.diagramm[urteil.liste[j]] | 1))
                     {
                        part = part | this.diagramm[urteil.liste[j]];
                     }

                  // Welche der enthaltenen "Sterne" kommen außerhalb
                  // der Konklusion nicht vor?

                  urteil = urteil.nicht (this.parser.grele.length);

                  for (j=0; j<urteil.liste.length && part>0; j++)
                     if (this.diagramm[urteil.liste[j]]
                         != (this.diagramm[urteil.liste[j]] | 1))
                     {
                        part = part & (-1 ^ this.diagramm[urteil.liste[j]]);
                     }

                  folgt = (part > 0);
               }
               else if (urteil.copula == 'I')
               {
                  var part = 0, exists = false;
                  folgt = false;

                  // Welche Sterne rühren von einem Individualbegriff her?
                  // (Das könnte man sich natürlich auch schon beim Ein-
                  // tragen der Prämissen merken.)
                  for (j=0; j<this.indiv.length; j++)
                     part = part | this.indiv[j].sternBit;

                  // Welche dieser Sterne kommen in allen Feldern
                  // der Konklusion vor?
                  for (j=0; j<urteil.liste.length && part>0; j++)
                     if (this.diagramm[urteil.liste[j]]
                         != (this.diagramm[urteil.liste[j]] | 1))
                     {
                        part = part & this.diagramm[urteil.liste[j]];
                        exists = true;
                     }

                  // Falls ein ungestrichenes Feld gefunden wurde
                  // und wir noch restliche Sterne haben:
                  if (exists && part>0)
                  {
                     // Welche der restlichen Sterne kommen außerhalb
                     // der Konklusion nicht vor?

                     urteil = urteil.nicht (this.parser.grele.length);

                     for (j=0; j<urteil.liste.length && part>0; j++)
                        if (this.diagramm[urteil.liste[j]]
                            != (this.diagramm[urteil.liste[j]] | 1))
                        {
                           part = part & (-1 ^ this.diagramm[urteil.liste[j]]);
                        }
                  }

                  folgt = exists && (part > 0);
               }
               else
               {
                  folgt = false;
                  alert ('Urteil ohne Copula!?!');
               }

               this.proto += 'Konklusion ' + (i+1) + ': folgt'
                             + (folgt?'':' nicht')
                             + '\n';
            }
         }

         this.sek = (new Date ().getTime () - this.sek.getTime ()) / 1000;
      }
   }
}