// A JavaScript Program to implement a Gentzen system for Kleene algebras
// version of 9 March 2005, by Peter Jipsen, http://www.chapman.edu/~jipsen

// currently loops on (x*);(x*) <= x*

// The code has two main parts to it:
// 1. Handling formulas (actually only the part about equations and inequations is used)
//      parsing the ascii input and writing html output.
// 2. Implementing the Gentzen system.

// Part 1. Handling formulas
//check if the symbol font is available
symb = navigator.appVersion.lastIndexOf('Win')!=-1 ||
    navigator.appVersion.lastIndexOf('Mac')!=-1;

function out(col,str,alt,sp) {
  return sp+"<font"+(col==""?"" : " color="+col)+
    (alt==""?">"+str : (symb?" >"+str : ">"+alt))+"</font>"+sp;
}

bl="&nbsp;";

avar = {name:"a", arity:0, output:"<i>a</i>"};
bvar = {name:"b", arity:0, output:"<i>b</i>"};
cvar = {name:"c", arity:0, output:"<i>c</i>"};
dvar = {name:"d", arity:0, output:"<i>d</i>"};
xvar = {name:"x", arity:0, output:"<i>x</i>"};
yvar = {name:"y", arity:0, output:"<i>y</i>"};
zvar = {name:"z", arity:0, output:"<i>z</i>"};

vari = [ xvar, yvar, zvar ];

zero = {name:"0", arity:0, output:"0"};
unit = {name:"1", arity:0, output:"1"};
//topp = {name:"1", arity:0, output:"1"};

cons = [ zero, unit ];

meet = {name:"^", arity:2, priority:6, output:out("Blue","&and;","^",bl),
   infix:true, paren:true};
join = {name:"v", arity:2, priority:6, output:out("Blue","&or;","v",bl),
   infix:true, paren:true};
times = {name:";", arity:2, priority:8,
   output:out("Blue",";",";",""), infix:true, paren:true};
over = {name:"/", arity:2, priority:8,
   output:'<font color="Blue">/</font>', infix:true, paren:true};
under = {name:"\\", arity:2, priority:8,
   output:'<font color="Blue">\\</font>', infix:true, paren:true};
star = {name:"*", arity:1, priority:9,
   output:out("Blue","*","*",""), infix:true, paren:false};

oper = [ meet, join, times, over, under, star ];

eq   = {name:"=",  arity:2, output:'<font color="Red"> = </font>', infix:true, priority:4};
//less = {name:"<",  arity:2, output:'<font color="Red"> &lt; </font>', infix:true};
leq  = {name:"<=", arity:2, output:out("Red","&le;","&lt;=",bl),
  infix:true,  priority:4};
geq  = {name:">=", arity:2, output:out("Red","&ge;","&gt;=",bl),
  infix:true,  priority:4};

pred = [ eq, leq, geq ];

for (var i=0; i<vari.length; i++) vari[i].vari=true;
for (var i=0; i<cons.length; i++) cons[i].cons=true;
for (var i=0; i<oper.length; i++) oper[i].oper=true;
for (var i=0; i<pred.length; i++) pred[i].pred=true;

notSymbol = {name:"~",  arity:1,
  output:'<font color="Blue">~</font>'};
impSymbol = {name:"->", arity:2, priority:1,
  output:'&nbsp;<font color="Blue">==></font>&nbsp;',
  infix:true,paren:true};
andSymbol = {name:"and", arity:2, priority:3,
  output:'&nbsp;<font color="Blue"> and </font>&nbsp;',
  infix:true,paren:true};
orSymbol = {name:"or", arity:2, priority:2,
  output:'&nbsp;<font color="Blue"> or </font>&nbsp;',
  infix:true,paren:true};
iffSymbol = {name:"iff", arity:2, priority:0,
  output:'&nbsp;&nbsp;<font color="Blue"> iff </font>&nbsp;&nbsp;',
  infix:true,paren:true};
allSymbol = {name:"A",  arity:2, 
  output:'<font face="Symbol" color="Blue">"</font>'};
exSymbol = {name:"E",  arity:2, 
  output:'<font face="Symbol" color=Blue>$</font>'};

