**** generates graph (with mt title and notes) from a PNTransList
**** if parent node set is given, use that to get node ids, ow generate


fmod PNTL2GRAPH is
  inc GRAPH .
  inc META-PETRI .
  inc PL-PRINT .
  inc QVAL .  inc SVAL .  inc TVAL .   **** note values
  inc NAT-QID .

************************      opdecls         ************************ 
**** TermList is list of pnet transitions (meta represented)
  op pntl2graph : Module TermList NodeList -> Graph .  
  op pntl2graph : Qid TermList NodeList -> Graph .  

**** pntl2g0 processes transitions one at a time 
****         modname pntTL    new     new      next  parent
  op pntl2g0 : Qid TermList NodeList EdgeList Nat NodeList -> Graph .

**** pntl2g1 processing  trans given by terms
****        modname ridT ioccsT ooccsT boccsT   pntTL
  op pntl2g1 : Qid Term Term   Term   Term    TermList 
              NodeList EdgeList Nat NodeList -> Graph .


**** get occ nodes for list of occ terms,
**** returns updated nodelist, ids of occ nodes, and next occ id nat
****           modname  occTL   found    next found  parent
  op getONodes : Qid TermList NodeList Nat NatList NodeList -> getNodesResult .
  op getONode : Qid Term NodeList Nat NodeList -> getNodesResult .

****                                            pre     post
  op getRNode : Qid Term NodeList Nat NodeList NatList NatList -> getNodesResult .

**** make Occ or Rule node with atts computed from occ or rule id term
  op mkONode : Qid Term Nat -> Node .
  op mkRNode : Qid Term Nat String String -> Node .

**** making incoming, outgoing and bidir edges, with empty notes
  ops mkIedges mkOedges mkBedges : NatList Nat EdgeList -> EdgeList .

************************    end opdecls        ************************ 

  vars t ridT ioccsT ooccsT boccsT pntlT preT postT thT locT : Term .
  vars pntTL tl : TermList .
  vars res0?? res1?? res2?? : [ResultPair?] .
  var mod : Module .
  var modname : Qid .
  vars ndl ndl' indl ondl bndl rndl pndl node? : NodeList .
  var nendl : NeNodeList .
  vars edl iedl oedl bedl : EdgeList .
  vars n n' id n0 n1 n2 n3 : Nat .
  vars ids inl onl bnl rnl : NatList .
  var id? : FindResult .
  vars thStr locStr inlStr onlStr : String .

