fmod PLA-AUX is
  inc IDATA .

**** additional Val subsorts
  inc GVAL-IO .
  inc MVAL-IO .     
  inc SXVAL-IO .     

  inc PL-PRINT .  *** for printing titles
  inc META-PETRI .
****  inc SEXP .

  var es : ESet .
  var n : Nat .
  vars s gstr astr rstr : String .
  vars pntlT occsT t uoccsT goccsT aoccsT ridsT : Term .
  vars gname pname qid type modname name kbname xname dname user-dname  : Qid .
  var pnotes gnotes notes : Notes .
  var b : Bool .
  var sexpl : SexpL .
  var toks : QidList .


    
******************************************************************************
***** for conditional ESet functions

  sort BoolESet .
  op `{_,_`} : Bool ESet -> BoolESet [ctor] .
  op be2b : BoolESet -> Bool .
  op be2e : BoolESet -> ESet .
  eq be2b({b,es}) = b .
  eq be2e({b,es}) = es .

**** gensym hack for generating new ids 

  op getGlobalCounter : ESet -> String .
  op incGlobalCounter : ESet -> ESet .
  op incGlobalCounter : ESet Nat -> ESet .

  eq getGlobalCounter(es) = 
          svalString(getVal(es,'sval,'globalCounter,sv("0"))) .
  eq incGlobalCounter(es) = incGlobalCounter(es,1) .
  eq incGlobalCounter(es,n) = 
       addEntry(es,'sval,'globalCounter,
                sv(string(rat(getGlobalCounter(es),10) + n,10))) .


  op stringInc : String -> String .
  eq stringInc(s) = 
      (if string(rat(s,10) + 1, 10) :: String
       then string(rat(s,10) + 1, 10) 
       else s fi) .