conn = [notSymbol, andSymbol, orSymbol, impSymbol, iffSymbol, allSymbol, exSymbol];

comma = {name:",", punc:true};
leftBracket = {name:"(", punc:true};
rightBracket = {name:")", punc:true};
leftSqBracket = {name:"[", punc:true};
rightSqBracket = {name:"]", punc:true};

punc = [comma, leftSqBracket, rightSqBracket, leftBracket, rightBracket ];


function add(arr, elt){    // the push method is not supported in IExpl*der
  arr[arr.length]=elt;
}

function Expr(symbol, arg, priority){ // third argument only used during parsing
  this.symbol = symbol;
  this.arg = arg;
  this.priority = priority;
}

function randomInt(n) {
  return Math.floor(n*Math.random());
}

function randomElt(a) {
  return a[Math.floor(a.length*Math.random())];
}

function randomVari(){
  return new Expr(randomElt(vari), [])
}

function randomList(len,max){
//random list of values in [0..max-1] with one of them = max-1
  var l=[];
  for (var i=0; i<len; i++)
    add(l,randomInt(max));
  l[randomInt(len)]=max-1;
  return l;
}

function randomTerm(depth){
  if (depth > 0) {
    var op=randomElt(oper);
    var dep=randomList(op.arity,depth);
    var arg=[];
    for (var i=0; i<op.arity; i++)
      add(arg,randomTerm(dep[i]));
    return new Expr(op, arg);
  }
  if (Math.random()<0.5) 
    return new Expr(randomElt(vari), []);
  return new Expr(randomElt(cons), []);
}

function randomFormula(fDepth,tDepth){
  if (fDepth > 0) {
    var co=randomElt(conn);
    if (co==allSymbol || co==exSymbol){ 
      var arg = [randomVari(), randomFormula(fDepth-1,tDepth)];
      return new Expr(co, arg);
    }
    var dep=randomList(co.arity,fDepth);
    var arg=[];
    for (var i=0; i<co.arity; i++)
      add(arg,randomFormula(dep[i],tDepth));
    return new Expr(co, arg);
  }
  var pr=randomElt(pred);
  var dep=randomList(pr.arity,tDepth);
  var arg=[];
  for (var i=0; i<pr.arity; i++)
    add(arg,randomTerm(dep[i]));
  return new Expr(pr, arg);
}

function e2s(q) {//convert expression to string
  if (q.arg.length==0) return q.symbol.output;
  if (q.symbol==allSymbol || q.symbol==exSymbol)
    return q.symbol.output + e2s(q.arg[0]) + "&nbsp;" + e2s(q.arg[1]);
  else if (q.symbol.infix)
    if (q.symbol.paren) return "(" + e2s(q.arg[0]) + 
      q.symbol.output + (q.arg.length==2?e2s(q.arg[1]):"") + ")";
    else return e2s(q.arg[0]) + q.symbol.output + (q.arg.length==2?e2s(q.arg[1]):"");
  var st = "";
  for (var i = 0; i < q.arg.length-1; i = i+1)
    st = st + e2s(q.arg[i]) + ",";
  st = st + e2s(q.arg[q.arg.length-1]);
  if (q.symbol.paren) return q.symbol.output + "(" + st + ")";
  else return q.symbol.output + st;
}

//Parsing ascii strings into expressions

//First we concatenate all the symbol arrays

function compareNames(s1,s2) {
  if (s1.name > s2.name) return 1
  else return -1;
}

symbols = vari.concat(cons, oper, pred, conn, punc);
symbols.sort(compareNames);
names = [];
for (var i=0; i<symbols.length; i++) names[i] = symbols[i].name;

maxPriority=0;
for (var i=0; i<symbols.length; i++)
  if (symbols[i].priority && symbols[i].priority>maxPriority)
    maxPriority = symbols[i].priority;
maxPriority++;

//names should contain no blanks

function removeCharsAndBlanks(str,n) {
  var st = str.slice(n);
  for (var i=0; i<st.length && st.charAt(i)==" "; i=i+1);
  return st.slice(i);
}

function position(arr, str, n) { // assumes arr is sorted
  for (var i=n; i<arr.length && arr[i]<str; i++);
  return i; // i=arr.length || arr[i]>=str
}

