/* PCP: Point and Click Proofs, Peter Jipsen, March 2001
   www.math.vanderbilt.edu/~pjipsen/PCP/PCPproofs.js

   Requires: www.math.vanderbilt.edu/~pjipsen/PCP/math2html.js
   Examples: www.math.vanderbilt.edu/~pjipsen/PCP/PCPmain.html
*/

function obj2str(obj, obj_name) {
  var result = ""
  for (var i in obj)
    result += i + " = " + obj[i] + "; "
  return result
}

function equalExpr(p,q) {
if (p==null || q==null || p.symbol==null || q.symbol==null) {
  document.write(obj2str(p),obj2str(q),"*******equalExpr*******");
  return false;
}
  if (p.symbol.name!=q.symbol.name) return false;
  if (p.arg.length!=q.arg.length) return false;
  if (p.arg.length==0) return true;
  for (var i=0; i<p.arg.length; i++)
    if (!equalExpr(p.arg[i],q.arg[i])) return false;
  return true;
}

function conj2list(q,li) {
  if (q.symbol==andSymbol) {
    li=conj2list(q.arg[0],li);
    li=conj2list(q.arg[1],li);
  } else add(li,q);
  return li;
}

function checkConjList(conj,li) {
// check that conjuncts in conj match the formulas in li
  var cli=conj2list(conj,[]);
  if (cli.length!=li.length) return false;
  for (var i=0; i<cli.length; i++) {
    if (!equalExpr(cli[i],li[i])) return false;
  }
  return true;
}

function getElement(pr,li) {
  var elt=pr;
  for (var i=0; i<li.length; i++)
    elt=elt[li[i]];
  return elt;
}

function getSubproof(pr,li) {
  var elt=pr;
  for (var i=0; i<li.length-1; i++)
    elt=elt[li[i]];
  return elt;
}

function clone(t) {
  var b=[];
  for (var i=0; i<t.arg.length; i++)
    b[i]=clone(t.arg[i]);
  return new Expr(t.symbol,b,0);
}

// a substitution is a list of terms with sub[i] to replace vari[i]
function appl(t,sub) {
  if (t.symbol.vari || t.symbol.formulavari) 
    if (sub[t.symbol.index]==null) 
      return clone(currentSubstitution[t.symbol.index]);
    else return clone(sub[t.symbol.index]);
  var a=[];
  for (var i=0; i<t.arg.length; i++)
    a[i]=appl(t.arg[i],sub);
  return new Expr(t.symbol,a,0);
}

function checkProof(pr,cpr,ns) {//make it work for linear subproofs
  for (var i=0; i<cpr.length; i++)
    if (cpr[i].length==null) {
      if (cpr[i].conclude) {
        if (cpr[i].expr.symbol!=impSymbol) return "Conclusion not an implication at "+ns+i;
        if (cpr[i-1].length==null) return "No subproof above conclusion at "+ns+i;
        if (!equalExpr(cpr[i].expr.arg[1],
             cpr[i-1][cpr[i-1].length-1].expr)) return "Last line of subproof differs from conclusion at "+ns+i;
        var premList=[];
        for (var j=0; j<cpr[i-1].length; j++)
          if (cpr[i-1][j].assume) add(premList,cpr[i-1][j].expr);
        if (!checkConjList(cpr[i].expr.arg[0],premList)) return "Assumptions of subproof differ from premises of conclusion at "+ns+i;
      }
      if (cpr[i].apply) {
        var r=getElement(pr,cpr[i].rule);
        var sr=appl(r.expr,cpr[i].subst);
        if (sr.symbol==impSymbol) {
          var premList=[];
          for (var j=0; j<cpr[i].premises.length; j++)
            add(premList,getElement(pr,cpr[i].premises[j]).expr);
          if (!checkConjList(sr.arg[0],premList)) return "Premises do not match rule at "+ns+i;
          if (!equalExpr(sr.arg[1],cpr[i].expr)) return "Formula does not match rule conclusion at "+ns+i;
        } else if (!equalExpr(sr,cpr[i].expr)) return "Formula does not match rule at "+ns+i;
      }
    } else {
      var result=checkProof(pr,cpr[i],ns+i+".");
      if (result!=true) return result;
    }
  return true;
}

