******************************************************************************
*** PLA based on IMaude
***  comparing graphs 
***  based on a non-explorable xnet
***  the only ops are xnet2tkb and compare?

******************************************************************************
mod PLA-COMPARE is

  inc RFE .
  inc PLA-AUX .
  inc STATUS-AUX .

****  inc META-PETRI .
****  inc PNTL2GRAPH .
  inc NEW-GRAPH2G2D .
  inc PLA-EXPLORE .


******************************************************************************
*** Variables
******************************************************************************
var ctl : Control .
var wait4s : Wait4Set .
var reqQ reqQ' reqQ0 reqQ1 reqQ2 : RequestQ .
vars es es' : ESet .
var ee : Entry .
var ee? : Entry? .
var log : Log .


vars outQ toks toks' anc0 anc1 : QidList .
vars mname pname gname newgname newpname kbname ukbname type g2dvname : Qid .
vars modname modname0 modname1 name0 gname0 name1 gname1 pgname cgname : Qid .
vars b b0 fail : Bool .
vars ctr ctr1 title subtitle ?string choices : String .
vars notes notes' gnotes pnotes xnotes opnotes : Notes .
vars graph0 graph1 graph01 ?graph ?graph' : Graph .
var res?? : [ResultPair?] .
vars t0 t1 pntlT pntlT0 pntlT1 xstateT : Term .
vars ndl ndl' ndl'' ndl0 ndl1 : NodeList .
vars edl edl' edl0 edl1 : EdgeList .
vars nid src tgt : Nat .

