***(
in pl-print -- thT,locT extracted from occT by reflection

)

fmod META-PETRI is
  inc MY-META-ALL .

*** meta syntax for petri nets, pntrans, occs

  var  occT : Term .       **** '<_`,_>[thT,locT]
  var  occTL : TermList .  **** list of occTs
  var  neOccTL : NeTermList .
  var  occsT : Term .      ****  'none.Occs, occT or '__[occT0, occT1, occTL]

  var  pntT : Term .       **** 'pnTrans[....]
  var  pntTL : TermList .  **** list of pntTs
  var  nePntTL : NeTermList .
  var  pntlT : Term .      ****  'nil.PNTransList, pntT or '__[pntT0, pntT1, pntTL]
 
  vars thT locT : Term .                  **** thing and location terms
  vars ridT ioccsT ooccsT boccsT : Term . **** pntrans args

*** generic
  var b : Bool .
  var term  t t' : Term .
  var tl : TermList .
  var mod : Module .
  var res?? : [ResultPair?] .
  var qid : Qid .
  var qidl : QidList .

**** can we assume the qidlT is normalized?
**** converting metarep of a term of sort QidList to a termlist
**** with elements that metarepresent a term of sort Qid
**** metareduce first to flatten,  also ensures t is meaningful in mod
  op qidlT2tl : Module Term -> TermList .
  ceq qidlT2tl(mod, t) =
       (if hasSort(mod,t','QidList) 
           then (if hasSort(mod,t','Qid) 
                 then t'
                 else getArgs(t')
                 fi)
           else empty fi)
  if res?? := metaReduce(mod,t) 
  /\ t' := (if res?? :: ResultPair then getTerm(res??) else 'nil.QidList fi) .


**** converting a qidlist to a termlist 
  op qidl2tl : QidList -> TermList .
  eq qidl2tl(nil) = empty .
  eq qidl2tl(qid qidl) = (mkQidConst(qid), qidl2tl(qidl)) .

**** a qidTerm list to a term
  op qidTL2qidlT : TermList -> Term .
  eq qidTL2qidlT(empty) = 'nil.QidList .
  eq qidTL2qidlT(t) =  t .
  eq qidTL2qidlT((t,tl)) = '__[t,tl] .

  op qidl2qidlT : QidList -> Term .
  eq qidl2qidlT(qidl) = qidTL2qidlT(qidl2tl(qidl)) .



