**** loadmaude loaded pla-kb.maude
******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-KB is
  inc RFE  .   *** rewriter + filemanager
  inc PLA-AUX .

  inc PL2TLT .
****  inc PNTL2GRAPH .
  inc KBGVAL-IO .
  inc NEW-GRAPH2G2D .
  inc PL-PRINT .

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

var n : Nat .
vars mname g2dname g2dvname kbname modname restore? save? qid : Qid .
vars type tkbFname occsFname graphFname user-dname : Qid .
vars outQ toks toks' qidl qidl0 qidl1 qidl2 dnames : QidList .
var ?graph : Graph .
vars pntlT occsT occT : Term .
var occTL : TermList .
vars res0?? res1?? res?? : [ResultPair?] .
vars pnotes gnotes notes onotes unotes dnotes : Notes .
var ndl : NodeList .
var edl : EdgeList .
var id ?string : String .

**** initOccMap
  vars locops modops entityops : QidList .
	vars locT thT pT msT t : Term .
	vars thTL tl : TermList .
	var opid : Qid .

var qids : QidSet .

var str : String .

******************************************************************************
**** KB management initKBnet
******************************************************************************
  eq isReq('initKBnet) = true .
  eq enabled(wait4s,req('initKBnet,ql(kbname modname toks),reqQ)) = true .

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

op initKBnet : ESet Qid Qid -> ESet .
ceq initKBnet(es,kbname,modname) =
        addEntry(es,'tval,'tkb kbname, pnotes, tm(modname,pntlT))
  if pntlT := pl2tlt(modname)
  /\ pnotes :=  ("source" := ql('rules modname))
   .


******************************************************************************
**** KB management initDKBnet  -- only instances needed for dish
**** (initDKBnet RKB QQQ allDish)
******************************************************************************
var dname : Qid .

  eq isReq('initDKBnet) = true .
  eq enabled(wait4s,req('initDKBnet,ql(kbname modname dname toks),reqQ)) = true .

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


***(
op initDKBnet : ESet Qid Qid Qid -> ESet .
ceq initDKBnet(es,kbname,modname,dname) =
        addEntry(es,'tval,'tkb kbname, pnotes, tm(modname,pntlT))
  if pntlT := pld2tlt(modname,dname)
  /\ pnotes :=  ("source" := ql('rules modname dname))
   .
)

op initDKBnet : ESet Qid Qid Qid -> ESet .
ceq initDKBnet(es,kbname,modname,dname) =
        addEntry(es,'tval,'tkb kbname, pnotes, tm(modname,pntlT))
  if pntlT := pld2tlt(modname,dname)
  /\ qids := getRuleIds(upRls(modname,true))  --- QidSet
  /\ qidl1 := qids2qidl(qids,nil)
  /\ qidl := pntTL2ridl(pntlT2pntTL(pntlT),nil) 
  /\ qidl0 :=  missingQids(qids,qidl,nil)
  /\ pnotes := (("source" := ql('rules modname dname)),
                ("rids" := ql(qidl1)), 
                ("tids" := ql(qidl)), 
                ("unreachable" := ql(qidl0)) 
                ) .

  eq isReq('initDAKBnet) = true .
  eq enabled(wait4s,req('initDAKBnet,ql(kbname modname toks),reqQ)) = true .

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

**** compute all dish   and save it
op initDAKBnet : ESet Qid Qid  -> ESet .
ceq initDAKBnet(es,kbname,modname) =
       addEntry(
         addEntry(es,'tval, 'dish 'allDish, dnotes, tm(modname,occsT)),
                     'tval,'tkb kbname, pnotes, tm(modname,pntlT))
  if dnames := constListBySortX(upOpDecls(modname,true),
                              (lesserSorts([modname],'Dish) ; 'Dish ))
  /\ occsT := dnames2OccsT([modname],dnames,'none.Occs) 
  /\ pntlT := pldrules2tlt([modname],upRls(modname,true),occsT) 
***  /\ ql(dnames) := getVal(es,'qval,'knownDishes,ql(nil))
  /\ dnotes := (("source" := ql('predef 'allDish)),
                ("kbname" := ql(kbname)),
                ("user-dname" := ql('allDish))) 
  /\ qids := getRuleIds(upRls(modname,true))  --- QidSet
  /\ qidl1 := qids2qidl(qids,nil)
  /\ qidl := pntTL2ridl(pntlT2pntTL(pntlT),nil) 
  /\ qidl0 :=  missingQids(qids,qidl,nil)
  /\ pnotes := (("source" := ql('rules modname)),
 ****              ("rids" := ql(qidl1)), 
 ****              ("tids" := ql(qidl)), 
                   ("unreachable" := ql(qidl0)) 
                ) .
***(
op plda2tlt  : Qid  -> Term . 
ceq plda2tlt(modname) = pldrules2tlt([modname],upRls(modname,true),occsT) 
   if dnames := constListBySortX(upOpDecls(modname,true),
                              (lesserSorts([modname],'Dish) ; 'Dish ))
   /\ occsT := dnames2OccsT([modname],dnames,'none.Occs)   .

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


)


op qids2qidl : QidSet QidList -> QidList .
eq qids2qidl(none,qidl) = qidl .
eq qids2qidl((qid ; qids),qidl) = qids2qidl(qids,qidl qid) .

op pntTL2ridl : TermList QidList -> QidList .
eq pntTL2ridl(empty,qidl) = qidl .
ceq pntTL2ridl((t,tl),qidl) = pntTL2ridl(tl,qidl (if qid == '? then nil else qid fi) ) 
  if qid := qidT2qid(pntT2ridT(t),'?)  .

op missingQids : QidSet QidList QidList -> QidList .
eq missingQids(none,qidl,qidl0) = qidl0 .
eq missingQids((qid ; qids),qidl,qidl0) = 
    (if occurs(qid,qidl) 
     then missingQids(qids,qidl,qidl0)  
     else missingQids(qids,qidl,qidl0 qid) 
     fi) .


******************************************************************************
**** KB management initKBgraph
******************************************************************************
  eq isReq('initKBgraph) = true .
  eq enabled(wait4s,req('initKBgraph,ql(kbname toks),reqQ)) = true .

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

op initKBgraph : ESet Qid -> ESet .
ceq initKBgraph(es,kbname) =
     addEntry(
      addEntry(updateNotes(es,'tval, 'tkb kbname,
                             insert("graph",ql(kbname), 
                                     getNotes(es,'tval, 'tkb kbname))),
               'gval,kbname, gnotes, gv(graph(string(kbname),mt,ndl,edl))),
             'qval,'knownKBs,ql(qidl kbname))
  if tm(modname,pntlT) := getVal(es,'tval,'tkb kbname, dumTv)
  /\ ql(qidl) := getVal(es,'qval,'knownKBs,ql(nil))
  /\ graph(id,notes,ndl,edl) := 
          (if modname == 'BOOL
           then mtGraph
           else pntl2graph([modname],pntlT2pntTL(pntlT),nil)
           fi)
  /\ gnotes := (("source" := ql('tkb kbname)), 
                ("kbname" := ql(kbname)))  .


******************************************************************************
**** KB management initOccMap
******************************************************************************
  eq isReq('initOccMap) = true .
  eq enabled(wait4s,req('initOccMap,ql(kbname toks),reqQ)) = true .

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


***(
addEntry(es,'tval,'tkb kbname, pnotes, tm(modname,pntlT))
addEntry(es,'gval,kbname, gnotes, gv(graph(string(kbname),mt,ndl,edl)))
)

**** make occmap from tkb

  op initOccMap : ESet Qid  -> ESet .
 ceq initOccMap(es,kbname) = 
        addEntry(es,'qval, 'occmap kbname, (onotes,unotes),ql(nil))
 if tm(modname,pntlT) := getVal(es,'tval,'tkb kbname, tm('QQQ,'nil.PNTransList))
 /\ res?? := metaReduce([modname],'allOccs[pntlT]) 
 /\ occsT := (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi)
 /\ onotes := occTL2occnotes(modname,occsT2occTL(occsT),mt) 
 /\ unotes := genUsedX(onotes,nil,nil,nil) .


  op occTL2occnotes : Qid TermList Notes -> Notes .
  op occT2occnotes : Qid Term Notes -> Notes .
  eq occTL2occnotes(modname,empty,notes) = notes .
  eq occTL2occnotes(modname,(occT,occTL),notes) =  
       occTL2occnotes(modname,occTL,
                      (notes, (occT2chatty(occT) := tm(modname,occT)))) .

***(
	op genUsed : ESet Qid -> ESet .
	eq genUsed(es,kbname) =
	    genUsedX(es,getNotes(es,'occmap kbname),nil,nil,nil) .
	op genUsedX : ESet Notes QidList QidList QidList -> ESet .
	eq genUsedX(es,mt,locops,modops,entityops) =
	      addEntry(
	       addEntry(
	        addEntry(es,'qval,'usedLocNames,ql(elimDups(locops))),
	                    'qval,'usedModifications, ql(elimDups(modops))),
	                    'qval,'usedEntities, ql(elimDups(entityops))) .
)
	op genUsedX :  Notes QidList QidList QidList -> Notes .
	eq genUsedX(mt,locops,modops,entityops) =
	      (  ("usedLocNames" := ql(elimDups(locops))),
	        ("usedModifications" := ql(elimDups(modops))),
	        ("usedEntities" := ql(elimDups(entityops))) ) .

	ceq genUsedX(((id := tm(modname,occT)), notes),locops,modops,entityops) =
	    genUsedX(notes,
	             (locops getName(locT)), 
	             (modops sthTL2mods(thTL,nil)), 
	             (entityops sthTL2entities(thTL,nil)) ) 
	if locT := occT2locT(occT)
	/\ thT := occT2thT(occT)
	/\ thTL := flattenThingTL(thT,'_:_)  .
 
	***** TermList has only simple things
	op sthTL2mods : TermList QidList -> QidList .
	eq sthTL2mods(empty,qidl) = qidl .
	eq sthTL2mods((thT,thTL),qidl) = sthTL2mods(thTL,qidl sthT2mods(thT)) .

	op sthTL2entities : TermList QidList -> QidList .
	eq sthTL2entities(empty,qidl) = qidl .
	eq sthTL2entities((thT,thTL),qidl) = sthTL2entities(thTL,qidl sthT2entity(thT)) .

	op sthT2mods : Term  -> QidList .
	eq sthT2mods(thC:Constant) = nil .
	eq sthT2mods('`[_-_`][pT,msT]) = 
	      modTL2modops(modsT2modTL(msT,empty)) sthT2mods(pT) .   
	eq sthT2mods(thT) = nil [owise] .

	op sthT2entity : Term  -> QidList .
	eq sthT2entity(thC:Constant) = getName(thC:Constant) .
	eq sthT2entity('`[_-_`][pT,msT]) =
      	 sthT2entity(pT) modTL2entities(modsT2modTL(msT,empty)).
	eq sthT2entity(thT) = nil [owise] .

  op modTL2entities : TermList -> QidList .
  op modT2entities : Term -> QidList .
  op modArgs2entities : TermList -> QidList .
  op modArg2entities : Term -> QidList .

  eq modTL2entities(empty) = nil .
  eq modTL2entities((t,tl)) = modT2entities(t) modTL2entities(tl) .
	eq modT2entities(m:Constant) = nil .
	eq modT2entities(opid[tl]) = modArgs2entities(tl)  .
	eq modT2entities(t) = nil [owise] .
  eq modArgs2entities(empty)   = nil .
  eq modArgs2entities((t,tl))  = modArg2entities(t) modArgs2entities(tl) .
  eq modArg2entities(c:Constant) = getName(c:Constant) .
  eq modArg2entities(t) = nil [owise] .

	op modTL2modops : TermList -> QidList .
	op modT2modop : Term -> QidList .
	eq modTL2modops(empty) = nil .
	eq modTL2modops((t,tl)) = modT2modop(t) modTL2modops(tl) .

	eq modT2modop(m:Constant) = getName(m:Constant)  .
	eq modT2modop(opid[tl]) = opid  .
	eq modT2modop(t) = nil [owise] .

  op elimDups : QidList -> QidList .
  eq elimDups(qidl0 qid qidl1 qid qidl2) = elimDups(qidl0 qid qidl1 qidl2) .
  eq elimDups(qidl0) = qidl0 [owise] .

******************************************************************************
**** KB management initKB ~ initKBnet ; initKBGraph
******************************************************************************
  eq isReq('initKB) = true .
  eq enabled(wait4s,req('initKB,ql(kbname modname toks),reqQ)) = true .

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


******************************************************************************
***  KB management 
**** defineKBGraph send kb node info to viewer g2d
******************************************************************************

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

  crl[defineKBGraph]:
   [nil,
    st(processing(req('defineKBGraph, ql(kbname g2dvname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,
       (wait4s !
         wait4(g2dvname,kbname,
               req('logreq,ql('defineKBGraph kbname g2dvname),reqQ'))), 
       reqQ,
       es,
       log), outQ 
     g2dvname '\n mname '\n toks' maudePrompt ]
   if gv(?graph) := getVal(es,'gval,kbname,gv(mtGraph)) 
   /\ mname :=  getMaudeName(es)
   /\ ?string :=
        withAck((if (graphNodes(?graph) == nil)
                   then "(apply displayMessage \"Alert\" \"Empty Graph\")"
                   else mkdefKBGraphExp(kbname,graphNodes(?graph)) 
                   fi), mname,g2dvname) 
   /\ toks' := str2toks(?string) .

******************************************************************************
**** KB management saveKB, restoreKB
**** default filenames  <kbname>-tkb.txt <kbname>-occs.txt  <kbname>-graph.txt
**** use filemanager services
****  (save fname entry etype ids)
****  (restore fname vname stype)
******************************************************************************

  op mkKBFileName : Qid Qid -> Qid .
  eq mkKBFileName(kbname,type) = 
        qid(string(kbname) + "-" + string(type) + ".txt") .

**** save graph in reduced form
  eq isReq('saveKBG) = true .
  eq enabled(wait4s,
             req('saveKBG,ql(kbname modname graphFname toks),reqQ)) = true .
  crl[saveKBG]:
   [nil,  
    st(processing(req('saveKBG, ql(kbname modname graphFname toks),reqQ0)), 
       wait4s,reqQ,es,log), 
   outQ] 
  =>
   [nil,
    st(ready, wait4s, (reqQ reqQ1), es, log), 
    outQ] 
  if qidl := 
     '`( 'entry 'gval '`( 'qidlist kbname '`) '\n
           showNotes(getNotes(es,'gval,kbname)) '\n
           showKBGVal(modname,getVal(es,'gval,kbname,gv(mtGraph))) '`)
  /\ reqQ1 := req('filewrite,ql(graphFname 'C qidl), 
                   req('logreq,ql('saveKBG graphFname 'C kbname modname), 
                       reqQ0)) .

  eq isReq('saveKB) = true .
  eq enabled(wait4s,req('saveKB,ql(kbname toks),reqQ)) = true .
  crl[saveKB]:
   [nil,  
    st(processing(req('saveKB, ql(kbname toks),reqQ0)), 
       wait4s,reqQ,es,log), 
   outQ] 
  =>
   [nil,
    st(ready, wait4s, (reqQ reqQ1), es, log), 
    outQ] 
  if tkbFname := mkKBFileName(getNth(0,toks,kbname),'tkb)
  /\ graphFname := mkKBFileName(getNth(0,toks,kbname),'graph) 
  /\ tm(modname,pntlT) := getVal(es,'tval,'tkb kbname, tm('BOOL,'true.Bool))
  /\ reqQ1 :=  (if modname == 'BOOL
                then reqQ0   *** no kb
                else  req('save,ql(tkbFname 'C 'entry 'tval 'tkb kbname), 
                           req('saveKBG,ql(kbname modname graphFname), reqQ0) ) 
                fi)  .

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

  crl[restoreKB]:
   [nil,  
    st(processing(req('restoreKB, ql(kbname toks),reqQ0)), 
       wait4s,reqQ,es,log), 
   outQ] 
  =>
   [nil,
    st(ready, wait4s, (reqQ reqQ1), es, log), 
    outQ] 
  if tkbFname := mkKBFileName(getNth(0,toks,kbname),'tkb)
  /\ graphFname := mkKBFileName(getNth(0,toks,kbname),'graph) 
  /\ reqQ1 := req('restore,ql(tkbFname 'tmp 'entry), 
                  req('restore,ql(graphFname 'tmp 'entry), 
                    reqQ0))
   .


endm
