// The JavaScript Program to implement an equational decision procedure for Residuated Lattices
//  version of 5 June 2000, by Peter Jipsen, http://proof.mth.uct.ac.za/~pjipsen

// The code has three 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 decision procedure.
// 3. Administering the RL quiz

// Part 1. Handling formulas

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:"T", arity:0, output:"T"};

cons = [ zero, unit, topp ];

meet = {name:"^", arity:2, priority:6,
   output:'&nbsp;<font face="Symbol" color="Blue">Ù</font>&nbsp;', infix:true, paren:true};
join = {name:"v", arity:2, priority:6,
   output:'&nbsp;<font face="Symbol" color="Blue">Ú</font>&nbsp;', infix:true, paren:true};
times = {name:"*", arity:2, priority:8,
   output:'<font color="Blue"><tt>*</tt></font>', 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};

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

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:'<font face="Symbol" color="Red"> £ </font>', 
  infix:true,  priority:4};
geq  = {name:">=", arity:2, output:'<font face="Symbol" color="Red"> ³ </font>', 
  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 face="Symbol" color="Blue">Ø</font>'};
impSymbol = {name:"->", arity:2, priority:1,
  output:'&nbsp;<font face="Symbol" 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) { //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;
  str=removeCharsAndBlanks(str,0);
  symbol=getSymbol(str); //either a symbol or a bracket or empty
  if (symbol==null||symbol==rightBracket||symbol==rightSqBracket) 
    return [null,"Error, '(', '[' or symbol expected: "+str];
  str=removeCharsAndBlanks(str,symbol.name.length); 

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

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

  } else if (symbol==null) {
    return [null,"Error, incorrect symbol : "+symbol.name+" "+str];

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

  } else {                          //read prefix expr1 ... exprN or prefix(...)
    if (symbol.infix) return [null,"Error, misplaced infix symbol: "+symbol.name+" "+str];
    var more = true;
    nextsymbol = getSymbol(str);
    var commas=false;
    if (nextsymbol==leftBracket) {
      str = removeCharsAndBlanks(str,symbol.name.length);
      commas=true;
    }
    while (str!="" && more) {
      nextsymbol = getSymbol(str);
      if (nextsymbol==null) return [null,"Error, incorrect symbol: "+str];
      estr=str2expr(str);expr=estr[0];str=estr[1];
      if (str.slice(0,5)=="Error") return [null,str];
      add(arg,expr);
      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);
  }

//parse right argument of infix operation
  symbol = getSymbol(str);
  var insert=null;
  if (symbol==null || !symbol.infix) return [expr,str];
  str = removeCharsAndBlanks(str,symbol.name.length);
  if (str=="" || str.charAt(0)==")" || str.charAt(0)=="]") { //unary infix symbol
    expr=new Expr(symbol, [expr], maxPriority); 
//document.write(symbol.name+expr);
    return [expr,str];
  }
  var right=null;
  estr = str2expr(str);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);
  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+" !- "+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) {
  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;
//document.write(space(n)+seq2str(s)+"&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"+reason+"<br>");
  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;
  }
  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]);
}


//**************************************
// Part 3. Administering the RL quiz


//generate inequations for quiz
inequations=[];
for (var i=0; i<5; i=i+1)
  add(inequations,b(randomTerm(2),leq,randomTerm(2)));

function correct(win, score, st) {
  win.document.write("<font color=Green>Correct, "+st+", 1 point.</font>");
  return score+1;
}

function wrong(win, score, st) {
  win.document.write("<font color=Red>Wrong, "+st+", -1 point.</font>");
  return score-1;
}

function comment(win, st) {
  win.document.write("<center><font color=Blue>"+st+"</font></center>");
}

function check(frm) { //analyse the radio buttons and output results
  win=open("", "resultWindow", "height=450,width=750,menubar=yes,resizable=yes,scrollbars=yes");
  win.document.open();
  var score=0;
  win.document.write("<html><head><title>Quiz Results");
  win.document.write("</title></head><body><h3 align=center>"+
    "Results for your personalised Quiz 1</h3>");
  for (var i=0; i<inequations.length; i=i+1){
    win.document.write((i+1)+". &nbsp; "+
      e2s(inequations[i])+"&nbsp;&nbsp; ");
    proof=[];
    proofattempt=[];
    var ans=isProvable("",0,leq2seq(inequations[i]));
    if (!frm.elements[2*i].checked && !frm.elements[2*i+1].checked)
      win.document.write("Undecided, 0 points");
    else if (ans)
      if (frm.elements[2*i].checked)
        score=correct(win, score, "this is True in RL");
      else
        score=wrong(win, score, "this is True in RL");
    else if (frm.elements[2*i+1].checked)
      score=correct(win, score, "this is False in RL");
    else
      score=wrong(win, score, "this is False in RL");
  win.document.write("<br>");
  }
  win.document.write("<h3 align=center><font color=Red>"+
    "Your Score is "+score+"/"+inequations.length+"</font></h3>");
  if (score<1) comment(win,"Guessing will get you nowhere :-)");
  else if (score<inequations.length/2) 
    comment(win,"You need to practise your RL derivations :-)");
  else if (score<0.75*inequations.length) comment(win,"RL inequations can be quite tricky.");
  else if (score<inequations.length) 
    comment(win,"Pretty good, you seem to know what you are doing.");
  else comment(win,"Congratulations, you're an expert!");
  win.document.write('<p><center>Click the X in the top right '+
    'hand corner to close this window</center>');
  win.document.write('<p>Here are the Gentzen sequent proofs and proof attempts '+
    'for the above inequalities:');
  for (var i=0; i<inequations.length; i=i+1){
    win.document.write("<p><b>"+(i+1)+". &nbsp; "+e2s(inequations[i])+"</b><p>"+
       pr2str(leq2seq(inequations[i])));
//    showProof(win, leq2seq(inequations[i]));
  }
  win.document.write("</body></html>");
  win.document.close();  
}