firstGap=[];
currentFocus=[]; //pointer into the current proof

function updateCurrentF(pr,ns) {
  for (var i=0; i<pr.length; i++)
    if (pr[i].length==null) {
      if (pr[i].focusAbove!=null) currentFocus=(ns+i).split(".");
      if (pr[i].gap && firstGap.length==0) firstGap=(ns+i).split(".");
    }
    else updateCurrentF(pr[i],ns+i+".");
}

function updateCurrentFocus(pr,ns) {
  firstGap=[];
  currentFocus=[];
  updateCurrentF(pr,ns);
  if (currentFocus.length==0 && firstGap.length!=0) {
    currentFocus=firstGap;
    var subpr=getSubproof(currentProof,currentFocus);
    getElement(currentProof,currentFocus).focusAbove=subpr[0].consider!=null;
  }
}

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

sp=" &nbsp; &nbsp; &nbsp; ";

function less(ind1,ind2) { //return true if ind2 is in the scope of ind1
  for (var i=0; i<ind1.length; i++)
    if (i==ind2.length || parseInt(ind1[i])>parseInt(ind2[i]) ||
      parseInt(ind1[i])<parseInt(ind2[i]) && i<ind1.length-1) return false;
  return true;
}

showFlag=true;

function proof2html(p,pr,indent,ns) {
  var st="";
  var s=" ";
  for (var i=0; i<pr.length; i++) {
    if (pr[i].length==null) {
    if (showFlag || (!pr[i].gap || pr[i].focusAbove!=null)) {
      if (i>=10) s="";
      if (less((ns+i).split("."),currentFocus) && 
          (pr[i].expr.symbol.pred || pr[i].expr.symbol.conn) || pr[i].gap &&
          (pr[i-1].expr.symbol.pred || pr[i-1].expr.symbol.conn))
        st=st+"<input type=button value=\""+s+ns+i+s+
          "\" onClick=\"parent.applyRule(\'"+ns+i+"\')\">";
      else st=st+"&nbsp;"+s+ns+i+s;
      st=st+space(indent);
      if (pr[i].apply) {
        var r=pr[i];
//document.write(obj2str(r),"**<br>");
        var q=getElement(p,r.rule);
        if (pr[0].consider) st=st+q.expr.symbol.output;
        st=st+e2s(r.expr);
        st=st+sp+"(by "+(q.name==null?r.rule.join("."):q.name);
        if (r.premises!=null)
          for (var j=0; j<r.premises.length; j++) {
            q=getElement(p,r.premises[j]);
            st=st+", "+(q.name==null?r.rule.join("."):q.name);
          }
//        for (var j=0; j<pr[i].subst.length; j++)
//          st=st+", &nbsp;"+vari[j].output+" := "+e2s(pr[i].subst[j]);
        st=st+")";
      } else st=st+e2s(pr[i].expr);
      if (pr[i].axiom) st=st+sp+"(axiom)";
      if (pr[i].assume) st=st+sp+"(assume)";
      if (pr[i].conclude) st=st+sp+"(conclude)";
      if (pr[i].focusAbove!=null) {
        currentFocus=(ns+i).split(".");
        subprFocus=i+(pr[i].focusAbove?-1:1);
        if (pr[i].focusAbove) st=st+"<input type=button value=\"undo"+
          "\" onClick=\"parent.undoAbove()\">...<input type=button "+
          "value=\" v \" onClick=\"parent.focusBelow(\'"+ns+i+"\')\">..."+
       "<input type=button value=\"hide/show\" onClick=\"parent.hideshow()\">";
        else st=st+"<input type=button value=\" ^"+
          " \" onClick=\"parent.focusAbove(\'"+ns+i+"\')\">...<input "+
          "type=button value=\"undo\" onClick=\"parent.undoBelow()\">..."+
       "<input type=button value=\"hide/show\" onClick=\"parent.hideshow()\">";
      } else if (pr[i].gap) st=st+"<input type=button value=\" ^"+
          " \" onClick=\"parent.focusAbove(\'"+ns+i+"\')\">...<input type=button "+
          "value=\" v \" onClick=\"parent.focusBelow(\'"+ns+i+"\')\">...";
      if (pr[i].name!=null) 
        if (pr[i].name[0]=="(") st=st+" &nbsp; "+pr[i].name;
        else st=st+" &nbsp; <b>"+pr[i].name+"</b>";
      st=st+"<br>\n";
    }
    } else if (showFlag || i==currentFocus[indent-1])
      st=st+proof2html(p,pr[i],indent+1,ns+i+".");
  }
  return st; 
}