function getSymbol(str) {
  var k=0;
  var j=0;
  var st="";
  var oldst="";
  var more = true;
  for (var i=1; i<=str.length && more; i++) {
    oldst=st;
    st=str.slice(0,i);
    j=k;
    k=position(names, st, j);
    more = (k<names.length && st==names[k].slice(0,i))
  }
  if (k==names.length) return null;
  if (!more) st=oldst;
  else j=k;
  if (st==names[j]) return symbols[j]; //maximal substring that appears in names
  else return null;
}

aSymbols = symbols.concat([{name:"  ", output:" &nbsp; "}]);
aSymbols.sort(compareNames);
aNames = [];
for (var i=0; i<aSymbols.length; i++) aNames[i] = aSymbols[i].name;

function a2h(str) {
  var j,k;
  var st,oldst,hstr;
  var more;
  while (str!="") {
    k=0;
    st="";
    more=true;
    for (var i=1; i<=str.length && more; i++) {
      oldst=st;
      st=str.slice(0,i);
      j=k;
      k=position(aNames, st, j);
      more = (k<aNames.length && st==aNames[k].slice(0,i));
    }
    if (!more) st=oldst;
    else j=k;
    if (st==aNames[j]) {
      hstr = hstr.concat(aSymbols[j].output);
      str = str.slice(st.length);
    } else {
      hstr = hstr.concat(st.charAt(0));
      str = str.slice(1);
    }
  }
  return hstr;
}

/*
blanks ( ) [ ] , are seperators (not allowed in names of symbols)
Arguments may be separated by spaces or single commas.
Parenthesis must be balanced.

Symbols are either terminal (arity==0) or prefix or infix (unary infix defaults to postfix)

expr ::= terminal | prefix expr1 ... exprN | prefix(expr1, ... , exprN) | 

         expr infix | expr1 infix exprN | (expr) | [expr]

Expressions are read from left to right, choosing the longest initial substring
that matches the name of a symbol. Symbol priority is taken into account.
*/

