******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-INFO is
  inc RFE .
  inc PLA-AUX .
  inc STATUS-AUX .

  inc META-PETRI .
  inc PL-PRINT .

******************************************************************************
*** 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 .

var b : Bool .
var n nodeId cur : Nat .
var fres : FindResult .
vars maudename mname g2dname g2dvname kbname modname modname' : Qid .
vars type tkbFname occsFname graphFname nid flag qid clab : Qid .
vars gname pname newgname newpname pathpname dname dgname : Qid .
vars outQ toks toks' rids srctoks : QidList .
var ?graph : Graph .
vars pntlT pntlT' pnetT occsT ioccsT ioccsT' uoccsT roccsT nT occT : Term .
vars goccsT aoccsT ridsT ugoccsT : Term .
var tl occTL : TermList .
var mod : Module .
vars dnotes gnotes pnotes notes : Notes .
vars res0?? res1?? res?? res2?? res3?? : [ResultPair?] .
vars id ?string status str gstr astr rstr title subtitle : String .

vars ndl ndl' nds nodes pndl : NodeList .
var edl : EdgeList .
var rules : RuleSet .
var rule : Rule .
 
******************************************************************************
 op display2GTemplate : -> String .
  eq display2GTemplate = 
      "(apply displayMessage2G %gname %title %message)" .

  op displayTemplate : -> String .
  eq displayTemplate = 
      "(apply displayMessage %title %message)" .

******************************************************************************
**** display unused 
******************************************************************************

  eq isReq('displayUnused) = true .
  eq enabled(wait4s,req('displayUnused,ql(gname g2dvname toks),reqQ)) = 
      not(waiting4(wait4s,g2dvname))  .

 rl[displayUnused]:
   [nil,
    st(processing(req('displayUnused, ql(gname g2dvname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, 
       (wait4s ! wait4(g2dvname,gname,nil)), 
       (reqQ reqQ'),
       es, 
       log), 
    outQ
     displayUnusedToks(es,gname,g2dvname,toks)  ]  .

  op displayUnusedToks : ESet Qid Qid QidList -> QidList .
  ceq displayUnusedToks(es,gname,g2dvname,toks) = 
          g2dvname '\n mname '\n str2toks(?string)  maudePrompt
    if  gnotes := getNotes(es,'gval, gname) 
    /\ ql(srctoks) := lookupd(gnotes,"source",ql(nil))
    /\ pnotes := getNotes(es,'tval,srctoks)
    /\ tm(modname,occsT) := lookupd(pnotes,"unusedOccs", dumTv)
    /\ mname :=  getMaudeName(es)
    /\ dgname := getNth(0,toks,gname)
    /\ ?string := 
         (if modname == 'BOOL
          then ""
          else withAck(fillTemplate(display2GTemplate,
                   (("%gname" :~ squote(string(dgname))),
                     ("%title" :~ squote("Unused in " + string(gname))),
                     ("%message" :~ 
                      squote(printLnOccTL([modname],
                                          occsT2occTL(occsT))))) ),
                   mname,g2dvname)
          fi) 
    .
   

  op printLnOccTL : Module TermList -> String .
  eq printLnOccTL(mod,empty) = "" .
  eq printLnOccTL(mod,(occT, occTL)) = 
      occ2label(mod,occT) + "\n" + printLnOccTL(mod,occTL)
     .
     

******************************************************************************
  op display2GMaudeRule : ESet Qid Qid QidList -> String .
  ceq display2GMaudeRule(es,gname,clab,toks) = 
         fillTemplate(display2GTemplate,
              (("%gname" :~ squote(string(dgname))),
                ("%title" :~ squote(title)),
                ("%message" :~ squote(?string))))
    if dgname := getNth(0,toks,gname)
    /\ gnotes := getNotes(es,'gval,gname)
    /\ ql(kbname) := lookupd(gnotes,"kbname",ql(nil))
    /\ tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,dumTv)
    /\ str := string(clab)
    /\ rules :=   getRule(upRls(modname,true), pnRidStr2Rid(str)) 
    /\ title := "Maude rule " +
                 (if rules :: Rule then string(getRuleId(rules)) else "" fi)
    /\ ?string := 
     (if rules :: Rule then rule2string([modname], rules) else "not found" fi) .

  op pnRidStr2Rid : String -> Qid .
  ceq pnRidStr2Rid(str) = 
          qid(if fres :: Nat then substr(str,0,fres) else str fi)  
    if  fres := rfind(str, PNRidSuffix, length(str)) .


  op rule2string : Module Rule -> String .
  eq rule2string(mod,rule) = 
    "\n rl[" + string(getRuleId(rule)) + "]: \n  "
       + removeBQs(qidl2str(metaPrettyPrint(mod,getLhs(rule),mixfix flat)),0,"")
       + "\n => \n  "
       + removeBQs(qidl2str(metaPrettyPrint(mod,getRhs(rule),mixfix flat)),0,"")
       + " . \n"
    .

  eq isReq('display-maude-rule) = true .
  eq enabled(wait4s,req('display-maude-rule,ql(gname g2dvname clab toks),reqQ))
      = not(waiting4(wait4s,g2dvname))  .


crl[display-maude-rule]:
   [nil,
    st(processing(req('display-maude-rule, ql(gname g2dvname clab toks), 
                      reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,
      (wait4s ! wait4(g2dvname, nil, 
                      req('logreq,ql('display-maude-rule gname clab),reqQ'))),
       reqQ, 
       es,
       log), outQ 
     g2dvname '\n mname '\n toks' maudePrompt ]
    if  mname :=  getMaudeName(es)
    /\ ?string :=
          withAck(display2GMaudeRule(es,gname,clab,toks), mname, g2dvname) 
    /\  toks' := str2toks(?string) 
    .

endm