function hideshow() {
  showFlag=!showFlag;
  proof.location.href="PCPproof.html"
}

function undoAbove() {//modify currentProof and redisplay
  var fo=getElement(currentProof,currentFocus);
  var subpr=getSubproof(currentProof,currentFocus);
  if (subprFocus>0 && !subpr[subprFocus].axiom &&
      subpr[subprFocus].name==null) {
    for (var i=subprFocus; i<subpr.length-1; i++) //delete above
      subpr[i]=subpr[i+1];
    subpr.length--;
  } else if (subpr.length==3 && currentFocus.length>1) {
    subpr=getSubproof(currentProof,currentFocus.slice(0,currentFocus.length-1));
    subpr[currentFocus[currentFocus.length-2]]=
      subpr[currentFocus[currentFocus.length-2]][1];
  }
  if (list.length!=0) {
    list=[];
    choose.location.href="PCPchoose.html";
  }
  proof.location.href="PCPproof.html";
}

function undoBelow() {//modify currentProof and redisplay
  var fo=getElement(currentProof,currentFocus);
  var subpr=getSubproof(currentProof,currentFocus);
  if (subprFocus<subpr.length-1 && !subpr[subprFocus].axiom &&
      subpr[subprFocus].name==null) {
    for (var i=subprFocus; i<subpr.length-1; i++) //delete above
      subpr[i]=subpr[i+1];
    subpr.length--;
    subpr[subprFocus]={expr:subpr[subprFocus].expr};
  } else if (subpr.length==3 && currentFocus.length>1) {
    subpr=getSubproof(currentProof,currentFocus.slice(0,currentFocus.length-1));
    subpr[currentFocus[currentFocus.length-2]]=
      subpr[currentFocus[currentFocus.length-2]][1];
  }
  if (list.length!=0) {
    list=[];
    choose.location.href="PCPchoose.html";
  }
  proof.location.href="PCPproof.html";
}

function focusAbove(st) {//modify currentProof and redisplay
  var ind=st.split(".");
  getElement(currentProof,currentFocus).focusAbove=null;
  getElement(currentProof,ind).focusAbove=true;
  if (list.length!=0) {
    list=[];
    choose.location.href="PCPchoose.html";
  }
  proof.location.href="PCPproof.html";
}

function focusBelow(st) {//modify currentProof and redisplay
  var ind=st.split(".");
  getElement(currentProof,currentFocus).focusAbove=null;
  getElement(currentProof,ind).focusAbove=false;
  if (list.length!=0) {
    list=[];
    choose.location.href="PCPchoose.html";
  }
  proof.location.href="PCPproof.html";
}

function displayExprList(li) {
document.writeln("=================<br>");
  for (var i=0; i<li.length; i++)
    document.writeln(i,". ",e2s(li[i]),"<br>");
}

substList=[];
premsList=[];

function match(q,t,sub) {
// Find substitution such that q==sub(t); return true if found.
//displayExprList(sub);
  if (t.symbol.vari)
    if (sub[t.symbol.index]==null) {
      if (q.symbol.conn || q.symbol.pred || q.symbol.formulavari) return false;
      sub[t.symbol.index]=q;
      if (substList.length<defaultSubstitution.length)
        add(substList,t.symbol.index);
      return true;
    } else 
      return equalExpr(sub[t.symbol.index],q);
  if (t.symbol.formulavari) {
    if (sub[t.symbol.index]==null) {
      if (q.symbol.vari || q.symbol.cons || q.symbol.oper) return false;
      sub[t.symbol.index]=q;
      return true;
    } else 
      return equalExpr(sub[t.symbol.index],q);
  }
  if (t.symbol.name!=q.symbol.name) return false;
  if (t.arg.length!=q.arg.length) return false;
  for (var i=0; i<t.arg.length; i++)
    if (!match(q.arg[i],t.arg[i],sub)) return false;
  return true;
}