**** occ terms
  op mkOccT : Term Term -> Term .
  op isOccT : Term -> Bool .
  ops occT2thT occT2locT : Term -> TermList .   *** empty if arg not an occT
  op occTL2occTL : TermList -> TermList . **** flattens
  eq mkOccT(thT,locT) = '<_`,_>[thT,locT] .
  eq isOccT('<_`,_>[thT,locT]) = true .
  eq isOccT(term) = false [owise] .
  eq occT2thT('<_`,_>[thT,locT]) = thT .
  eq occT2thT(term) = empty [owise] .
  eq occT2locT('<_`,_>[thT,locT]) = locT .        
  eq occT2locT(term) = empty [owise] .

  op occTL2occsT : TermList -> Term .
  op occsT2occTL : Term -> TermList .
  op normalizeOccTL : TermList TermList Bool -> TermList .  **** flatten

**** assumes terms are Occ terms
  eq occTL2occsT(empty) = 'none.Occs .
  eq occTL2occsT(occT) = occT .
  eq occTL2occsT(neOccTL) = '__[neOccTL] .  **** could flatten tl

  eq occsT2occTL('none.Occs) = empty .
  eq occsT2occTL('__[occTL]) = occTL2occTL(occTL) .   **** flatten 
  eq occsT2occTL(term) = (if isOccT(term) then term else empty fi) [owise] .

  eq occTL2occTL(empty) = empty .
  eq occTL2occTL((occT,occTL)) = (occsT2occTL(occT), occTL2occTL(occTL)) .

  eq normalizeOccTL(empty,occTL,b) = 
       (if b then normalizeOccTL(occTL,empty,false) else occTL fi)  .
  eq normalizeOccTL((term,tl),occTL, b) =
       normalizeOccTL(tl,(occTL, occsT2occTL(term)),  
                       (if isOccT(term) then b else true fi)) .

  op occTLconc : TermList Term -> TermList .
  eq occTLconc(tl,term) = (if isOccT(term) then (tl,term) else tl fi) .

**** pnt terms
  op mkPntT : Term Term Term Term -> Term .
  op isPntT : Term -> Bool .
  ops pntT2ridT pntT2ioccsT pntT2ooccsT pntT2boccsT : Term -> TermList . 
                       *** empty if arg not a pntT
  op pntTL2pntTL : TermList -> TermList .

  eq mkPntT(ridT,ioccsT,ooccsT,boccsT) = 'pnTrans[ridT,ioccsT,ooccsT,boccsT] .
  eq isPntT('pnTrans[ridT,ioccsT,ooccsT,boccsT]) = true .
  eq isPntT(term) = false [owise] .
  eq pntT2ridT('pnTrans[ridT,ioccsT,ooccsT,boccsT]) = ridT .
  eq pntT2ridT(term) = empty [owise] .
  eq pntT2ioccsT('pnTrans[ridT,ioccsT,ooccsT,boccsT]) = ioccsT .
  eq pntT2ioccsT(term) = empty [owise] .
  eq pntT2ooccsT('pnTrans[ridT,ioccsT,ooccsT,boccsT]) = ooccsT .
  eq pntT2ooccsT(term) = empty [owise] .
  eq pntT2boccsT('pnTrans[ridT,ioccsT,ooccsT,boccsT]) = boccsT .
  eq pntT2boccsT(term) = empty [owise] .

  op pntTL2pntlT : TermList -> Term .
  op pntlT2pntTL : Term -> TermList .
  op normalizePntTL : TermList TermList Bool -> TermList .  **** flatten

  eq pntTL2pntlT(empty) = 'nil.PNTransList .
  eq pntTL2pntlT(pntT) = pntT .
  eq pntTL2pntlT(nePntTL) = '__[nePntTL] .  **** could flatten tl

  eq pntlT2pntTL('nil.PNTransList) = empty .
  eq pntlT2pntTL('__[pntTL]) = pntTL2pntTL(pntTL) .   **** flatten 
  eq pntlT2pntTL(term) = (if isPntT(term) then term else empty fi) [owise] .

  eq pntTL2pntTL(empty) = empty .
  eq pntTL2pntTL((pntT,pntTL)) = (pntlT2pntTL(pntT), pntTL2pntTL(pntTL)) .

  eq normalizePntTL(empty,pntTL,b) = 
       (if b then normalizePntTL(pntTL,empty,false) else pntTL fi)  .
  eq normalizePntTL((term,tl),pntTL,b) =
       normalizePntTL(tl,(pntTL, pntlT2pntTL(term)),  
                       (if isPntT(term) then b else true fi)) .

  op pntTLconc : TermList Term -> TermList .
  eq pntTLconc(tl,term) = (if isPntT(term) then (tl,term) else tl fi) .

**** pnet terms
  op mkPnT : Term Term -> Term .
  op isPnT : Term -> Bool .
  op pnT2pntlT : Term -> Term .
  op pnT2occsT : Term -> Term .

  eq mkPnT(pntlT,occsT) = 'pnet[pntlT,occsT] .
  eq isPnT('pnet[pntlT,occsT]) = true .
  eq isPnT(term) = false [owise] .
  eq pnT2pntlT('pnet[pntlT,occsT]) = pntlT .
  eq pnT2pntlT(empty) = empty [owise] . 
  eq pnT2occsT('pnet[pntlT,occsT]) = occsT .
  eq pnT2occsT(empty) = empty [owise] . 

  op metaGetTrans : TermList Term  -> TermList .
  eq metaGetTrans(empty,ridT) = empty .
  eq metaGetTrans((pntT,pntTL),ridT) =
      (if pntT2ridT(pntT) == ridT then pntT else metaGetTrans(pntTL,ridT) fi) .

**** phase out was in aux-eset
**** meta pnet ops
  ops pnetT2pntlT pnetT2occsT : Term -> Term .
  eq  pnetT2pntlT('pnet[pntlT,occsT]) = pntlT .
  eq  pnetT2pntlT(t) = 'nil.PNTransList [owise] .

  eq  pnetT2occsT('pnet[pntlT,occsT]) = occsT .
  eq  pnetT2occsT(t) = 'none.Occs [owise] .

endfm



fmod TEST-META-PETRI is
  inc META-PETRI .

  ops thT1 thT2 locT1 locT2 : -> Term .
  ops occT1 occT2 : -> Term .

  eq occT1 = mkOccT(thT1,locT1)  .
  eq occT2 = mkOccT(thT2,locT2)  .

  op occsT0 : ->  Term .
  eq occsT0 = occTL2occsT((occT1,occT2)) .

  ops pntT0 pntT1 : -> Term .
  eq pntT0 = mkPntT(mkQidConst('123),occT1,occT2,'none.Occs) .
  eq pntT1 = mkPntT(mkQidConst('321),occT2,occT1,'none.Occs) .

  op pntlT0 : -> Term . 
  eq pntlT0 =  pntTL2pntlT((pntT0,pntT1)) .        

  op pnT0 : -> Term .
  eq pnT0 = mkPnT(pntlT0,occsT0) .

***(
red  isOccT(occT1) .
red  occT2thT(occT1) .
red  occT2locT(occT1) .
red  occT2thT(thT1) .
red  occT2locT(thT1) .

red occsT2occTL(occsT0) .
red occTL2occsT(empty) .
red occTL2occsT(occT1) .

red isPntT(pntT0) .
red pntT2ridT(pntT0) .
red pntT2ridT(occT2) .
red pntT2ioccsT(pntT0) .
red pntT2ooccsT(pntT0) .
red pntT2boccsT(pntT0) .

red pntlT2pntTL(pntlT0) .

red pnT2pntlT(pnT0) .
red pnT2occsT(pnT0) .

red normalizeOccTL((occsT0, occT1, 'none.Occs),empty,false) .
red normalizePntTL((pntT0, pntlT0, 'nil.PNTransList),empty,false) .

red pntTLconc(pntT1,pntT0) .
red pntTLconc(pntT1,'nil.PNTransList) .

red occTLconc(occT2,occT1) .
red occTLconc(occT2,'none.Occs) .

)



endfm