function str2expr(str,pri) { //builds expr and returns [expr,substring]
// If returned substring starts with "Error: ..." it contains information about a parsing error
  var arg=[];
  var token="";
  var symbol;
  var nextsymbol;
  var expr;
  var estr;
  var more;
  str=removeCharsAndBlanks(str,0);
  symbol=getSymbol(str); //either a symbol or a bracket or empty
//document.writeln("@@",str,"#",symbol,"<br>");
  if (symbol==null||symbol==rightBracket) 
    return [null,"Error, '(' or symbol expected: "+str];
  str=removeCharsAndBlanks(str,symbol.name.length); 

  if (symbol==leftBracket) {                        //read (expr)
    estr=str2expr(str,0);expr=estr[0];str=estr[1];
    if (str.slice(0,5)=="Error") return [null,str];
    expr.priority = maxPriority;
    symbol=getSymbol(str);
    if (symbol==null) return [null,"Error, unknown symbol: "+str];
    str=removeCharsAndBlanks(str,symbol.name.length); 
    if (symbol!=rightBracket) return [null,"Error, ')' expected : "+str];

  } else if (symbol.arity==0 || symbol.infix) {//read terminal
    expr=new Expr(symbol,[], maxPriority);

  } else {                  //read prefix expr1 ... exprN or prefix(...)
    nextsymbol = getSymbol(str);
    var commas=false;
    if (nextsymbol==leftBracket && symbol.paren) {
      str = removeCharsAndBlanks(str,nextsymbol.name.length);
      nextsymbol = getSymbol(str);
      commas=true;
    }
    more = nextsymbol!=null && 
      (commas || !nextsymbol.infix && !nextsymbol.endSymb) && //nextsymbol!=norm) && 
      nextsymbol!=rightBracket && nextsymbol!=comma;
    while (str!="" && more && (symbol.endName==null||
        symbol.endName!=str.slice(0,symbol.endName.length))) {
      nextsymbol = getSymbol(str);
//document.write(symbol.name,nextsymbol.name,"@",str,"<br>");
      if (nextsymbol==null) return [null,"Error, incorrect symbol: "+str];
      if (commas)
        estr=str2expr(str,-1);
      else estr=str2expr(str,symbol.priority);
      expr=estr[0];str=estr[1];
      if (str.slice(0,5)=="Error") return [null,str];
      add(arg,expr);
      nextsymbol = getSymbol(str);
      more = nextsymbol != null && 
        (commas || !nextsymbol.infix && nextsymbol!=norm) &&
        nextsymbol!=rightBracket;
      if (commas)
        if (str=="") return [null,"Error, ')' expected: "+str];
        else if (str.charAt(0)==",") str=removeCharsAndBlanks(str,1);
        else if (str.charAt(0)==")") {
          more = false;
          str=removeCharsAndBlanks(str,1);
        }
    }
    expr=new Expr(symbol, arg, maxPriority);
    if (symbol.endName!=null) {
//document.write(symbol.name,"#",str,"<br>");
      if (symbol.endName!=str.slice(0,symbol.endName.length))
        return [null,"Error, "+symbol.endName+" expected: "+str];
      str=removeCharsAndBlanks(str,symbol.endName.length);
    }
  }
//parse right argument of infix operation
  symbol = getSymbol(str);// infix op symb
  var insert=null;
  if (symbol==null || !symbol.infix || symbol.priority<pri || 
    symbol==comma && pri==-1) 
    return [expr,str];//complete subterm
  str = removeCharsAndBlanks(str,symbol.name.length);
  more=true;
  while (more) {
    more=false;
    nextsymbol = getSymbol(str);
    if (str=="" || str.charAt(0)==")" || nextsymbol!=null && 
      nextsymbol.infix) { //unary infix symbol
      expr=new Expr(symbol, [expr], maxPriority); 
      more=nextsymbol!=null && nextsymbol.infix;
      if (!more) return [expr,str];
      symbol = nextsymbol;
      str = removeCharsAndBlanks(str,symbol.name.length);
    }
  }
  var right=null;
  estr = str2expr(str,pri);right=estr[0];str=estr[1];
  if (str.slice(0,5)=="Error") return [null,str];
  if (right.priority>symbol.priority || 
      (right.priority==symbol.priority && right.symbol.rightparen)) {
    expr=new Expr(symbol, [expr,right], symbol.priority); 
  } else {
    insert=right;
    while (insert.arg[0].priority && insert.arg[0].priority<symbol.priority) 
      insert=insert.arg[0];
    if (insert.arg[0].priority>symbol.priority || 
      insert.arg[0].symbol.rightparen) {
      expr=new Expr(symbol, [expr,insert.arg[0]], symbol.priority);
      insert.arg[0]=expr;
    } else {
      expr=new Expr(symbol, [expr,insert.arg[0].arg[0]], symbol.priority);
      insert.arg[0].arg[0]=expr;
    }
    expr=right;
  }
  return [expr,str];
}

function parse(str) {
  var temp = str2expr(str,0);
  if (temp[1].slice(0,5)=="Error") document.write("<P>"+temp[1]+"<P>");
  else if (temp[1].slice(0,5)!="") document.write("<P>Parse Leftover: "+temp[1]+"<P>");

//still have to check arities of expressions

  return temp[0];
}

function outputList(li) {
  for (var i=0; i<li.length; i=i+1)
    document.write(" &nbsp;"+li[i].output);
}

function symbolString(li) {
  var st="";
  for (var i=0; i<li.length; i=i+1)
    st=st+" &nbsp;"+li[i].output;
  return st;
}

//*******************************************************
// Part 2. Implementing the Gentzen system decision procedure.

function Seq(left, right){
  this.left = left;    // array of terms
  this.right = right;  // term
}

function seq2str(s) {
  var st="";
  for (var i=0; i<s.left.length; i=i+1){
    st=st+e2s(s.left[i]);
    if (i<s.left.length-1) st=st+", ";
  }
  st=st+leq.output+e2s(s.right);
  return st;
}

function concat(ar1,ar2){
  return ar1.concat(ar2);
}

function modify(ar1,m,elt){ // return ar1, but with ar1[m]==elt; ensure m<ar1.length
  var ar = ar1.slice(0,ar1.length);
  ar[m]=elt;
  return ar;
}

