******************************************************************************
*** PLA based on IMaude 
*** defines initialization requests 
*** assembles remaining request modules
******************************************************************************
mod INTERACTIVE-PLA is

  inc PLA-KB .
  inc PLA-DISH .
  inc PLA-GRAPH .

****  inc PLA-EXPLORE .
  inc PLA-COMPARE .
****  inc PLA-INFO .
  inc PLA-INFOX .
  inc PLA-EXPORT .
***  inc PLA-IMPORT .








******************************************************************************
*** 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 n : Nat .
vars maudename g2dname g2dvname kbname modname restore? save? : Qid .
vars name reqid type tok mname gname dname  : Qid .
vars outQ toks toks' dnames : QidList .
var ?graph : Graph .
vars pntlT occsT : Term .
vars res0?? res1?? res?? : [ResultPair?] .
vars title msg ?string : String .


******************************************************************************
**** initializing the PLA environment
***** initPLAeset
****   initializes maudeName, g2dName, g2dVname globalCounter
******************************************************************************
 
op initPLAeset : ESet Qid Qid Qid -> ESet .
eq initPLAeset(es,maudename,g2dname,g2dvname) =
    addEntry(
     addEntry(
      addEntry(
       addEntry(
        addEntry(
         addEntry(es, 
                'qval, 'maudeName, ql(maudename)), 
                'qval, 'g2dName, ql(g2dname)), 
                'qval, 'g2dVName, ql(g2dvname)),
                'sval, 'globalCounter, sv("0")),
                'qval, 'knownDishes, ql(nil)),
                'qval, 'knownKBs, ql(nil)) .

