******************************************************************************
****  net2jnet
******************************************************************************
 
fmod NET2JNET is
  inc PL-PRINT .
  inc MAUDE2JSON-AUX .

vars qid pname modname ptype dname user-dname kbname parent netname : Qid .
var str : String .
vars t pnetT goccsT aoccsT aridsT : Term .
var tl : TermList .
var es : ESet .
var pnotes : Notes .
var bindings :  TBinds .



op jnetTemplate : -> String .
eq jnetTemplate =
"\"{\
\\\"stype\\\": \\\"jnet\\\",\
\\\"name\\\": %name,\
\\\"type\\\": %type,\
\\\"kbname\\\": %kbname,\
\\\"rids\\\": %rids,\
\\\"parent\\\": %parent,\
\\\"op\\\": %op,\
\\\"args\\\": %args,\
\\\"init\\\": %init\
}\"" .

*** pnotes source ~ dishnet dname; subnet opname; pathnet pname; 
**** xnotes source ?

op ssquoteQ : Qid -> String .
eq ssquoteQ(qid) = ssquote(string(qid)) .
op ssquote : String -> String .
eq ssquote(str) = "\\\"" + str + "\\\"" .

op occTL2ssqArr : TermList String -> String .
eq occTL2ssqArr(empty,str) = "[" + str + "]" .
eq occTL2ssqArr((t,tl),str) =
       occTL2ssqArr(tl,str + sep?(str,", ") + ssquote(occT2chatty(t))) .