function allrewrites(q, stq, ind, s, t, ri, fw, li, subexpr) {
// Find all subst such that subst[i](s) is a subterm of q 
// and replace this subterm by subst[i](t)
  var sub=[];
  if (match(stq.arg[ind],s,sub)) {
    var temp=stq.arg[ind];
    stq.arg[ind]=appl(t,sub);
    add(li,{expr:clone(q.arg[0]),apply:true,rule:ri,forward:fw,
            pos:[],subst:sub});
    stq.arg[ind]=temp;
  }
  if (subexpr) // match subexpr if not leq or implies
    for (var i=0; i<stq.arg[ind].arg.length; i++) 
      allrewrites(q,stq.arg[ind],i,s,t,ri,fw,li,subexpr);
}

function oneStepEq(q,ru,ri,above) { 
// q focus expr, ru rule applied, side above/below
// return list of expressions after substitution, with rule
  var li=[];
  var nq=new Expr(minus,[q],0);
  var iffeq=ru.symbol==eq || ru.symbol==iffSymbol;
  if (iffeq || above)
    allrewrites(nq,nq,0,ru.arg[0],ru.arg[1],ri,true,li,iffeq);
  if (iffeq || !above)
    allrewrites(nq,nq,0,ru.arg[1],ru.arg[0],ri,false,li,iffeq);
  return li;
}

function matchConj(te,conj,sub,sl,li) {
// updates sub while looking for match of all conjuncts in te
// updates list of matching formulas, and substitution
  if (conj.symbol!=andSymbol) {
    for (var i=0; i<te.length; i++) {
      if (match(te[i].expr,conj,sub))
        add(li,{subst:sub.slice(0,sub.length),
          premises:premsList.concat([te[i].index])});
      if (substList.length>sl) {
        for (var j=sl; j<substList.length; j++)
          sub[substList[j]]=null;
        substList.length=sl;
      }
    }
  } else
    for (var i=0; i<te.length; i++) {
      if (match(te[i].expr,conj.arg[1],sub)) {
        add(premsList,te[i].index);
        matchConj(te,conj.arg[0],sub,substList.length,li);
        premsList.length--;
      }
      if (substList.length>sl) {
        for (var j=sl; j<substList.length; j++)
          sub[substList[j]]=null;
        substList.length=sl;
      }
    }
}

function oneStepForward(te,ru,ri) { 
// te = true expr, ru rule applied
// return list of expressions after substitution, with rule
  var li=[];
  var sub=[];
  var concli=[];
  substList=[];
  premsList=[];
  matchConj(te,ru.arg[0],sub,0,li);
  for (var i=0; i<li.length; i++)
    add(concli,{expr:appl(ru.arg[1],li[i].subst),apply:true,rule:ri,
            premises:li[i].premises,subst:li[i].subst});
  li=[];
  if (ru.symbol==iffSymbol) {
    matchConj(te,ru.arg[1],sub,0,li);
    for (var i=0; i<li.length; i++)
      add(concli,{expr:appl(ru.arg[0],li[i].subst),apply:true,rule:ri,
            premises:li[i].premises,subst:li[i].subst});
  }
  return concli;
}

var currentTrueExpr=[];

function findTrueE(pr,indent,ns) {
  var ind;
  for (var i=0; i<pr.length; i++)
    if (pr[i].length==null) {
      ind=(ns+i).split(".");
      if (less(ind,currentFocus) && !pr[i].gap)
        add(currentTrueExpr,{expr:pr[i].expr, index:ind});
    }
    else if (i==currentFocus[indent]) findTrueE(pr[i],indent+1,ns+i+".");
}

function findTrueExpr() {
  currentTrueExpr=[];
  findTrueE(currentProof,0,"");
  return currentTrueExpr;
}

