******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-JSON is
  inc RFE  .   *** rewriter + filemanager
  inc PLA-AUX .

**** 17Jan04 
  inc PL2TLT .
  
  inc MAUDE2JSON .
  inc NET2JNET .


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

var n : Nat .
vars mname g2dname g2dvname kbname modname restore? save? : Qid .
vars type tkbFname occsFname graphFname user-dname dir  : Qid .
vars outQ toks toks' qidl dnames : QidList .
var ?graph : Graph .
vars pntlT occsT ridT lhs rhs : Term .
vars res0?? res1?? res?? : [ResultPair?] .
vars pnotes gnotes notes : Notes .
var ndl : NodeList .
var edl : EdgeList .
var id ?string str : String .

vars fname locmname modmname pmname cmname gmname : Qid .
vars opsfname rulesfname occsfname modsfname locsfname sitesfname : Qid .
var dname netname rid : Qid .

var rule : Rule .
vars rules orules : RuleSet .
vars pntTL tl : TermList .
var mod : Module .
var attrs : AttrSet .

******************************************************************************
**** JSON management 
****  assume addEntry(es,'tval,'tkb kbname, pnotes, tm(modname,pntlT))
****         addEntry(es,'gval,kbname, gnotes, gv(kbgraph))
**** first generate occsmap using 
****  op tkb2occmap : ESet Qid Qid -> ESet .
****     addEntry(es,'qval,kbname, occnotes, ql(nil))

**** defineJSON modname (<class>OPS) kbname (where to find tkb and occmap) 
**** createDef<class> generate <class>.lsp file
****  createDefLocs,createDefMods,createDefEntities,createDefOccs,createDefRules, 
**** send load expression to g2dActor 

******************************************************************************
**** (createDefLocs locs.json Tiny LOCATIONOPS)
  eq isReq('createDefLocs) = true .
  eq enabled(wait4s,req('createDefLocs,ql(fname kbname modname toks),reqQ)) 
       = true .

**** assumes modname is the OPS module for location constants
  rl[createDefLocs]:
   [nil,
    st(processing(req('createDefLocs,ql(fname kbname modname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(locs2json(modname))), reqQ')), 
       es,
       log),
       outQ ] .



******************************************************************************
**** (createDefMods mods.json Tiny MODIFICATIONOPS)

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

**** assumes modname is the OPS module for modification constants
  rl[createDefMods]:
   [nil,
    st(processing(req('createDefMods,ql(fname kbname modname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(mods2json(modname))), reqQ')), 
       es,
       log),
       outQ ] .


******************************************************************************
**** (createDefEntities entities.json Tiny PROTEINOPS CHEMICALOPS GENEOPS)

  eq isReq('createDefEntities) = true .
  eq enabled(wait4s,req('createDefEntities,
                         ql(fname kbname pmname cmname gmname toks), reqQ)) 
       = true .

**** assumes pmname cmname gmname are the OPS module 
****   for protein,chemical, and gene constants
  rl[createDefEntities]:
   [nil,
    st(processing(req('createDefEntities,
                      ql(fname kbname pmname cmname gmname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(entities2json(pmname,cmname,gmname))),
                reqQ')), 
       es,
       log),
       outQ ] .


******************************************************************************
**** (createDefOccs occs.json Tiny)
  eq isReq('createDefOccs) = true .
  eq enabled(wait4s,req('createDefOccs,
                         ql(fname kbname toks), reqQ)) 
       = true .

**** assumes tkb and occsmap defined
  rl[createDefOccs]:
   [nil,
    st(processing(req('createDefOccs, ql(fname kbname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(occs2json(es,kbname))),
                reqQ')), 
       es,
       log),
       outQ ] .

******************************************************************************
**** (createDefRules rules.json Tiny)

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

**** assumes tkb defined
  crl[createDefRules]:
   [nil,
    st(processing(req('createDefRules, ql(fname kbname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
            ql(fname 'C str2toks(str)),
                reqQ')), 
       es,
       log),
       outQ ] 
  if str := rules2json(es,kbname) .


******************************************************************************
***** putting it all together 
**** (createDefJKB kbname LOCATIONOPS MODIFICATIONOPS 'PROTEINOPS, 'CHEMICALOPS, 'GENEOPS)
**** file names hardwired for now
******************************************************************************
**** (createDefJKB Tiny LOCATIONOPS MODIFICATIONOPS PROTEINOPS CHEMICALOPS GENEOPS)

  eq isReq('createDefJKB) = true .
  eq enabled(wait4s, 
        req('createDefJKB,ql(kbname locmname modmname pmname cmname gmname toks), 
                        reqQ)) 
       = true .

  crl[createDefJKB]:
   [nil,
    st(processing(
        req('createDefJKB,ql(kbname locmname modmname pmname cmname gmname toks), 
                        reqQ')),
       wait4s,reqQ,es,log), 
    outQ]
    =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es, log), outQ]
   if
    reqQ0 :=
       req('createDefLocs,ql('JSON/locs.json kbname locmname),
         req('createDefMods,ql('JSON/mods.json kbname modmname),
           req('createDefEntities,ql('JSON/entities.json kbname pmname cmname gmname),
             req('createDefOccs,ql('JSON/occs.json kbname),
               req('createDefRules,ql('JSON/rules.json kbname),
                   reqQ'))))) .


******************************************************************************
**** (createDefBasicOps JSONB/basicops.json LOCATIONOPS MODIFICATIONOPS PROTEINOPS CHEMICALOPS GENEOPS)

  eq isReq('createDefBasicOps) = true .
  eq enabled(wait4s,req('createDefBasicOps,ql(fname toks), reqQ)) 
       = true .

**** assumes pmname cmname gmname are the OPS module 
  rl[createDefBasicOps]:
   [nil,
    st(processing(req('createDefBasicOps, ql(fname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(basicOps2json(toks,""))), reqQ')), 
       es,
       log),
       outQ ] .

******************************************************************************
***** putting it all together 
**** (createDefBasicJKB dir kbname LOCATIONOPS MODIFICATIONOPS PROTEINOPS, CHEMICALOPS, GENEOPS)
**** 
******************************************************************************
**** (createDefBasicJKB JSONB RKB LOCATIONOPS MODIFICATIONOPS PROTEINOPS CHEMICALOPS GENEOPS)

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

  crl[createDefBasicJKB]:
   [nil,
    st(processing(
        req('createDefBasicJKB,ql(dir kbname toks), reqQ')),
       wait4s,reqQ,es,log), 
    outQ]
    =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es, log), outQ]
   if opsfname := qid(string(dir) + "/" + "basicOps.json")
   /\ modsfname := qid(string(dir) + "/" + "mods.json")
   /\ locsfname := qid(string(dir) + "/" + "locs.json")
   /\ occsfname := qid(string(dir) + "/" + "occs.json")
   /\ rulesfname := qid(string(dir) + "/" + "rules.json")
   /\ reqQ0 :=
       req('createDefBasicOps,ql(locsfname 'LOCATIONOPS),
         req('createDefBasicOps,ql(modsfname 'MODIFICATIONOPS),
           req('createDefBasicOps,ql(opsfname toks),
             req('createDefOccs,ql(occsfname kbname),
               req('createDefRules,ql(rulesfname kbname),
                   reqQ'))))) .


******************************************************************************
***** putting it all together -- omitting unused ops
**** (createDefBasicUJKB JSONU RKB  PROTEINOPS, CHEMICALOPS, GENEOPS)
**** 
******************************************************************************

  eq isReq('createDefBasicUJKB) = true .
  eq enabled(wait4s, req('createDefBasicUJKB,ql(dir kbname toks), reqQ)) = true .
  crl[createDefBasicUJKB]:
   [nil,
    st(processing(
        req('createDefBasicUJKB,ql(dir kbname toks), reqQ')),
       wait4s,reqQ,es,log), 
    outQ]
    =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es, log), outQ]
   if opsfname := qid(string(dir) + "/" + "basicOps.json")
   /\ modsfname := qid(string(dir) + "/" + "mods.json")
   /\ sitesfname := qid(string(dir) + "/" + "sites.json")
   /\ locsfname := qid(string(dir) + "/" + "locs.json")
   /\ occsfname := qid(string(dir) + "/" + "occs.json")
   /\ rulesfname := qid(string(dir) + "/" + "rules.json")
   /\ reqQ0 :=
       req('createDefBasicUOps,ql(kbname locsfname 'LOCATIONOPS),
         req('createDefBasicUOps,ql(kbname modsfname 'MODIFICATIONOPS),
          req('createDefBasicUOps,ql(kbname sitesfname 'SITEOPS),
           req('createDefBasicUOps,ql(kbname opsfname toks),
             req('createDefOccs,ql(occsfname kbname),
               req('createDefRules,ql(rulesfname kbname),
                   reqQ')))))) .


******************************************************************************
**** (createDefBasicUOps JSONU/basicOps.json PROTEINOPS CHEMICALOPS GENEOPS)
******************************************************************************

  eq isReq('createDefBasicUOps) = true .
  eq enabled(wait4s,req('createDefBasicUOps,ql(fname toks), reqQ)) 
       = true .

  rl[createDefBasicUOps]:
   [nil,
    st(processing(req('createDefBasicUOps, ql(kbname fname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C 
             str2toks(basicOps2json(getNotes(es,'qval,'occmap kbname),  
                                    toks,""))), 
             reqQ')), 
       es,
       log),
       outQ ] .


******************************************************************************
**** (jsonTest )
******************************************************************************
  var pname : Qid .

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

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


op jTestTemplate : -> String .
eq jTestTemplate = "(apply jsonTest %jstr)" .

op jTestExp : QidList -> String .
ceq jTestExp(toks) = fillTemplate(jTestTemplate, ("%jstr" :~ str))
if str :=  "\"{\\\"a\\\": \\\"aa\\\", \\\"b\\\": [\\\"b\\\", \\\"b\\\"]}\"" .


**** (dnetTest pname)

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

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


op jnetTestTemplate : -> String .
eq jnetTestTemplate = "(apply jsonNetTest %jstr)" .

op dnetTestExp : ESet Qid -> String .
ceq dnetTestExp(es,pname) = fillTemplate(jnetTestTemplate, ("%jstr" :~ str))
if str :=  mkJsonDishNet(es,pname) .


**** (pnet2jkb g2dvname pname)

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

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

op pnet2jkbTemplate : -> String .
eq pnet2jkbTemplate = "(apply addJNet %name %jstr)" .

op pnet2jkb : ESet Qid -> String .
ceq pnet2jkb(es,pname) = 
       fillTemplate(jnetTestTemplate,
                   (("%name" :~ squote(string(pname))), ("%jstr" :~ str)))
if str :=  pnet2json(es,pname) .

******************************************************************************
**** (savePNet pname fname)

  eq isReq('savePNet) = true .
  eq enabled(wait4s,req('savePNet,ql(pname netname fname toks), reqQ)) = true .

**** assumes tkb defined
  crl[savePNet]:
   [nil,
    st(processing(req('savePNet, ql(pname netname fname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
            ql(fname 'C str2toks(str)),
                reqQ')), 
       es,
       log),
       outQ ] 
  if str := pnet2jsonSave(es,pname,netname) .




******************************************************************************
**** (mkNSaveDishNet RKB dir dname)
**** one dish

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

**** assumes tkb defined
  crl[mkNSaveDishNet]:
   [nil,
    st(processing(req('mkNSaveDishNet, ql(kbname dir dname toks),reqQ0)), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('predefDish, ql(kbname dname dname dname), 
          req('dish2pnet, ql(kbname dname pname),
            req('savePNet, ql(pname dname fname), reqQ0))) 
        ),
       incGlobalCounter(es,1),
       log),
       outQ ] 
   if pname := qid("pnet" + stringInc(getGlobalCounter(es)) )
   /\ fname := qid(string(dir) + "/" + string(dname) + ".json") .


  eq isReq('mkNSaveDishNets) = true .
  eq enabled(wait4s,req('mkNSaveDishNets, ql(kbname dir dnames), reqQ)) = true .

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

  crl[mkNSaveDishNets]:
   [nil,
    st(processing(req('mkNSaveDishNets,
                       ql(kbname dir dname dnames),reqQ0)), 
       wait4s,reqQ,es,log), 
    outQ]
  =>
   [nil, st(ready, wait4s,reqQ1,es,log),outQ ] 
   if reqQ1 :=
        (reqQ
           req('mkNSaveDishNet, ql(kbname dir dname),
           req('mkNSaveDishNets,ql(kbname dir dnames) ,reqQ0)))
       .

**** If toks non nil export the allDish as well
  eq isReq('Dishes2Json) = true .
  eq enabled(wait4s,req('Dishes2Json, ql(kbname modname toks), reqQ)) = true .

  crl[Dishes2Json]:
   [nil,
    st(processing(req('Dishes2Json, ql(kbname modname toks),reqQ0)), 
       wait4s,reqQ,es,log), 
    outQ]
  =>
   [nil, st(ready, wait4s,(reqQ reqQ1),es,log),outQ ] 
  if dnames := constListBySortX(upOpDecls(modname,true),
                              (lesserSorts([modname],'Dish) ; 'Dish ))
  /\ reqQ2 := 
        (if (size(dnames) == 1 or toks == nil)
          then reqQ0 
          else req('mkNSaveAllDish, ql(kbname 'DishNets), reqQ0) fi)
  /\ reqQ1 :=
      req('mkNSaveDishNets,ql(kbname 'DishNets dnames),reqQ2) .

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

  crl[mkNSaveAllDish]:
   [nil,
    st(processing(req('mkNSaveAllDish, ql(kbname dir toks),reqQ0)), 
       wait4s,reqQ,es,log), 
    outQ]
  =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
          req('dish2pnet, ql(kbname 'allDish pname),
            req('savePNet, ql(pname 'allDish fname), reqQ0)) 
        ),
       incGlobalCounter(es,1),
       log),
       outQ ] 
   if pname := qid("pnet" + stringInc(getGlobalCounter(es)) )
   /\ fname := qid(string(dir) + "/" + string('allDish) + ".json") .


***********************************************************************
**** 15dec20 clt -- for generating json sort info
**** (createDefSorts JSONS/sorts.json ALLOPS)
****  inc ALLOPS2JSON .

***(
vars modname fname outQ : Qid .
vars toks : QidList .

var ctl : Control .
var wait4s : Wait4Set .
vars reqQ reqQ' : RequestQ .
vars es es' : ESet .
var log : Log .
)
  eq isReq('createDefSorts) = true .
  eq enabled(wait4s,req('createDefSorts,ql(fname modname toks), reqQ)) 
       = true .

  rl[createDefSorts]:
   [nil,
    st(processing(req('createDefSorts, ql(fname modname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
             ql(fname 'C str2toks(sorts2json(modname))), 
             reqQ')), 
       es,
       log),
       outQ ] .
       
***** 17Jan04
***********************************************************************
**** (createDefORules JSonB/orules.json QQQ RKB)

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

**** assumes tkb defined
  crl[createDefORules]:
   [nil,
    st(processing(req('createDefORules, 
                      ql(fname modname kbname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewrite, 
            ql(fname 'C str2toks(str)),
                reqQ')), 
       es,
       log),
       outQ ]
  if rules := upRls(modname,true)
            ****	getRls(upModule(modname,true)) 
  /\ orules := plrules2orules([modname],rules)
	/\ pntTL := orules2opntl([modname],orules) 
  /\ pnotes :=  ("source" := ql('orules modname))
  /\ notes := getNotes(es,'qval,kbname)
	/\ str := rules2json1(rules,notes,pntTL,"","") 
.
       
op orules2opntl : Module RuleSet -> TermList .
op orule2opntl : Module Rule -> TermList .

eq orules2opntl(mod,none) = empty .
eq orules2opntl(mod,rule rules) = 
     orule2opntl(mod,rule) , orules2opntl(mod,rules) .

ceq orule2opntl(mod,rl lhs => rhs [ label(rid) attrs ] .) = tl
  if ridT := mkQidConst(rid)
  /\ res?? := metaReduce(mod,'mkPNTrans[ridT,lhs,rhs]) 
  /\ tl := (if res?? :: ResultPair then getTerm(res??) else empty fi) .

*********************************************************
***** Stopping the whole thing
*********************************************************

 eq isReq('stopIOP) = true .
  eq enabled(wait4s,req('stopIOP,ql(toks),reqQ0)) =
      not(waiting4(wait4s,'graphics2d)) .

**** (stopIOP  toks)
 rl[stopIOP]:
   [nil,
    st(processing(req('stopIOP,ql(toks),reqQ0)),
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, 
       wait4s,
       reqQ reqQ0,es,log),
    outQ 'system '\n  'maude 
         '\n 'stop
         '\n  'system
    maudePrompt ] .   

endm