function equalTerms(s,t) {
//parent.output.document.write("$");
  if (s.symbol!=t.symbol) return false;
  if (s.arg.length!=t.arg.length) return false;
  for (var i=0; i<s.arg.length; i=i+1)
    if (!equalTerms(s.arg[i],t.arg[i])) return false;
  return true;
}

function space(n){
  var st="";
  for (var i=0; i<n; i++) 
    st=st+"|&nbsp;&nbsp;&nbsp;&nbsp;";
  return st;
}

proof=[];
proofattempt=[];

function isProvable(reason,n,s) {//indent n, sequent s
  add(proof,space(n)+seq2str(s)+"&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"+reason+"<br>");
  add(proofattempt,proof[proof.length-1]);
  var l=proof.length;
//parent.output.document.writeln(">"+space(n)+seq2str(s)+"&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"+reason+"<br>\n");
  if (s.left.length==1 && equalTerms(s.left[0],s.right)) return true; //Id
  if (s.left.length==0 && s.right.symbol==unit) return true; // 1-right
//  if (s.right.symbol==topp) return true; // T-right

  if (s.right.symbol==under) // \-right
    if (isProvable(under.output+"-<i>r</i>", 
      n, new Seq(concat([s.right.arg[0]],s.left),s.right.arg[1]))) return true;
    else {proof = proof.slice(0,l);}// return false;}

  if (s.right.symbol==over) // /-right
    if (isProvable(over.output+"-<i>r</i>", 
      n, new Seq(concat(s.left,[s.right.arg[1]]),s.right.arg[0]))) return true;
    else {proof = proof.slice(0,l);}// return false;}

  if (s.right.symbol==meet) // meet-right
    if (isProvable(meet.output+"-<i>r</i>1", n+1, new Seq(s.left,s.right.arg[0]))
        && isProvable(meet.output+"-<i>r</i>2", n+1, new Seq(s.left,s.right.arg[1])))
      return true;
    else {proof = proof.slice(0,l);}// return false;}

  for (var i=0; i<s.left.length; i=i+1) {
    if (s.left[i].symbol==unit) // 1-left
      if (isProvable(unit.output+"-<i>l</i>", 
        n, new Seq(concat(s.left.slice(0,i),s.left.slice(i+1)),s.right))) return true;
      else {proof = proof.slice(0,l);}// return false;}

    if (s.left[i].symbol==zero) // 0-left
      return true;

    if (s.left[i].symbol==times) // *-left
      if (isProvable(times.output+"-<i>l</i>", 
        n, new Seq(s.left.slice(0,i).concat(s.left[i].arg,s.left.slice(i+1)), s.right)))
        return true;
      else {proof = proof.slice(0,l);}// return false;}

    if (s.left[i].symbol==meet) // meet-left
      if (isProvable(meet.output+"-<i>l</i>1", 
        n, new Seq(modify(s.left,i,s.left[i].arg[0]),s.right))) return true;
      else {
        proof = proof.slice(0,l);
        if (isProvable(meet.output+"-<i>l</i>2", 
          n, new Seq(modify(s.left,i,s.left[i].arg[1]),s.right))) return true;
        else proof = proof.slice(0,l); // try other rules before returning false
      }

    if (s.left[i].symbol==join) // join-left
      if (isProvable(join.output+"-<i>l</i>1", 
        n+1, new Seq(modify(s.left,i,s.left[i].arg[0]),s.right))
          && isProvable(join.output+"-<i>l</i>2", 
        n+1, new Seq(modify(s.left,i,s.left[i].arg[1]),s.right))) return true;
      else {proof = proof.slice(0,l);} // return false;}

    if (s.left[i].symbol==under) {// \-left
      for (var j=0; j<=i; j=j+1) // sigma=s.left[j..i-1], gamma=s.left[0..j-1]
        if (isProvable(under.output+"-<i>l</i>1", 
          n+1, new Seq(s.left.slice(j,i),s.left[i].arg[0]))
            && isProvable(under.output+"-<i>l</i>2", n+1, new Seq(concat(s.left.slice(0,j),
                 modify(s.left.slice(i),0,s.left[i].arg[1])),s.right))) return true;
        else proof = proof.slice(0,l);
//      return false;
    }

    if (s.left[i].symbol==over) {// /-left
      for (var j=i; j<s.left.length; j=j+1) // sigma=s.left[i+1..j], delta=s.left[j+1..end]
        if (isProvable(over.output+"-<i>l</i>1", 
          n+1, new Seq(s.left.slice(i+1,j+1),s.left[i].arg[1]))
            && isProvable(over.output+"-<i>l</i>2", 
          n+1, new Seq(concat(modify(s.left.slice(0,i+1),i,s.left[i].arg[0]),
                 s.left.slice(j+1)),s.right))) return true;
        else proof = proof.slice(0,l);
//      return false;
    }
  }

  if (s.right.symbol==join) // join-right
    if (isProvable(join.output+"-<i>r</i>1", n, new Seq(s.left,s.right.arg[0])))
      return true;
    else {
      proof = proof.slice(0,l);
      if (isProvable(join.output+"-<i>r</i>2", n, new Seq(s.left,s.right.arg[1])))
        return true;
      else {proof = proof.slice(0,l);}// return false;}
    }

  if (s.right.symbol==times) { // ;-right
    for (var i=0; i<=s.left.length; i=i+1) 
      if (isProvable(times.output+"-<i>r</i>1", n+1, new Seq(s.left.slice(0,i),s.right.arg[0]))
        && isProvable(times.output+"-<i>r</i>2", n+1, new Seq(s.left.slice(i),s.right.arg[1]))) 
        return true;
      else proof = proof.slice(0,l);
//    return false;
  }

  if (s.right.symbol==star) { // *-right (3 rules)
//parent.output.document.write("@");
    if (isProvable(star.output+"-<i>r</i>1", n+1, new Seq(s.left,new Expr(unit,[])))) return true;
    else proof = proof.slice(0,l);
    if (isProvable(star.output+"-<i>r</i>x", n+1, new Seq(s.left,s.right.arg[0]))) return true;
    else proof = proof.slice(0,l);
    for (var i=1; i<s.left.length; i=i+1) {
//parent.output.document.write("#");
      if (isProvable(star.output+"-<i>r</i>a", n+1, new Seq(s.left.slice(0,i),s.right))
        && isProvable(star.output+"-<i>r</i>b", n+1, new Seq(s.left.slice(i),s.right))) 
        return true;
      else proof = proof.slice(0,l);
    }
//    return false;
  }

  if (s.left.length>0 && s.left[0].symbol==star) {// *-leftleft
//parent.output.document.write("#");
    if (isProvable(star.output+"-<i>ll</i>1", 
      n+1, new Seq(s.left.slice(1),s.right))
        && isProvable(star.output+"-<i>ll</i>2", 
      n+1, new Seq(s.left[0].arg.concat([s.right]),s.right))) return true;
    else proof = proof.slice(0,l);
  }

  if (s.left.length>0 && s.left[s.left.length-1].symbol==star) // *-leftright
    if (isProvable(star.output+"-<i>lr</i>1", 
      n+1, new Seq(s.left.slice(0,s.left.length-1),s.right))
        && isProvable(star.output+"-<i>lr</i>2", 
      n+1, new Seq(concat([s.right],s.left[s.left.length-1].arg),s.right))) return true;
    else {proof = proof.slice(0,l);}

  proof = proof.slice(0,l);
  return false;
}

function showProof(s) {
  proof=[];
  proofattempt=[];
  if (isProvable("",0,s))
    document.write(proof.join("")+"true<br>");
  else
    document.write(proofattempt.join("")+"false<br>");
}

function pr2str(s) {
  proof=[];
  proofattempt=[];
  if (isProvable("",0,s))
    return proof.join("")+"true<br>";
  else
    return proofattempt.join("")+"false<br>";
}

function b(a1,sym,a2) {
  return new Expr(sym,[a1,a2]);
}

function eq2leq(eqn){
  return b(eqn.arg[0],leq,eqn.arg[1]);
}

function eq2geq(eqn){
  return b(eqn.arg[1],leq,eqn.arg[0]);
}

function leq2seq(le){
  return new Seq([le.arg[0]],le.arg[1]);
}