function applyRule(st) {
// uses currentFocus +1 or -1
// calculate possible next steps, store in list
// display choices in a new frame
  currentRuleStr=st;
  var ind=st.split(".");
  var ru=getElement(currentProof,ind);
  var fo=getElement(currentProof,currentFocus);
  var subpr=getSubproof(currentProof,currentFocus);
  var ex=subpr[subprFocus];
//alert("currentFocus="+currentFocus);
  if (ru.gap) {//make linear subproof for =, <= or iff, subproof for implies
    var gi=parseInt(ind[ind.length-1]);
    subpr=getSubproof(currentProof,ind);
    var gf=(subpr[gi].focusAbove==null?null:subpr[gi].focusAbove);
    if (subpr[gi+1].expr.symbol==impSymbol) {
      var spr=[];
      var cli=conj2list(subpr[gi+1].expr.arg[0],[]);
      for (var i=0; i<cli.length; i++)
        add(spr,{expr:appl(cli[i],constantSubst), assume:true});
      add(spr,{expr:subpr[gi].expr, gap:true, focusAbove:(gf==null?false:gf)});
      add(spr,{expr:appl(subpr[gi+1].expr.arg[1],constantSubst)});
      subpr[gi]=spr;
    } else subpr[gi]=[{expr:subpr[gi+1].expr.arg[0], consider:true},
               {expr:subpr[gi].expr, gap:true, focusAbove:true},
               {expr:subpr[gi+1].expr.arg[1]}];
    subpr[gi+1].conclude=true;
    if (gf==null) 
      getElement(currentProof,currentFocus).focusAbove=null;
    if (list.length!=0) {
      list=[];
      choose.location.href="PCPchoose.html";
    }
    proof.location.href="PCPproof.html";
  } else if (subpr[0].consider) {
//linear proof, attempt to apply rule only to expr
    list=oneStepEq(ex.expr,ru.expr,ind,fo.focusAbove);
  } else if (fo.focusAbove) {
//match premises of rule to some earlier proof steps
//or insert instance of atomic rule
    list=[];
//    if (ru.expr.symbol.pred)  // uncomment to avoid long instances
      list=[{expr:appl(ru.expr,currentSubstitution), apply:true, rule:ind,
        subst:currentSubstitution}];
// find substitution so that all premises of rule match true expressions
// add conclusion of rule to list
    var te=findTrueExpr();
    list=list.concat(oneStepForward(te,ru.expr,ind));
//    list=list.concat(oneStepEq(ex.expr,ru.expr,ind,fo.focusAbove));
  } else { //focus below, not in linear proof
// attempt to match ex to instance of ru, close gap if success
    var sub=[];
    if (match(ex.expr,ru.expr,sub)) { //close gap
      ex.rule=ind;
      ex.apply=true;
      for (var i=subprFocus-1; i<subpr.length-1; i++) //delete gap
        subpr[i]=subpr[i+1];
      subpr.length--;
      proof.location="PCPproof.html";
    } else { //no direct match
      if (ru.expr.symbol==eq || ru.expr.symbol==iffSymbol) 
        list=oneStepEq(ex.expr,ru.expr,ind,fo.focusAbove);
      else list=[];
      if (ru.expr.symbol==impSymbol || ru.expr.symbol==iffSymbol) {
//match (each of) conclusion(s) of rule to expr
        var cli=conj2list(ru.expr.arg[1],[]);
        for (var i=0; i<cli.length; i++) {
          var sub=[];
          if (match(ex.expr,cli[i],sub))
            add(list,{expr:appl(ru.expr.arg[0],sub), apply:true, rule:ind, 
              subst:sub});
        }
      }
    }
  }
  choose.location="PCPchoose.html";
}

