******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-INFOX is
  inc PLA-INFO .
  inc GRAPH-INFO .
  inc SPLIT-PAREN .

***  inc PNTL2GRAPH .
***  inc GRAPH2G2D .
***  inc GRAPH2LOLA .

******************************************************************************
*** 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 toks toks' htoks outQ qidl : QidList .
vars gname mname kbname clab modname g2dvname dgname qid : Qid .
vars funName ptype pname : Qid .
vars gnotes pnotes notes : Notes .
var b : Bool .
vars nodes nodes' : NodeList .
var occT : Term .
vars str ?string : String .
var fres : FindResult .
var ispec : Sexp .

******************************************************************************
**** Component Info
******************************************************************************
  op displayComponentInfo : ESet Qid Qid QidList -> String .
  ceq displayComponentInfo(es,gname,clab,toks) = 
      (if modname == 'BOOL 
**** 09nov08
****   or tl:TermList == empty
       or not(tl:TermList :: Term)
       then "(apply displayMessage \"Component Info Error\"  \"No Info for "
               + string(clab) + "\")" 
****       else mkComponentInfoExp(dgname,modname,tl:TermList)
       else mkComponentInfoExpX(ispec,gname,modname,clab,tl:TermList)
       fi) 
    if dgname := getNth(0,toks,gname)
    /\ nodes := graphNodes(gvalGraph(getVal(es,'gval,gname,gv(mtGraph))))
    /\ nodes' := getNode(nodes,"chattylabel",sv(string(clab)))
    /\ tm(modname,occT) :=
        (if nodes' :: Node
         then lookupd(nodeNotes(nodes'),"occ",dumTv)
         else dumTv
         fi)
    /\ tl:TermList := (if modname == 'BOOL then empty else occT2thT(occT) fi)
    /\ sxv(ispec) := getVal(es,'sxval,'ComponentInfoSpec,sxv([nil]))
   .

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


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

******************************************************************************
******************************************************************************
  op displayRuleEvidence : ESet Qid Qid QidList -> String .
  ceq displayRuleEvidence(es,gname,clab,toks) = 
      (if toks == 'unknown 
       then "(apply displayMessage \"Rule Evidence Error\"  \"No rule "
               + string(clab) + "\")" 
       else mkRuleEvidenceExp(dgname,clab,toks')
       fi) 
    if ql(kbname) := lookupd(getNotes(es,'gval,gname),"kbname",ql('unknown))
    /\ ql(toks') :=
           lookupd(getNotes(es,'qval,kbname),pnRid2RidStr(clab),ql('unknown))
    /\ dgname := getNth(0,toks,gname) .

  op pnRid2RidStr : Qid -> String .
  ceq pnRid2RidStr(clab) = 
          (if fres :: Nat then substr(str,0,fres) else str fi)  
    if  str := string(clab)
    /\ fres := rfind(str, PNRidSuffix, length(str)) .


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


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

*****************************************************************************
**** printing history 
*****************************************************************************
eq isReq('printHistory) = true .
eq enabled(wait4s,req('printHistory,ql(gname g2dvname funName toks),reqQ))
      = not(waiting4(wait4s,g2dvname))  .


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

op history2string : QidList String -> String .  
op printHistory : ESet Qid Qid -> String .  

ceq history2string(htoks,str) =
  (if b
   then history2string(toks',
                       str + " ( " + removeBQs(qidl2str(toks),0,"")  +  " )\n")
   else str                       
  fi)
if {b,'`( toks '`), toks'} := splitParen(htoks) .

eq history2string(htoks,str) = str [owise] .

ceq printHistory(es,gname,funName) =
   "(apply " + string(funName) + " "  + squote(string(gname)) + " " 
   + squote(history2string(htoks,"")) + ")"
if gnotes := getNotes(es,'gval,gname) 
**** 'xnet xname
/\ ql(ptype pname) := lookupd(gnotes,"source", ql('unknown 'unknown))
/\ pnotes := getNotes(es,'tval, ptype pname)
/\ ql(htoks) := lookupd(pnotes,"history", ql(nil)) 
.

******************************************************************************
**** displayUnreachable
**** desplays a list of unreachable rule ids
**** (displayUnreachable RKB graphics2d)
******************************************************************************
  eq isReq('displayUnreachable) = true .
  eq enabled(wait4s, req('displayUnreachable,ql(kbname g2dvname  toks),reqQ)) 
       = true .

crl[displayUnreachable]:
   [nil,
    st(processing(req('displayUnreachable, ql(kbname g2dvname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ', es, log),
  outQ
   g2dvname '\n mname '\n str2toks(?string)  maudePrompt
  ] 
  if notes := getNotes(es,'tval,'tkb kbname)
  /\ ql(qidl) := lookupd(notes,"unreachable",ql(nil))
  /\ mname :=  getMaudeName(es)
  /\ str := (if qidl == nil 
             then "No unreachable rules!" 
             else printLnQidL(qidl,"") fi)
  /\ ?string :=  withAck(fillTemplate(displayInfoTemplate,
                   (("%title" :~ squote("Unreachable rules in " + string(kbname))),
                    ("%message" :~ squote(str))) ),
                   mname,g2dvname)    .
   

  op displayInfoTemplate : -> String .
  eq displayInfoTemplate = 
      "(apply displayInfoMessage %title %message)" .


  op printLnQidL : QidList String -> String .
  eq printLnQidL(nil,str) = str .
  eq printLnQidL((qid qidl),str) = 
      printLnQidL(qidl, str + "\n" + string(qid)) .


******************************************************************************
**** displayDuplicateRuleIds
**** desplays a list of rule ids that are duplicated
**** (displayDuplicateRuleIds graphics2d)
**** modname QQQ is hardwired
******************************************************************************
  eq isReq('displayDuplicateRuleIds) = true .
  eq enabled(wait4s, req('displayDuplicateRuleIds,ql(g2dvname  toks),reqQ)) 
       = true .

crl[displayDuplicateRuleIds]:
   [nil,
    st(processing(req('displayDuplicateRuleIds, ql(g2dvname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ', es, log),
  outQ
   g2dvname '\n mname '\n str2toks(?string)  maudePrompt
  ] 
  if qidl := duplicateIds(getRls(upModule('QQQ,true)),nil,nil)
  /\ mname :=  getMaudeName(es)
  /\ str := (if qidl == nil 
             then "No duplicate rule ids!" 
             else printLnQidL(qidl,"") fi)
  /\ ?string :=  withAck(fillTemplate(displayInfoTemplate,
                   (("%title" :~ squote("Duplicate Rule Ids")),
                    ("%message" :~ squote(str))) ),
                   mname,g2dvname)    .
   
vars seen dups : QidList .
var rule : Rule .
var rules : RuleSet .
var rid : Qid .

op duplicateIds : RuleSet QidList QidList -> QidList .
eq duplicateIds(none,seen,dups)  = dups .
ceq duplicateIds(rule rules,seen,dups)  = 
    (if occurs(rid,seen)
     then duplicateIds(rules,seen, dups rid)
     else duplicateIds(rules,seen rid, dups)
     fi)  
  if rid := getRuleId(rule) .


endm

