******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-DISH is

  inc RFE .
  inc PLA-AUX .
  inc META-PETRI .
  inc NEW-GRAPH2G2D .

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

var n : Nat . var b : Bool .
vars maudename mname g2dname g2dvname kbname modname restore? save? : Qid .
vars user-dname source dname dname' newname fname ack nid sign tmp oname : Qid .
vars knowndishes : QidList .
vars udname : Qid .
vars outQ toks toks' toks0 toks1 toks2 edit-toks args fname?  dnames : QidList .
vars t pntlT occsT occsT' occT occsT1 occsT2 occsT0 : Term .
vars dnotes dnotes' notes  : Notes .
vars res0?? res1?? res?? : [ResultPair?] .
vars adds removes tl : TermList .
vars ndl ndl' nds : NodeList .
var edl : EdgeList .
vars id ?string str clab : String .
var ?graph : Graph .
var module : Module .

******************************************************************************
**** using a predDefined dish, no editing
******************************************************************************

****              mod  kbnodes  occTL    occndl 
  op occTL2Nodes : Qid NodeList TermList NodeList -> NodeList .
  eq occTL2Nodes(modname,ndl,(t,tl),ndl') =
        occTL2Nodes(modname, ndl,tl,ndl' getNode(ndl,"occ",tm(modname,t))) .
  eq occTL2Nodes(modname,ndl,empty,ndl') = ndl' .

  op chatty2occsT : Qid NodeList QidList TermList  -> Term .
  eq chatty2occsT(modname,ndl, nil, tl) = occTL2occsT(tl) .
  ceq chatty2occsT(modname,ndl, oname toks, tl) = 
        chatty2occsT(modname,ndl,toks,
                     (if occT == 'none.Occs then tl else (tl,occT) fi))
    if nds := getNode(ndl,"chattylabel",sv(string(oname)))
    /\ notes := (if nds :: Node then nodeNotes(nds) else mt fi)
    /\ occT := tvalTerm(lookupd(notes,"occ",tm(modname,'none.Occs))) .

******************************************************************************
  eq isReq('predefDish) = true .
  eq enabled(wait4s,
            req('predefDish,ql(kbname user-dname newname dname toks), reqQ))
             = true .

  crl[predefDish]:
   [nil,  
    st(processing(req('predefDish, 
                      ql(kbname user-dname newname dname toks), 
                      reqQ0)), 
       wait4s,reqQ,es,log), 
   outQ] 
  =>
   [nil,
    st(ready, wait4s, (reqQ reqQ'), es', log), 
    outQ] 
  if {b,es'} := predefDish(es,kbname, user-dname, newname, dname)  
  /\ reqQ' := (if b 
               then reqQ0
               else req('logreq, ql('predefDish 'nodish 
                             kbname user-dname newname dname toks), 
                        reqQ0)
                fi)  .

  op predefDish : ESet Qid Qid Qid Qid -> BoolESet .
  ceq predefDish(es,kbname, user-dname, newname, dname) =
    {res?? :: ResultPair, 
      (if res?? :: ResultPair 
       then  addEntry(
               addEntry(es,
                       'tval, 'dish newname, dnotes, tm(modname,occsT)),
                       'qval,'knownDishes,ql(dnames newname user-dname))
       else es fi)}
  if tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,tm('BOOL,'true.Bool))
  /\ res?? := metaReduce([modname], 'pl2occs[mkConst(dname,'Dish)])
  /\ occsT := (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi)
  /\ ql(dnames) := getVal(es,'qval,'knownDishes,ql(nil))
  /\ dnotes := (("source" := ql('predef dname)),
                ("kbname" := ql(kbname)),
                ("user-dname" := ql(user-dname))) .


******************************************************************************
**** Create a new dish/initial state
**** (newDish kbname  g2dvname)
****   startup dish editor scope from (fetch kbname) . occ-labs, and userdname list

******* (getDish kbname g2dvname dname)
****        get the occs, occs2labs  
****      in viewer  get dishEditor from kbname, set selection labs

******* (setDish kbname g2dvname udname toks)
****     labs to occs using graph of kbname, gen fresh dname, add dname udname to
****     knownDishes,  and add tval dish dname (modname,occsT) to env
******* (displayDish kbname g2dvname udname toks)
****     setDish; dish2pnet; pnet2graph; defineGraph; showGraph
******************************************************************************
**** newDish
******************************************************************************
  eq isReq('newDish) = true .
  eq enabled(wait4s, req('newDish,ql(kbname g2dvname toks), reqQ))
            = not(waiting4(wait4s,g2dvname)) .

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

  op newDishTemplate : -> String .
  eq newDishTemplate = "(apply initDishEditor %kbname %dishnames)" .

  op mkNewDishExp : ESet Qid  -> String .
  ceq mkNewDishExp(es,kbname) =
      fillTemplate(newDishTemplate, 
           (("%kbname" :~ squote(string(kbname))),
            ("%dishnames" :~ ?string)))
    if dnames := qvalQidList(getVal(es,'qval,'knownDishes,ql(nil)))
    /\ ?string := known2userDnameArrStr(dnames,"") .

  op known2userDnameArrStr : QidList String -> String .
  eq known2userDnameArrStr(dname user-dname toks,str) = 
       known2userDnameArrStr(toks, str + " " + squote(string(user-dname))) .
  eq known2userDnameArrStr(toks,str) = "(array java.lang.String " + str + ")" .
 
******************************************************************************
**** getDish
******************************************************************************
  eq isReq('getDish) = true .
  eq enabled(wait4s, req('getDish,ql(kbname g2dvname user-dname toks), reqQ))
            = not(waiting4(wait4s,g2dvname)) .

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

  op getDishReplyTemplate : -> String .
  eq getDishReplyTemplate = "(apply getDishReply %kbname %dishoccs)" .

  op mkGetDishReplyExp : ESet Qid Qid -> String .
  ceq mkGetDishReplyExp(es,kbname,user-dname) =
      fillTemplate(getDishReplyTemplate, 
           (("%kbname" :~ squote(string(kbname))),
            ("%dishoccs" :~ ?string)))
    if dnames := qvalQidList(getVal(es,'qval,'knownDishes,ql(nil)))
    /\ dname  := lookupDname(dnames,user-dname)
    /\ tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,dumTv)
    /\ occsT := 
         (if dname == user-dname 
          then getPreDefDishOccs(es,modname,dname)
          else tvalTerm(getVal(es,'tval,'dish dname, tm(modname,'none.Occs)))
          fi) 
   /\ ndl := graphNodes(gvalGraph(getVal(es,'gval,kbname,gv(mtGraph))))
   /\ ?string := occTL2ArrExp(modname,ndl,occsT2occTL(occsT),"") .

  op getPreDefDishOccs : ESet Qid Qid -> Term .
  ceq getPreDefDishOccs(es,modname, dname) = occsT
  if res?? := metaReduce([modname], 'pl2occs[mkConst(dname,'Dish)])
  /\ occsT := (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi) .

  op lookupDname : QidList Qid -> Qid .
  eq lookupDname(dname dname' dnames, user-dname) = 
       (if user-dname == dname' 
        then dname 
        else lookupDname(dnames, user-dname) 
        fi) .
  eq lookupDname(dnames, user-dname) = 'unknown [owise] .


****               mod  kbnodes  occTL    occ-labs 
  op occTL2ArrExp : Qid NodeList TermList String -> String .
  ceq occTL2ArrExp(modname,ndl,(t,tl),str) =
        occTL2ArrExp(modname, ndl,tl, 
              str + (if clab == "" then "" else " " + squote(clab) fi))
   if nds := getNode(ndl,"occ",tm(modname,t))
   /\ sv(clab) := (if nds :: Node
                   then lookupd(nodeNotes(nds),"chattylabel",sv(""))
                   else sv("") fi) .
  eq occTL2ArrExp(modname,ndl,empty,str) = "(array java.lang.String " + str + ")" .
 
******************************************************************************
**** getAllDish
******************************************************************************
  eq isReq('getAllDish) = true .
  eq enabled(wait4s, req('getAllDish,ql(kbname g2dvname toks), reqQ))
            = not(waiting4(wait4s,g2dvname)) .

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

  op mkGetAllDishReplyExp : ESet Qid  -> String .
  ceq mkGetAllDishReplyExp(es,kbname) =
      fillTemplate(getDishReplyTemplate, 
           (("%kbname" :~ squote(string(kbname))),
            ("%dishoccs" :~ ?string)))
    if tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,dumTv)
    /\ occsT := tvalTerm(getVal(es,'tval,'dish 'allDish, tm(modname,'none.Occs)))
    /\ ndl := graphNodes(gvalGraph(getVal(es,'gval,kbname,gv(mtGraph))))
    /\ ?string := occTL2ArrExp(modname,ndl,occsT2occTL(occsT),"") .

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

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

  op getDishesReplyTemplate : -> String .
  eq getDishesReplyTemplate = "(apply getDishReply %kbname %dishoccs)" .

  op mkGetDishesReplyExp : ESet Qid QidList -> String .
  ceq mkGetDishesReplyExp(es,kbname,toks) =
      fillTemplate(getDishReplyTemplate, 
           (("%kbname" :~ squote(string(kbname))),
            ("%dishoccs" :~ ?string)))
    if dnames := qvalQidList(getVal(es,'qval,'knownDishes,ql(nil)))
    /\ tm(modname,pntlT) := getVal(es,'tval, 'tkb kbname,tm('BOOL,'true.Bool))
    /\ occsT :=  dnames2OccsTX([modname],es,toks,dnames,'none.Occs)
   /\ ndl := graphNodes(gvalGraph(getVal(es,'gval,kbname,gv(mtGraph))))
   /\ ?string := occTL2ArrExp(modname,ndl,occsT2occTL(occsT),"") .

  op dnames2OccsTX : Module ESet QidList  QidList Term -> Term .
  eq dnames2OccsTX(module,es,nil,knowndishes,occsT) = occsT .
 ceq dnames2OccsTX(module,es,udname dnames,knowndishes,occsT) = 
          dnames2OccsTX(module,es,dnames,knowndishes,occsT1)
  if dname  := lookupDname(knowndishes,udname)  **** the maude dname
  /\ tm(modname,occsT2) := getVal(es,'tval,'dish dname,tm('BOOL,'true.Bool))
  /\ res?? := (if occsT2 == 'true.Bool
               then metaReduce(module, 'pl2occs[mkConst(dname,'Dish)]) 
               else {occsT2,'Occs}
              fi)
  /\ occsT0 := (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi) 
  /\ res1?? := metaReduce(module, 'addOccs[occsT,occsT0])
  /\ occsT1 := (if res1?? :: ResultPair then getTerm(res1??) else 'none.Occs fi)
  .


******************************************************************************
**** setDish
******************************************************************************
  eq isReq('setDish) = true .
  eq enabled(wait4s,
            req('setDish,ql(kbname user-dname newname toks), reqQ))
             = true .

  crl[setDish]:
   [nil,  
    st(processing(req('setDish, 
                      ql(kbname user-dname newname toks), 
                      reqQ0)), 
       wait4s,reqQ,es,log), 
   outQ] 
  =>
   [nil,
    st(ready, wait4s, (reqQ reqQ'), es', log), 
    outQ] 
  if {b,es'} := setDish(es,kbname, user-dname, newname, toks)  
  /\ reqQ' := (if b 
               then reqQ0
               else req('logreq, ql('setDish 'failed
                             kbname user-dname newname toks), 
                        reqQ0)
                fi)  .

****            kbname  user-dname newname 
  op setDish : ESet Qid   Qid   Qid  QidList -> BoolESet .
  ceq setDish(es,kbname, user-dname,newname,toks) =
    {b, (if b
         then addEntry(
                addEntry(es,
                        'tval, 'dish newname, dnotes, tm(modname,occsT)),
                        'qval,'knownDishes,ql(dnames newname user-dname))
       else es fi)}
   if  ql(dnames) := getVal(es,'qval,'knownDishes,ql(nil))
   /\ tm(modname,pntlT) := getVal(es,'tval,'tkb kbname,dumTv)
   /\ ndl := graphNodes(gvalGraph(getVal(es,'gval,kbname,gv(mtGraph))))
   /\ occsT := chatty2occsT(modname,ndl, toks, empty)
   /\ b := modname =/= 'BOOL and ndl =/= nil 
   /\ dnotes := (("kbname" := ql(kbname)),
                 ("user-dname" := ql(user-dname))) .



******************************************************************************
******* (displayNewDish kbname g2dvname udname toks)
****     setDish; dish2pnet; pnet2graph; defineGraph; showGraph
******************************************************************************
  eq isReq('displayNewDish) = true .
  eq enabled(wait4s,
            req('displayNewDish,ql(kbname g2dvname user-dname toks), reqQ))
             = true .

  crl[displayNewDish]:
   [nil,
    st(processing(req('displayNewDish, ql(kbname g2dvname user-dname toks), 
                       reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, incGlobalCounter(es,1), log), outQ]
   if newname := qid("dish" + getGlobalCounter(es))
   /\ reqQ0 :=
       req('setDish,ql(kbname user-dname newname toks),
         req('displayDishnet,ql(kbname g2dvname newname),     
               reqQ')) .


******************************************************************************
******* (displayAllDish kbname g2dvname toks)

******************************************************************************
  eq isReq('displayAllDish) = true .
  eq enabled(wait4s,
            req('displayAllDish,ql(kbname g2dvname toks), reqQ))
             = true .

  crl[displayNewDish]:
   [nil,
    st(processing(req('displayAllDish, ql(kbname g2dvname toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es, log), outQ]
   if reqQ0 :=
         req('displayDishnet,ql(kbname g2dvname 'AllDish),reqQ') .



***(
******************************************************************************
******* (displayDishes kbname g2dvname user-dname toks)
****     setDish; dish2pnet; pnet2graph; defineGraph; showGraph
******************************************************************************
  eq isReq('displayDishes) = true .
  eq enabled(wait4s,
            req('displayDishes,ql(kbname g2dvname  user-dname toks), reqQ))
             = true .

  crl[displayDishes]:
   [nil,
    st(processing(req('displayDishes, ql(kbname g2dvname  user-dname toks), 
                       reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, incGlobalCounter(es,1), log), outQ]
   if newname := qid("dish" + getGlobalCounter(es))
   /\ reqQ0 :=
       req('setDishes,ql(kbname user-dname newname toks),
         req('displayDishnet,ql(kbname g2dvname newname),     
               reqQ')) .

)
endm