**** trying more efficient flattening of occs term
  eq pntl2graph(mod,pntTL,pndl) = pntl2g0(getName(mod),pntTL,nil,nil,0,pndl) .
  eq pntl2graph(modname,pntTL,pndl) = pntl2g0(modname,pntTL,nil,nil,0,pndl) .
  eq pntl2g0(modname,empty,ndl,edl,n,pndl) = graph("",mt,ndl,edl) .
  eq pntl2g0(modname,('pnTrans[ridT,ioccsT,ooccsT,boccsT], pntTL), 
                  ndl,edl,n,pndl) = 
      pntl2g1(modname,ridT,ioccsT,ooccsT,boccsT,pntTL,ndl,edl,n,pndl) .

  ceq  pntl2g1(modname,ridT,ioccsT,ooccsT,boccsT,pntTL,ndl,edl,n,pndl) =
      pntl2g0(modname,pntTL, rndl,bedl,n3,pndl)
  if {{indl,n0},inl} := getONodes(modname,occsT2occTL(ioccsT),ndl,n,(nil).NatList,
                                  pndl)
  /\ {{ondl,n1},onl} := getONodes(modname,occsT2occTL(ooccsT),indl,n0,
                                   (nil).NatList, pndl)
  /\ {{bndl,n2},bnl} := getONodes(modname,occsT2occTL(boccsT),ondl,n1,
                                   (nil).NatList, pndl)
  /\ {{rndl,n3},rnl} := getRNode(modname,ridT,bndl,n2,pndl, inl bnl, onl bnl)
  /\ iedl := mkIedges(inl,rnl,edl)
  /\ oedl := mkOedges(onl,rnl,iedl)
  /\ bedl := mkBedges(bnl,rnl,oedl)
.

****  op getONodes : Qid TermList NodeList Nat NatList NodeList 
****                 -> getNodesResult .
****  op getRNode : Qid Term NodeList Nat NodeList NatList NatList -
****                     > getNodesResult .
****  op mkONode : Qid Term Nat -> Node .
****  op mkRNode : Qid Term Nat -> Node .

  eq getONodes(modname,empty,ndl,n,ids,pndl) = {{ndl,n},ids} .
  ceq getONodes(modname,(t,tl),ndl,n,ids,pndl) =
        getONodes(modname,tl,ndl',n',(ids id),pndl) 
  if {{ndl',n'},id} := getONode(modname,t,ndl,n,pndl) .

  ceq getONode(modname,t,ndl,n,nendl) =
      (if node? :: Node
       then (if getNode(ndl,id?) :: Node
             then {{ndl,n}, id?}   *** already in graph
             else {{ndl node?,n},id?}
             fi)
        else {{ndl,n}, (nil).NatList}  **** shouldn't happen
        fi)
  if node? := getNode(nendl, "occ", tm(modname,t) )
  /\ id? := (if node? :: Node then nodeId(node?) else notFound fi)  .

  ceq getONode(modname,t,ndl,n,nil) =
     (if id? :: Nat
      then {{ndl,n}, id?}
      else {{ndl mkONode(modname,t,n), s n}, n}
      fi)        
  if id? := findNode(ndl, "occ", tm(modname,t) ) .

  eq mkONode(modname,t,n) =
      nd(n,
        (("type" := sv("occ")),
         ("occ" := tm(modname,t)),
         (if isOccT(t)
          then (("label" :=  sv(printThing([modname],occT2thT(t)))),
                ("loc" :=  sv(printLoc([modname],occT2locT(t)))),
                ("chattylabel" := sv(printThing([modname],occT2thT(t))
                                     + locsepchar
                                     + printLoc([modname],occT2locT(t)))) )
          else (("label" := sv("???")),
                ("loc" := sv("???")),
                ("chattylabel" := sv("???" + locsepchar + "???")) )
          fi) 
         )) .

****  op getRNode : Module Term NodeList Nat NodeList NatList NatList 
****                -> getNodesResult .
  ceq getRNode(modname,ridT,ndl,n,nendl,inl,onl) =
      (if node? :: Node
       then (if getNode(ndl,id?) :: Node
             then {{ndl,n}, id?}   *** already in graph
             else {{ndl node?, n},id?}
             fi)
        else {{ndl,n}, (nil).NatList}  **** shouldn't happen
        fi)
  if node? := getNode(nendl, "rule", tm(modname, ridT) ) 
  /\ id? := (if node? :: Node then nodeId(node?) else notFound fi)  .

  ceq getRNode(modname,ridT,ndl,n,nil,inl,onl) =
     (if id? :: Nat
      then {{ndl,n}, id?}
      else {{ndl mkRNode(modname,ridT,n,natl2str(inl),natl2str(onl)), s n}, n}
      fi)        
  if id? := findNode(ndl, "rule", tm(modname, ridT)) .

**** pre/post
  eq mkRNode(modname,ridT,n,inlStr,onlStr) =
      nd(n,
        (("type" := sv("rule")),
         ("label" := sv(printRidT(ridT))),
         ("chattylabel" := sv(printRidTAll(ridT))),
         ("rule" := tm(modname, ridT)),
         ("pre" := sv(inlStr)),
         ("post" := sv(onlStr)) ) ) .

  eq mkIedges(nil,n,edl) =  edl .
  eq mkIedges(n' inl,n,edl) =
         mkIedges(inl,n,edl ed(n',n,("type" := sv("unidir")))) .
****  eq mkIedges(inl,rnl,edl) = edl [owise] .

  eq mkOedges(nil,n,edl) =  edl .
  eq mkOedges(n' onl,n,edl) = 
        mkOedges(onl,n,edl ed(n,n',("type" := sv("unidir")))) .
****  eq mkOedges(onl,rnl,edl) = edl [owise] .

  eq mkBedges(nil,n,edl) =  edl .
  eq mkBedges(n' bnl,n,edl) = 
        mkBedges(bnl,n,edl ed(n',n, ("type" := sv("bidir")))) .
****  eq mkBedges(bnl,rnl,edl) = edl [owise] .

endfm
*** load graph2g2d