**** sort refinement for added Val sorts 
  op getVal : ESet Qid QidList GVal -> GVal .
  op getVal : ESet Qid QidList MVal -> MVal .

  op getGraphKBname : ESet Qid Qid -> Qid .
  eq getGraphKBname(es,gname,qid) =
       getNth(0,
              qvalQidList(lookupd(getNotes(es,'gval,gname),"kbname",ql(qid))), 
              qid) .

  op isXnetG : ESet Qid -> Bool .
  eq isXnetG(es,gname) =
        getNth(0,
               qvalQidList(lookupd(getNotes(es,'gval,gname),
                                           "source",ql('unknown 'unknown))),
               'unknown) == 'xnet .


  op isKB : ESet Qid -> Bool .
  eq isKB(es,gname) =
       'tkb == getNth(0, 
                      qvalQidList(lookupd(getNotes(es,'gval,gname),
                                          "source",
                                           ql('unknown 'unknown))),
                      'unknown) . 

 

  ops traceGraph tracePNet traceXNet : ESet Qid -> Sexp .
  ceq traceGraph(es,gname) = [a("graph") a(string(gname)) sexpl]
  if gnotes := getNotes(es,'gval,gname)
  /\ ql(type pname) := lookupd(gnotes,"source",ql('unknown 'unknown)) 
  /\ [sexpl] :=  traceNet(es,type,pname) .

  op traceNet : ESet Qid Qid -> Sexp .
  eq traceNet(es,'pnet,pname) = tracePNet(es,pname) .
  eq traceNet(es,'xnet,pname) = traceXNet(es,pname) .
  eq traceNet(es,type,pname) = [nil]  [owise] .
  
  ceq tracePNet(es,pname) = [a(string(type)) a(string(pname)) sexpl]
  if pnotes := getNotes(es,'tval,'pnet pname)
  /\ ql(type name) := lookupd(pnotes,"source",ql('unknown 'unknown)) 
  /\ sexpl := (if type == 'dishnet
               then dishnetTrace(pnotes,name)
               else queryTrace(pnotes,name)
                fi) .

  ops dishnetTrace queryTrace : Notes  Qid -> SexpL .
  ceq dishnetTrace(notes,dname)  = 
      ( [a("kbname") a(string(kbname)) ]
        [a("initialState") a(string(user-dname)) ] )
  if ql(name user-dname) := lookupd(notes,"dishname",ql('unknown 'unknown) )
  /\ ql(kbname) := lookupd(notes,"kbhname",ql('unknown) ) .

  ceq queryTrace(notes,name) =
     ( [a("parent") a(string(name)) ]
       [a("kbname") a(string(kbname))]       
       [a("initialState") a(string(user-dname))]
       [a("goalOccs") a(gstr)]
       [a("avoidOccs") a(astr)]
       [a("hiddenRules") a(rstr)] )
  if ql(dname user-dname) := lookupd(notes,"dishname",ql('unknown 'unknown) )
  /\ ql(kbname) := lookupd(notes,"kbhname",ql('unknown) ) 
  /\ tm(modname,goccsT) := lookupd(notes,"gOccs",tm('UNKNOWN,'none.Occs))
  /\ tm(modname,aoccsT) := lookupd(notes,"aOccs",tm('UNKNOWN,'none.Occs))
  /\ tm(modname,ridsT) := lookupd(notes,"aRules",tm('UNKNOWN,'nil.QidList)) 
  /\ gstr := printOccTL([modname],occsT2occTL(goccsT))
  /\ astr := printOccTL([modname],occsT2occTL(aoccsT))
  /\ rstr := printRidTL(qidlT2tl([modname],ridsT)) .

  ceq traceXNet(es,xname) =
     [a("xnet") a(string(xname)) 
       [a("scope") a(string(type)) a(string(name))]
       [a("kbname") a(string(kbname))]
       [a("history") history2sexp(toks)] ]
  if notes := getNotes(es,'tval,'xnet xname)
  /\ ql(type name) := lookupd(notes,"source",ql('unknown 'unknown))
  /\ ql(gname) := lookupd(notes,"graph",ql('unknown)) 
  /\ ql(kbname) := lookupd(getNotes(es,'gval,gname),"kbname",ql('unknown)) 
  /\ ql(toks) :=  lookupd(notes,"history", ql(nil)) .

  op traceTkb : ESet Qid -> Sexp .
  ceq traceTkb(es,kbname) = 
       [a("tkb") a(string(kbname)) a(string(type)) a(string(name))]
  if notes := getNotes(es,'tval,'tkb kbname)
  /\ ql(type name) := lookupd(notes,"source",ql('unknown 'unknown)) .

  op history2sexp : QidList -> Sexp .
  eq history2sexp(toks) = [a("history")] .   ***** hack

**** shared by pla-graph and pla-explore

  op mkGraphTitle : Qid Notes -> String .
  op mkGraphSubTitle : Notes -> String .

  ceq mkGraphTitle(pname,pnotes) =
         "Graph for " + string(type) + " " + string(pname) 
      if ql(type qid) := lookupd(pnotes,"source",ql('unknown 'unknown)) .

****  eq mkGraphTitle('pathnet,gname) = "Graph for path in "  + string(gname) .

**** 09aug02 clt to display in SEpanel
  ceq mkGraphSubTitle(pnotes) =
****    (if gstr == "" then "" else "\t Goals: " + gstr + "\n" fi)
    (if gstr == "" then "" else " Goals: " + gstr + "\n" fi)
    +
****    (if astr == "" then "" else "\t OccAvoids: " + astr + "\n" fi)
    (if astr == "" then "" else " OccAvoids: " + astr + "\n" fi)
    +
****    (if rstr == "" then "" else "\t RuleAvoids: " + rstr + "\n" fi)
    (if rstr == "" then "" else " RuleAvoids: " + rstr + "\n" fi)
  if tm(modname,goccsT) := lookupd(pnotes,"gOccs",tm('BOOL,'true.Bool)) 
  /\ tm(modname,aoccsT) := lookupd(pnotes,"aOccs",tm('BOOL,'true.Bool)) 
  /\ tm(modname,ridsT) := lookupd(pnotes,"aRules",tm('BOOL,'true.Bool)) 
  /\ gstr := printOccTL([modname],occsT2occTL(goccsT))
  /\ astr := printOccTL([modname],occsT2occTL(aoccsT))
  /\ rstr := printRidTL(qidlT2tl([modname],ridsT)) .

**** gname to be added at graph defn time
  op mkPGraphTitle : Qid Notes -> String .
  ceq mkPGraphTitle(gname,pnotes) =
       mkPGraphTitle(gname,type,user-dname)
    if ql(type name) := lookupd(pnotes,"source",ql('unknown 'unknown)) 
    /\ ql(dname user-dname) := lookupd(pnotes,"dishname",ql('unknown 'unknown)) .

  op mkPGraphTitle : Qid Qid Qid -> String .
  eq mkPGraphTitle(gname,'dishnet,dname) = "InitialNet for " + string(dname) .
  eq mkPGraphTitle(gname,'subnet,dname) =  "Subnet of " + string(dname) .
  eq mkPGraphTitle(gname,'pathnet,dname) = "Pathnet in " + string(dname) .

**** gname to be added at graph defn time
  op mkXGraphTitle : Qid Qid Qid -> String .
  eq mkXGraphTitle(gname,'tkb,kbname) = "Exploring in KB " + string(kbname) .
  eq mkXGraphTitle(gname,'pnet,dname) =
          "Exploring in InitialNet " + string(dname) .

  op mkQueryGNotes : Notes -> Notes .
  ceq mkQueryGNotes(pnotes) =
       (("gOccs" := sv(printOccTL([modname],occsT2occTL(goccsT)))),
        ("aOccs" := sv(printOccTL([modname],occsT2occTL(aoccsT)))),
        ("aRules" := sv(printRidTL(qidlT2tl([modname],ridsT)))),
        ("unRchGoals" := sv(printOccTL([modname],occsT2occTL(uoccsT))))
       )
  if tm(modname,goccsT) := lookupd(pnotes,"gOccs",tm('BOOL,'true.Bool)) 
  /\ tm(modname,aoccsT) := lookupd(pnotes,"aOccs",tm('BOOL,'true.Bool)) 
  /\ tm(modname,ridsT) := lookupd(pnotes,"aRules",tm('BOOL,'true.Bool)) 
  /\ tm(modname,uoccsT) := lookupd(pnotes,"unRchGoals",tm(modname,'none.Occs)) .

endfm

***(
pnet graph title:  
 Initial Net Graph gname  for user-dname
 Subnet Graph gname for user-dname

Pnet Graph info
    goals avoids hides -- strings -- if non-empty
    source string "pnet foo"
    
XNet Graph info
   source "tkb bar", "pnet foo"

info cmd -- show history


)