op pntTL2ssqrids : TermList String -> String .
eq pntTL2ssqrids(empty,str) = "[" + str + "]" .
eq pntTL2ssqrids((t,tl),str) =
       pntTL2ssqrids(tl,str + sep?(str,", ") + 
                        ssquoteQ(qidT2qid(pntT2ridT(t),'noRid))) .


**** a qidlist Term  is 'nil.QidList, '__[tl] or a qidT
**** (note aRules :=(tval QQQ(nil).d))

op qidlT2qidTL : Term -> TermList .
op qidlT2qidTLX : TermList -> TermList .
*** eq qidlT2qidTL('nil.Qidlist) = empty .
eq qidlT2qidTL(c:Constant) = 
     if getName(c:Constant) == 'nil then empty else c:Constant fi .
eq qidlT2qidTL('__[tl]) = qidlT2qidTLX(tl) .
eq qidlT2qidTL(t) = t [owise]  .   *** should be a qidT

eq qidlT2qidTLX(empty) = empty .
eq qidlT2qidTLX((t,tl)) = (qidlT2qidTL(t), qidlT2qidTLX(tl)) .

op qidTL2ssqids : TermList String -> String .
eq qidTL2ssqids(empty,str) = "[" + str + "]" .
eq qidTL2ssqids((t,tl),str) = 
     qidTL2ssqids(tl,str + sep?(str,", ") + ssquoteQ(qidT2qid(t,'noRid)) ) . 



op mkJsonDishNet : ESet Qid -> String .
ceq mkJsonDishNet(es,pname) = fillTemplate(jnetTemplate,bindings)
   if tm(modname,pnetT) := getVal(es,'tval,'pnet pname,tm('BOOL,'true.Bool))
   /\ pnotes := getNotes(es,'tval, 'pnet pname)
***   /\ ql(ptype dname) := lookupd(pnotes,"source",ql('unknown 'unknown))
   /\ ql(dname user-dname) := lookupd(pnotes,"dishname",ql('unknown 'unknown))
   /\ ql(kbname) := lookupd(pnotes,"kbname",ql('unknown))
   /\ ioccs:String :=  occTL2ssqArr(occsT2occTL(pnetT2occsT(pnetT)),"")
   /\ rids:String := pntTL2ssqrids(pntlT2pntTL(pnetT2pntlT(pnetT)), "")
   /\ bindings := (
        ("%name" :~ ssquoteQ(pname)),
        ("%type" :~ ssquote("pnet")),
        ("%kbname" :~ ssquoteQ(kbname)),
        ("%rids" :~ rids:String),
        ("%parent" :~ ssquoteQ(kbname)) ,
        ("%op" :~ ssquote("dishnet")),
        ("%args" :~ ssquoteQ(user-dname)),
        ("%init" :~ ioccs:String)
     ) .


op subnetArgsTemplate : -> String .
eq subnetArgsTemplate =
"{\
\\\"goals\\\": %goals,\
\\\"avoids\\\": %avoids,\
\\\"hides\\\": %hides,\
}" .

*** sub or pathnet
op mkJsonPNet : ESet Qid -> String .
ceq mkJsonPNet(es,pname) = fillTemplate(jnetTemplate,bindings)
   if tm(modname,pnetT) := getVal(es,'tval,'pnet pname,tm('BOOL,'true.Bool))
   /\ pnotes := getNotes(es,'tval, 'pnet pname)
   /\ ql(ptype parent) := lookupd(pnotes,"source",ql('unknown 'unknown))
*** dishnet dname; subnet opname; pathnet pname; xnet ???; cnet
   /\ goccsT  := tvalTerm(lookupd(pnotes,"gOccs",tm(modname,'none.Occs)))
   /\ aoccsT  := tvalTerm(lookupd(pnotes,"aOccs",tm(modname,'none.Occs)))
   /\ aridsT  := tvalTerm(lookupd(pnotes,"aRules",tm(modname,'nil.QidList)))
   /\ ql(kbname) := lookupd(pnotes,"kbname",ql('unknown))
   /\ ioccs:String :=  occTL2ssqArr(occsT2occTL(pnetT2occsT(pnetT)),"")
   /\ rids:String := pntTL2ssqrids(pntlT2pntTL(pnetT2pntlT(pnetT)),"")
   /\ goccs:String :=  occTL2ssqArr(occsT2occTL(goccsT),"")
   /\ aoccs:String :=  occTL2ssqArr(occsT2occTL(aoccsT),"")
   /\ arids:String :=  qidTL2ssqids(qidlT2qidTL(aridsT),"")
   /\ bindings :=  (
        ("%name" :~ ssquoteQ(pname)),
        ("%type" :~ ssquote("pnet")),
        ("%kbname" :~ ssquoteQ(kbname)),
        ("%rids" :~ rids:String),
        ("%parent" :~ ssquoteQ(parent)) ,
        ("%op" :~ ssquoteQ(ptype)),
        ("%args" :~ fillTemplate(subnetArgsTemplate,
                        (("%goals"  :~ goccs:String),
                         ("%avoids" :~ aoccs:String),
                         ("%hides"  :~ arids:String)) ) ),
        ("%init" :~ ioccs:String)
        )  .

  op pnet2json : ESet Qid -> String .
 ceq pnet2json(es,pname) = fillTemplate(jnetTemplate,bindings)
   if tm(modname,pnetT) := getVal(es,'tval,'pnet pname,tm('BOOL,'true.Bool))
   /\ pnotes := getNotes(es,'tval, 'pnet pname)
   /\ ql(ptype parent) := lookupd(pnotes,"source",ql('unknown 'unknown))
   /\ ql(kbname) := lookupd(pnotes,"kbname",ql('unknown))
   /\ ioccs:String :=  occTL2ssqArr(occsT2occTL(pnetT2occsT(pnetT)),"")
   /\ rids:String := pntTL2ssqrids(pntlT2pntTL(pnetT2pntlT(pnetT)),"")
   /\ bindings :=  (
        ("%name" :~ ssquoteQ(pname)),
        ("%type" :~ ssquote("pnet")),
        ("%kbname" :~ ssquoteQ(kbname)),
        ("%rids" :~ rids:String),
        ("%init" :~ ioccs:String),
        ("%parent" :~ (if ptype == 'dishnet 
                       then ssquoteQ(kbname) 
                       else ssquoteQ(parent) fi)) ,
        ("%op" :~ ssquoteQ(ptype)),
        ("%args" :~ (if ptype == 'dishnet
                    then mkDishNetArgs(pnotes)
                    else mkSubnetArgs(pnotes) fi))
 
         )  .

op mkDishNetArgs : Notes -> String .
ceq mkDishNetArgs(pnotes) = ssquoteQ(user-dname)
 if ql(dname user-dname) := lookupd(pnotes,"dishname",ql('unknown 'unknown)) .

op mkSubnetArgs : Notes -> String .
ceq mkSubnetArgs(pnotes) = fillTemplate(subnetArgsTemplate,
                        (("%goals"  :~ goccs:String),
                         ("%avoids" :~ aoccs:String),
                         ("%hides"  :~ arids:String)) ) 
   if goccsT  := tvalTerm(lookupd(pnotes,"gOccs",tm('QQQ,'none.Occs)))
   /\ aoccsT  := tvalTerm(lookupd(pnotes,"aOccs",tm('QQQ,'none.Occs)))
   /\ aridsT  := tvalTerm(lookupd(pnotes,"aRules",tm('QQQ,'nil.QidList)))
   /\ goccs:String :=  occTL2ssqArr(occsT2occTL(goccsT),"")
   /\ aoccs:String :=  occTL2ssqArr(occsT2occTL(aoccsT),"")
   /\ arids:String :=  qidTL2ssqids(qidlT2qidTL(aridsT),"")
  .

************************************************************************** Saving to file -- one less level of quotes

op occTL2sqArr : TermList String -> String .
eq occTL2sqArr(empty,str) = "[" + str + "]" .
eq occTL2sqArr((t,tl),str) =
       occTL2sqArr(tl,str + sep?(str,", ") + squote(occT2chatty(t))) .

op pntTL2sqrids : TermList String -> String .
eq pntTL2sqrids(empty,str) = "[" + str + "]" .
eq pntTL2sqrids((t,tl),str) =
       pntTL2sqrids(tl,str + sep?(str,", ") + 
                        squote(string(qidT2qid(pntT2ridT(t),'noRid)))) .


op qidTL2sqids : TermList String -> String .
eq qidTL2sqids(empty,str) = "[" + str + "]" .
eq qidTL2sqids((t,tl),str) = 
     qidTL2sqids(tl,str + sep?(str,", ") + squote(string(qidT2qid(t,'noRid))) ) . 


op jnetSaveTemplate : -> String .
eq jnetSaveTemplate =
"\n {\"stype\" : \"jnet\",\n\
\t \"name\" : %name,\n\
\t \"type\" : %type,\n\
\t \"kbname\" : %kbname,\n\
\t \"parent\" : %parent,\n\
\t \"rids\" : %rids,\n\
\t \"init\" : %init,\n\
\t \"op\" : %op,\n\
\t \"args\" : %args\n}"
.

  op pnet2jsonSave : ESet Qid Qid -> String .
 ceq pnet2jsonSave(es,pname,netname) = fillTemplate(jnetSaveTemplate,bindings)
   if tm(modname,pnetT) := getVal(es,'tval,'pnet pname,tm('BOOL,'true.Bool))
   /\ pnotes := getNotes(es,'tval, 'pnet pname)
   /\ ql(ptype parent) := lookupd(pnotes,"source",ql('unknown 'unknown))
   /\ ql(kbname) := lookupd(pnotes,"kbname",ql('unknown))
   /\ ioccs:String :=  occTL2sqArr(occsT2occTL(pnetT2occsT(pnetT)),"")
   /\ rids:String := pntTL2sqrids(pntlT2pntTL(pnetT2pntlT(pnetT)),"")
   /\ bindings :=  (
        ("%name" :~ squote(string(netname))),
        ("%type" :~ squote("pnet")),
        ("%kbname" :~ squote(string(kbname))),
        ("%rids" :~ rids:String),
        ("%init" :~ ioccs:String),
        ("%parent" :~ (if ptype == 'dishnet 
                       then squote(string(kbname)) 
                       else squote(string(parent)) fi)) ,
        ("%op" :~ squote(string(ptype))),
        ("%args" :~ (if ptype == 'dishnet
                    then mkDishNetSaveArgs(pnotes)
                    else mkSubnetSaveArgs(pnotes) fi))
 
         )  .


op subnetArgsSaveTemplate : -> String .
eq subnetArgsSaveTemplate =
"{\
\"goals\": %goals,\
\"avoids\": %avoids,\
\"hides\": %hides,\
}" .

op mkDishNetSaveArgs : Notes -> String .
ceq mkDishNetSaveArgs(pnotes) = squote(string(user-dname))
 if ql(dname user-dname) := lookupd(pnotes,"dishname",ql('unknown 'unknown)) .

op mkSubnetSaveArgs : Notes -> String .
ceq mkSubnetSaveArgs(pnotes) = fillTemplate(subnetArgsSaveTemplate,
                        (("%goals"  :~ goccs:String),
                         ("%avoids" :~ aoccs:String),
                         ("%hides"  :~ arids:String)) ) 
   if goccsT  := tvalTerm(lookupd(pnotes,"gOccs",tm('QQQ,'none.Occs)))
   /\ aoccsT  := tvalTerm(lookupd(pnotes,"aOccs",tm('QQQ,'none.Occs)))
   /\ aridsT  := tvalTerm(lookupd(pnotes,"aRules",tm('QQQ,'nil.QidList)))
   /\ goccs:String :=  occTL2sqArr(occsT2occTL(goccsT),"")
   /\ aoccs:String :=  occTL2sqArr(occsT2occTL(aoccsT),"")
   /\ arids:String :=  qidTL2sqids(qidlT2qidTL(aridsT),"")
  .


endfm