eq isReq('initPLAeset) = true .
eq enabled(wait4s,
          req('initPLAeset, ql(maudename g2dname g2dvname toks),reqQ)) = true .

rl[initPLAeset]:
   [nil, 
    st(processing(req('initPLAeset, ql(maudename g2dname g2dvname toks),
                      reqQ')),
     wait4s,reqQ,es,log),
     outQ]
   =>
   [nil, 
    st(ready, wait4s, (reqQ reqQ'),
       initPLAeset(es,maudename,g2dname,g2dvname),log), 
    outQ] .

******************************************************************************
**** initialize KBmanager
**** invoke initKBmanager in viewer
******************************************************************************
  eq isReq('initKBManager) = true .
  eq enabled(wait4s,req('initKBManager,ql(g2dvname toks),reqQ)) = 
      not(waiting4(wait4s,g2dvname)) .

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

****   /\ ?string := withAck("(apply defKBManager)", mname,g2dvname) 

******************************************************************************
**** initialize KBmanager with predef dishes
**** invoke initKBmanager in viewer
******************************************************************************
  eq isReq('initKBManagerD) = true .
  eq enabled(wait4s,req('initKBManagerD,ql(g2dvname modname toks),reqQ)) = 
      not(waiting4(wait4s,g2dvname)) .

  crl[initKBManagerD]:
   [nil,
    st(processing(req('initKBManagerD, ql(g2dvname modname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,
       (wait4s !
        wait4(g2dvname,nil,
              req('logreq, 
                   ql('initKBManagerD g2dvname modname toks),reqQ'))), 
       reqQ,
       es,
       log), outQ 
     g2dvname '\n mname '\n toks' maudePrompt ]
   if mname :=  getMaudeName(es)
   /\ dnames :=   constListBySortX(upOpDecls(modname,true),
                                   (lesserSorts([modname],'Dish) ; 'Dish )) 
   /\ ?string :=
        "(apply defKBManagerD " 
       + fillTemplate(stringArrayTemplate, ("%strings" :~ qidl2squotes(dnames)))
       + ")" 
   /\ toks' := str2toks(?string) .

****15nov14 clt remove redundant sending of OK, defKBManager does that
****   before putting up the progress bar
***(
   /\ ?string :=
        withAck("(apply defKBManagerD " 
       + fillTemplate(stringArrayTemplate, ("%strings" :~ qidl2squotes(dnames)))
       + ")", mname,g2dvname) 
)
***(
******************************************************************************
*** initPLAReq 
***   initializes eset 
***   initializes kb -- net and graph
***     if restore? == 'true get from file   ow construct from modname     
***     if save? == 'true save the initialized net and kbgraph
****       (toks is optional filename prefix override)
****    tells g2dvname about graph nodes 
****    initializes g2dvname dishmanager
****    starts KB listener

*** if restore specified and fails should it try from scratch?
*** toks could specify non-default names for file prefixes
******************************************************************************
  eq isReq('initPLAreq) = true .
  eq enabled(wait4s,req('initPLAreq,
            ql(maudename g2dname g2dvname kbname modname restore? save? toks),
            reqQ)) = true .

crl[initPLAreq]:
   [nil, 
    st(processing(req('initPLAreq, 
         ql(maudename g2dname g2dvname kbname modname restore? save? toks),
         reqQ')),
     wait4s,reqQ,es,log),
     outQ]
   =>
   [nil, 
    st(processing(reqQ0), wait4s,reqQ,es,log), 
    outQ]
  if reqQ2 := (if save? == 'true 
               then req('saveKB, ql(kbname toks),reqQ') 
               else reqQ' fi)
    /\ reqQ1 :=  req('defineKBGraph, ql(kbname  g2dvname),
                   req('initDishes,ql(kbname g2dvname modname), 
                     req('startcListener,
                         ql(kbname 'restartingListener g2dvname), reqQ2)))
    /\ reqQ0 :=
         req('initPLAeset, ql(maudename g2dname g2dvname),
              (if restore? == 'true
               then req('restoreKB, ql(kbname toks), reqQ1)
               else req('initKB, ql(kbname modname),reqQ1)
               fi) ) . 
)
******************************************************************************
**** (initDishes kbname  g2dvname modname)
**** tell viewer the names of predefined dishes
******************************************************************************
  eq isReq('initDishes) = true .
  eq enabled(wait4s,req('initDishes,ql(modname toks),reqQ)) = true .

  rl[initDishes]:
   [nil,
    st(processing(req('initDishes, ql(modname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil, st(ready, wait4s, reqQ reqQ', initDishes(es,modname), log), outQ ] .

  op initDishes : ESet Qid -> ESet  .
  ceq initDishes(es,modname) = es'
   if dnames :=   constListBySortX(upOpDecls(modname,true),
                                   (lesserSorts([modname],'Dish) ; 'Dish )) 
   /\ es' := addPreDefDishes(es,
                      qvalQidList(getVal(es,'qval,'knownDishes,ql(nil))), 
                      dnames) .

  op addPreDefDishes : ESet QidList QidList -> ESet .
  eq addPreDefDishes(es,toks',nil) = 
       addEntry(es,'qval,'knownDishes,ql(toks')) .
  eq addPreDefDishes(es,toks', dname toks) = 
        addPreDefDishes(es,toks' dname dname, toks) . 


******************************************************************************
***** sendAlert
******************************************************************************
  eq isReq('sendAlert) = true .
  eq enabled(wait4s,req('sendAlert,ql(g2dvname type toks),reqQ)) = 
      not(waiting4(wait4s,g2dvname)) .

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


  op sendAlertTemplate : -> String .
**** 09Oct10 stop progressd dialog if running
  eq sendAlertTemplate =
   "(seq  (apply closeProgressd) (apply displayMessage %title %msg))" .
  op mksendAlertExp : String String -> String .
  eq mksendAlertExp(title,msg) =
      fillTemplate(sendAlertTemplate, 
                   (("%title" :~ squote(title)),("%msg" :~ squote(msg)))) .

******************************************************************************
****  Debugging
******************************************************************************
***(  
var n : Nat .
vars maudename g2dname g2dvname kbname modname restore? save? : Qid .
vars name reqid type tok mname gname dname  : Qid .
vars outQ toks toks' dnames : QidList .
var ?graph : Graph .
vars pntlT occsT : Term .
vars res0?? res1?? res?? : [ResultPair?] .
vars title msg ?string : String .
)

   var t : Term .
   var val : Val .
   vars pname rid iob ix tag etype : Qid .
   vars pntTL tl occTL : TermList .
   var notes : Notes .
   var nodes : NodeList .

	op term2str : Term -> String .
	op termlist2str : NeTermList -> String .
	eq term2str(v:Variable) = string(v:Variable) .
	eq term2str(c:Constant) = string(c:Constant) .
	eq term2str(op:Qid[tl:NeTermList]) = 
	               string(op:Qid) + "[" + termlist2str(tl:NeTermList) + "]"  .
	eq termlist2str(t) = term2str(t) .
	eq termlist2str((t,tl:NeTermList)) =
	         term2str(t) + "," + termlist2str(tl:NeTermList)  .

	op val2str : Val -> String .
	eq val2str(dummy) = "dummy" .
	eq val2str(ql(toks)) = "QVal: " + qidl2str(toks) .
	eq val2str(sv(?string)) = "SVal: " + ?string .
	eq val2str(tm(modname,t)) = "TVal[" + string(modname) + "]: " + term2str(t) .
	eq val2str(val) = "???" [owise] .


	op pocc2str : ESet Qid Qid Qid Qid Qid -> String .
	ceq pocc2str(es,type,pname,rid,iob,ix) =
	   (if occTL :: Term then term2str(occTL) else "none.Occs" fi)
	if tm(modname,t) := getVal(es,'tval, type pname, dumTv)
	/\ pntTL := 
	      pntlT2pntTL(if modname == 'BOOL
	                  then 'nil.PNTransList
	                  else (if type == 'tkb or type == 'xnet
	                        then t
	                        else pnT2pntlT(t) fi)
	                   fi)
	/\ tl :=  metaGetTrans(pntTL,mkQidConst(rid))
	/\ n := (if rat(string(ix),10) :: Nat
	         then rat(string(ix),10) 
	         else 0
	         fi)
	/\ occTL := (if tl :: Term
	             then  (if iob == 'i
	                    then occsT2occTL(pntT2ioccsT(tl))
	                    else (if iob == 'o
	                    then occsT2occTL(pntT2ooccsT(tl))
	                    else occsT2occTL(pntT2boccsT(tl)) fi) fi)
	             else empty fi)  .


	op note2str : ESet Qid Qid QidList -> String .
	eq note2str(es,etype,tag,toks) =
        (if etype == 'tval
         then val2str(lookupd(getNotes(es,etype,toks),string(tag),dummy)) 
         else (if etype == 'gval 
               then gnote2str(es,etype,tag,toks)
               else "???"
               fi)
         fi)  .

	op gnote2str : ESet Qid Qid QidList -> String .
	ceq gnote2str(es,etype,tag,gname ix toks) =
         val2str(lookupd(notes,string(tag),dummy))
   if gv(?graph) := getVal(es,'gval,gname,gv(mtGraph))
	/\ n := (if rat(string(ix),10) :: Nat
	         then rat(string(ix),10) 
	         else 0
	         fi)
   /\ nodes := getNode(?graph,n) 
   /\ notes := (if nodes :: Node
                then nodeNotes(nodes)
                else mt fi)  .

	eq gnote2str(es,etype,tag,toks) = "???" [owise] .

**** (pocc2str type pname rid iob ix)

  eq isReq('pocc2str) = true .
  eq enabled(wait4s,req('pocc2str,ql(type pname rid iob ix toks),reqQ)) = true .

 
  rl[pocc2str]:
   [nil,
    st(processing(req('pocc2str, ql(type pname rid iob ix toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ, es,
       log), outQ 
     'user '\n getMaudeName(es) '\n 
          qid(pocc2str(es,type,pname,rid,iob,ix)) maudePrompt ]  .

**** (note2str etype tag ids)

  eq isReq('note2str) = true .
  eq enabled(wait4s,req('note2str,ql(etype tag toks),reqQ)) = true .

  rl[note2str]:
   [nil,
    st(processing(req('note2str, ql(etype tag toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ, es,
       log), outQ 
     'user '\n getMaudeName(es) '\n 
          qid(note2str(es,etype,tag,toks)) maudePrompt ]  .

endm

*** loop init .