******************************************************************************
*** compare selection dialog
******************************************************************************
  op compareSelectTemplate : -> String .
  eq compareSelectTemplate = "(apply compareSelect %gname %choices)" .

  op mkCompareSelectExp : ESet Qid String -> String .
  eq mkCompareSelectExp(es,gname,choices) = 
        fillTemplate(compareSelectTemplate, 
             (("%gname" :~ squote(string(gname))),
             ("%choices" :~ "(array java.lang.Object " + choices + ")"))
           )
      [owise] .

  eq mkCompareSelectExp(e('gval,cgname,gnotes,gv(?graph)) ! es,gname,choices) = 
      mkCompareSelectExp(es, gname,
         (if gname == cgname or isKB(e('gval,cgname,gnotes,gv(?graph)),cgname)
             or graphNodes(?graph) == nil
          then choices
          else choices + " " +
           fillTemplate(stringArrayTemplate,
               ("%strings" :~  squote(string(cgname)) + " " +
         squote(svalString(lookupd(gnotes,"title",sv(string(cgname))))) + " " +
         squote(svalString(lookupd(gnotes,"subtitle",sv(""))))
         ) ) fi)  ) .
  


******************************************************************************

***(
(compareGraphs gname g2dvname cgname toks)

form the join of the graphs
set compare attribute of the nodes -- left,right,both

form the underlying pnet -- 
  an xnet -- its scope and graph are the joined graph
          -- its source is itself

Define graph -- needs to set the compare attributes ala DefineXGraph
Need to define colorCompareGraph
)

*******************************************************************************
**** The viewer request
**** Pop up dialog with compareGraphsCont continuation
*******************************************************************************

  eq isReq('compareGraphsChoose) = true .
****                          from gname (left graph)
  eq enabled(wait4s,
             req('compareGraphsChoose,ql(gname g2dvname toks),reqQ)) 
        = not(waiting4(wait4s,g2dvname)) .


 crl[compareGraphsChoose]:
   [nil,
    st(processing(req('compareGraphsChoose, 
                      ql(gname g2dvname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, 
       wait4s, 
       reqQ reqQ0, es, log),
    outQ
    g2dvname '\n mname '\n toks' maudePrompt ]
  if mname :=  getMaudeName(es)
  /\ ?string := withAck(mkCompareSelectExp(es,gname,""), mname,g2dvname) 
  /\ toks' := str2toks(?string)
  /\ reqQ0 :=
       (if isXnetG(es,gname) 
       then req('startcListener,ql(gname 'serializingListener g2dvname), reqQ')
       else reqQ' fi) .




*******************************************************************************
  eq isReq('compareGraphs) = true .
****                          from gname (left graph)
  eq enabled(wait4s,
             req('compareGraphs,ql(gname g2dvname cgname  toks),reqQ)) 
           = true .
 crl[compareGraphs]:
   [nil,
    st(processing(req('compareGraphs, 
                      ql(gname g2dvname cgname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, (if b then incGlobalCounter(es',2) else es' fi), 
       log),
    outQ]
   if ctr := getGlobalCounter(es) 
   /\ ctr1 := stringInc(ctr) 
   /\ newpname := qid("xpnet" + ctr)
   /\ newgname := qid("graph" + ctr1)
   /\ {b,es'} := compareGraphs(es,gname,cgname,newgname,newpname)
   /\ reqQ1 := 
       (if not(b)
        then req('logreq,
                  ql('compareGraphs 'failed gname  g2dvname cgname),reqQ')
        else req('defineGraph,ql(g2dvname newgname),
                req('showGraph,ql(g2dvname newgname),
                   req('startcListener,ql(newgname 'serializingListener g2dvname),
                       reqQ')))
            fi)
   /\ reqQ0 :=
       (if isXnetG(es,gname)
        then req('startcListener,ql(gname 'serializingListener g2dvname),reqQ1)
        else reqQ1 fi) .


  op parentG : ESet Qid -> Qid .
  ceq parentG(es,gname) = 
     (if pname == 'unknown
      then parentKG(es,qvalQidList(lookupd(getNotes(es,'gval,gname),   
                               "kbname",ql('unknown))))
      else pname fi) 
  if ql(pname) := 
       lookupd(getNotes(es,'gval,gname), "parent", ql('unknown)) .

**** if not a top-level (rules) kb, find its parent graph
**** pnet source -- graph of source
**** xnet source -- parentG( graph of source )
  op parentKG : ESet Qid -> Qid .
  ceq parentKG(es,kbname) =
       (if type == 'rules or type == 'pnet then gname else parentG(es,gname) fi)
  if ql(type pname toks) :=
       lookupd(getNotes(es,'tval, 'tkb kbname),"source",ql('unknown 'unknown))
  /\ ql(gname) := 
        (if type == 'rules 
         then ql(kbname)
         else lookupd(getNotes(es,'tval,type pname), "graph", ql('unknown))
         fi)  .
    

**** finds least common ancestor (name) of gname0 gname1
**** anc0 anc1 are the ancestors of gname0 gname1 found so far
****  top0, top1 indicate if the top (right) ancesctor is a kb
**** assumes last(anc0) is not in anc1 and vv
**** initial call is findLub(es,gname0,gname1, false,false)

  op findLub : ESet QidList QidList Bool Bool -> Qid .
  eq findLub(es, anc0, anc1, true,true) = 'unknown .
  ceq findLub(es, anc0, anc1 name1, true,false) = 
       (if gname == 'unknown
        then 'unknown
        else (if occurs(gname,anc0)
               then gname
               else findLub(es, anc0, anc1 name1 gname, true, isKB(es,gname)) 
               fi) fi)
  if gname := parentG(es,name1) .
     
  ceq findLub(es, anc0 name0, anc1, false, true) = 
       (if gname == 'unknown
        then 'unknown
        else (if occurs(gname,anc1)
               then gname
               else findLub(es, anc0 name0 gname, anc1, isKB(es,gname), true) 
               fi) fi) 
  if gname := parentG(es,name0) .

  ceq findLub(es, anc0 name0, anc1 name1, false,false) =
       (if gname0 == 'unknown or  gname1 == 'unknown
        then 'unknown
        else (if occurs(gname0,anc1 name1)
               then gname0
               else (if occurs(gname1, anc0 name0 gname0)
                     then gname1
                     else findLub(es, anc0 name0 gname0, anc1 name1 gname1, 
                                 isKB(es,gname0), isKB(es,gname1))
                     fi) fi) fi) 
  if gname0 := parentG(es,name0) 
  /\ gname1 := parentG(es,name1) .



****                  gname cgname new gname/pname
  op compareGraphs : ESet Qid Qid  Qid Qid -> BoolESet .
  op compareGraphs1 : ESet Qid Qid  Qid Qid Qid Graph Graph -> BoolESet .


  ceq compareGraphs(es,gname,cgname,newgname,newpname) =
    (if (graph0 == mtGraph or graph1 == mtGraph or pgname == 'unknown)
     then {false,es}
     else compareGraphs1(es,gname,cgname,newgname,newpname,pgname,graph0,graph1)
     fi)
  if gv(graph0) := getVal(es,'gval,gname,gv(mtGraph))
  /\ gv(graph1) := getVal(es,'gval,cgname,gv(mtGraph))
  /\ pgname := findLub(es,gname,cgname, false, false) .

**** stop if pgname is unknown or one of the graphs is empty

  ceq compareGraphs1(es,gname,cgname,newgname,newpname,pgname,graph0,graph1) =
    {res?? :: ResultPair,es'}
  if graph01 := joinGraphs(string(newgname),graph0,graph1)
  /\ title := "Comparing " +
         svalString(lookupd(getNotes(es,'gval,gname),"title", sv(string(gname))))
             + " and " +
         svalString(lookupd(getNotes(es,'gval,cgname),"title", sv(string(cgname))))
  /\ ql(kbname) := lookupd(getNotes(es,'gval,pgname),"kbname",ql('unknown))
   /\ gnotes :=
         (("source" := ql('xnet newpname)),
           ("gtype" := ql('cnet)),  
		       ("kbname" := ql(kbname)),
           ("requestor" := ql(gname)),
           ("requestop" := ql('compare)), 
           ("requestargs" := sv(string(cgname))), 
           (if isKB(es,pgname) then mt else ("parent" := ql(pgname)) fi),
           ("title" := sv(title)),
           ("subtitle" := sv("")),
           ("gatts" := ql('kbname 'source 
                          'requestor 'requestop 'requestargs)),
           ("oatts" := ql('compare)),
           ("ratts" := ql('compare 'pre 'post)),
           ("selections" := sv("false")),
****COLOR  ("colorFun" := sv("colorCNode")),
           ("colorFun" := sv("colorCnetNode")),
           ("toolBarFun" := sv("toolBarFunCnet"))
		     )
****  /\ tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,dumTv)
  /\ tm(modname0,t0) :=            **** the pnet for gname
        getVal(es,'tval, 
               qvalQidList(lookupd(getNotes(es,'gval,gname),
                           "source",ql('unknown 'unknown))),
               dumTv)
  /\ pntlT0 := (if getOp(t0) == 'pnet 
                then first(getArgs(t0)) 
                else t0 fi)
  /\ tm(modname1,t1) :=            **** the pnet for cgname
        getVal(es,'tval, 
               qvalQidList(lookupd(getNotes(es,'gval,cgname),
                           "source",ql('unknown 'unknown))),
               dumTv)
  /\ pntlT1 := (if getOp(t1) == 'pnet 
                then first(getArgs(t1)) 
                else t1 fi)
  /\ fail := modname0 == 'BOOL or modname1 == 'BOOL  or modname1 =/= modname0 
  /\ res?? := (if fail 
               then noParse(0)
               else metaReduce([modname0],'compareXnet[pntlT0,pntlT1]) fi)
  /\ xstateT := (if res?? :: ResultPair
                 then getTerm(res??)
                 else mtXstateT
                 fi)
  /\ xnotes := 
          (("source" :=
             lookupd(getNotes(es,'gval,pgname),"source",ql('unknown 'unknown))),    
           ("scopegraph" := ql(pgname)),   
           ("graph" := ql(newgname)),
           ("kbname" := ql(kbname)),
           ("history" := ql('`( 'compare gname cgname '`))),
           ("scopenet" := tm(modname0,xstateT2scopeT(xstateT))),
           ("hidden" := tm(modname0,xstateT2hiddenT(xstateT))), 
           ("newnet" := tm(modname0,xstateT2newnetT(xstateT))), 
           ("seen" := tm(modname0,xstateT2soccsT(xstateT))),
           ("oup" := tm(modname0,xstateT2uoccsT(xstateT))),
           ("odn" := tm(modname0,xstateT2doccsT(xstateT))),
           ("oboth" := tm(modname0,xstateT2boccsT(xstateT))) )
  /\ es' :=
     (if res?? :: ResultPair
      then addEntry(addEntry(es,
            'tval,'xnet newpname,xnotes,tm(modname0,xstateT2xnetT(xstateT))),
            'gval, newgname,gnotes,gv(graph01))
      else es 
      fi) .

**** the generic resets could go into pntl2graph

  ops resetNodeNotes resetONotes resetRNotes : Notes -> Notes .

  eq resetNodeNotes(notes) = 
       (if svalString(lookupd(notes,"type",sv(""))) == "occ"
        then resetONotes(notes)
        else resetRNotes(notes)
         fi) .

   eq resetONotes(notes) = 
        (("type" := sv("occ")),
         ("occ" := lookupd(notes,"occ", tm('BOOL,'true.Bool))),
         ("label" := lookupd(notes,"label", sv("???"))),
         ("loc" := lookupd(notes,"loc", sv("???"))),
         ("chattylabel" := lookupd(notes,"chattylabel", sv("???"))) ) .

   eq resetRNotes(notes) = 
        (("type" := sv("rule")),
         ("label" := lookupd(notes,"label", sv("???"))),
         ("chattylabel" := lookupd(notes,"chattylabel", sv("???"))),
         ("rule" := lookupd(notes,"rule", tm('BOOL,'true.Bool))),
         ("pre" := lookupd(notes,"pre", sv(""))),
         ("post" := lookupd(notes,"post", sv(""))) ) . 

  op resetNodeLNotes : NodeList NodeList -> NodeList .
  eq resetNodeLNotes(nil,ndl)  = ndl .
  eq resetNodeLNotes(nd(nid,notes) ndl, ndl') = 
         resetNodeLNotes(ndl,ndl' nd(nid,resetNodeNotes(notes))) .




****             left      right    joined
  op joinNodes : NodeList NodeList NodeList -> NodeList .
  op joinEdges : EdgeList EdgeList EdgeList  -> EdgeList .

  eq joinNodes(ndl,nil,ndl') = 
       setNNotes(resetNodeLNotes(ndl,nil),"compare",sv("left"),nil) ndl' .
  eq joinNodes(ndl0 nd(nid,notes) ndl1, nd(nid,notes') ndl', ndl'') = 
      joinNodes(ndl0 ndl1, ndl',
             ndl'' nd(nid,insert("compare",sv("both"),resetNodeNotes(notes)))) .
  eq joinNodes(ndl,nd(nid,notes) ndl',ndl'') = 
      joinNodes(ndl,ndl',
            ndl'' nd(nid,insert("compare",sv("right"),resetNodeNotes(notes))))
     [owise] .

**** should be careful with notes for edges (double edge compare bug lives here)
  eq joinEdges(edl', nil, edl) =  edl' edl .
  eq joinEdges(edl0 ed(src,tgt,notes) edl1, ed(src,tgt,notes') edl', edl) = 
      joinEdges(edl0 edl1,edl', edl ed(src,tgt,notes) ) .
  eq joinEdges(edl0, ed(src,tgt,notes) edl', edl) = 
      joinEdges(edl0, edl', edl ed(src,tgt,notes) ) [owise] .

  op joinGraphs : String Graph Graph -> Graph .
  eq joinGraphs(?string,graph0,graph1) = 
       graph(?string,mt,
             joinNodes(graphNodes(graph0), graphNodes(graph1),nil),
             joinEdges(graphEdges(graph0), graphEdges(graph1),nil) ) .


***************************************************************************
**** saving net as tkb
***************************************************************************
  eq isReq('net2KB) = true .
****                               from    viewer   user kbname       
  eq enabled(wait4s,req('net2KB,ql(gname  g2dvname ukbname toks),reqQ)) 
           = true .

 crl[net2KB]:
   [nil,
    st(processing(req('net2KB, ql(gname g2dvname ukbname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
    =>
   [nil,
    st(ready,wait4s,reqQ reqQ0,es,log),
    outQ]
  if reqQ2 := req('startListener, ql(ukbname 'graphreq g2dvname), 
                   req('defineKBGraph,ql(ukbname g2dvname),
                       reqQ'))
  /\ reqQ1 := 
       (if isXnetG(es,gname)
        then req('startcListener,ql(gname 'serializingListener g2dvname),reqQ2)
        else reqQ2 fi)
  /\ reqQ0 := req('net2tkb,ql(gname g2dvname ukbname),reqQ1)  .

***************************************************************************
  eq isReq('net2tkb) = true .
****                                 from          username          
  eq enabled(wait4s,req('net2tkb,ql(gname g2dvname  ukbname toks),reqQ)) 
           = true .

 crl[net2tkb]:
   [nil,
    st(processing(req('net2tkb, ql(gname g2dvname ukbname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,  wait4s, reqQ reqQ0, es',  log),
      outQ]
   if b0 := getVal(es,'tval,'tkb ukbname,dumTv) == dumTv **** check for existing kb
   /\ {b,es'} := (if b0
                  then net2tkb(es,gname,ukbname)
                  else {false,es}
                  fi)
   /\ reqQ0 := 
        (if b0 and b
         then reqQ'
         else (if not(b0)
               then req('sendAlert,
                         ql(g2dvname 'net2KB 'Failure 
                                    gname ukbname 'exists), nil)
               else req('logreq,ql('net2KB gname ukbname 'failed), nil)
               fi) fi)  .

  op net2tkb : ESet Qid Qid -> BoolESet .
  ceq net2tkb(es,gname,ukbname) = {b,es'}
  if ql(type pname) := **** type should be 'xnet or 'pnet
       lookupd(getNotes(es,'gval,gname),"source",ql('unknown 'unknown))
  /\ tm(modname,t1) := getVal(es,'tval,type pname,dumTv)
  /\ pntlT := (if getOp(t1) == 'pnet 
                then first(getArgs(t1)) 
                else t1 fi)
  /\ gv(?graph) := getVal(es,'gval, gname,gv(mtGraph))
  /\ opnotes := getNotes(es,'tval,type pname)
  /\ pnotes :=  (("source" := ql(type pname)), 
                 ("graph" := ql(ukbname)),
    ****         ("parent" := lookupd(opnotes,"source",ql('unknown 'unknown))),
                 (if isXnetG(es,gname) 
                  then ("history" := lookupd(opnotes,"history",ql(nil)))
                  else mt fi)
                 )
  /\ gnotes :=  (("source" := ql('tkb ukbname)),("kbname" := ql(ukbname)))
  /\ ?graph' := graph(string(ukbname),mt,graphNodes(?graph),graphEdges(?graph))
  /\ b := (type == 'xnet or type == 'pnet)
            and ?graph =/= mtGraph and modname =/= 'BOOL
  /\ es' := 
      (if b
       then addEntry(addEntry(es,
              'tval,'tkb ukbname, pnotes, tm(modname,pntlT)),
              'gval,ukbname, gnotes, gv(?graph'))
       else es fi) .


endm 