function updateCurrentProof(nextStepChoice) {
// add next step to currentProof

  var fo=getElement(currentProof,currentFocus);
  var subpr=getSubproof(currentProof,currentFocus);
//  var linearSubpr=subpr[0].consider;
  if (fo.focusAbove) {
    if (equalExpr(list[nextStepChoice].expr,subpr[subprFocus+2].expr)) {
//subproof is complete
//also check all rules are =,iff (if conclusion is =,iff) or <= ******
      var ind=subprFocus+1;
      for (var i=ind; i<subpr.length-1; i++) //delete gap
        subpr[i]=subpr[i+1];
      subpr.length--;
      subpr[ind]=list[nextStepChoice];
    } else {
      var ind=subprFocus+1;
      for (var i=subpr.length; i>ind; i--)
        subpr[i]=subpr[i-1];
      subpr[ind]=list[nextStepChoice];
    } 
  } else {//fo.focusBelow
    nex=list[nextStepChoice].expr;
    if ((nex.symbol==eq || nex.symbol==iffSymbol) && 
       equalExpr(nex.arg[0],nex.arg[1])) {
      var ind=subprFocus;
      subpr[ind-1]={expr:nex, name:"(by equality)"};
      list[nextStepChoice].expr=subpr[ind].expr;
      if (subpr[ind].name!=null) list[nextStepChoice].name=subpr[ind].name;
      subpr[ind]=list[nextStepChoice];
   } else {
    if (subpr[0].consider) {
      var cli=[list[nextStepChoice].expr];
      var eqli=[{expr:subpr[subprFocus-2].expr,
    index:currentFocus.slice(0,currentFocus.length-1).concat([subprFocus-2])}];
    } else {
      var cli=conj2list(list[nextStepChoice].expr,[]); //list of premises
      var eqli=findTrueExpr();
    }
    var newli=[];
    var prems=[];
    for (var i=0; i<cli.length; i++) {
      var j=0;
      while (j<eqli.length && !equalExpr(cli[i],eqli[j].expr)) j++;
//record what premises are used ********
      if (j==eqli.length) add(newli,cli[i]); //new premise, still to be proved
      else add(prems,eqli[j].index);
    }
    if (newli.length==0) {
//subproof is complete
//in linear proof also check all rules are = (if conclusion is =) or <= ******
      var ind=subprFocus-1;
      for (var i=ind; i<subpr.length-1; i++) //delete gap
        subpr[i]=subpr[i+1];
      subpr.length--;
      list[nextStepChoice].expr=subpr[ind].expr;
      if (subpr[ind].name!=null) list[nextStepChoice].name=subpr[ind].name;
      subpr[ind]=list[nextStepChoice];
      subpr[ind].premises=prems;
    } 
    else // add newli expr
    {
      var ind=subprFocus;
      for (var i=subpr.length+2*newli.length-2; i>ind+2*newli.length-2; i--)
        subpr[i]=subpr[i-2*newli.length+1];
      for (var i=0; i<newli.length-1; i++) {
        subpr[ind+2*i]={expr:newli[i]};
        subpr[ind+2*i+1]={expr:subpr[ind-1].expr,gap:true};
      }
      subpr[ind+2*newli.length-2]={expr:newli[newli.length-1]};
      ind=ind+2*newli.length-1;
      list[nextStepChoice].expr=subpr[ind].expr;
      if (subpr[ind].name!=null) list[nextStepChoice].name=subpr[ind].name;
        subpr[ind]=list[nextStepChoice];
    } 
   }
  }
  list=[];
// load new page into proof frame
  proof.location.href="PCPproof.html";
  choose.location.href="PCPchoose.html";
}

function findVariables(q,li) {//modify li to contain all variables in q
  if (q.arg.length==0) {
    if (q.symbol.vari || q.symbol.formulavari)
      li[q.symbol.index]=true;
  } else 
    for (var i=0; i<q.arg.length; i++)
      findVariables(q.arg[i],li);
}

function applySubst(eltli,varli) {
  currentSubstitution=defaultSubstitution.slice(0,defaultSubstitution.length);
  var j=list.length;
  for (var i=0; i<varli.length; i++)
    if (varli[i]) {
      currentSubstitution[i]=parse(eltli[j].value);
      j++;
    }
  applyRule(currentRuleStr);
  choose.location.href="PCPchoose.html";
}

function parseProof(pr) {//modifies pr
  for (var i=0; i<pr.length; i++) 
    if (pr[i].length==null) {
      if (typeof pr[i].expr == "string") 
        pr[i].expr=parse(pr[i].expr);
      if (pr[i].subst!=null) 
        for (var j=0; j<pr[i].subst.length; j++)
          if (typeof pr[i].subst[j] == "string") 
            pr[i].subst[j]=parse(pr[i].subst[j]);
    } else parseProof(pr[i]);
}

defaultSubstitution=[parse("x"),parse("y"),parse("z"),
parse("u"),parse("v"),parse("w"),parse("P"),parse("Q"),parse("R")];
currentSubstitution=defaultSubstitution;
constantSubst=[parse("a"),parse("b"),parse("c"),parse("d"),parse("p"),
  parse("q")];

list=[];  //store choices of next expression
subprFocus=0;
currentRuleStr="";