***** pldrules2tlt

**** loadmaude loaded pl2tlt.maude

fmod PL2TLT is
  inc MY-META-ALL .
  inc META-PETRI .
**** assume PL + PETRI loaded

  vars lhs rhs t t' ioccsT ooccsT boccsT pntlT  ridT preOccsT postOccsT : Term .
  vars tl vals : TermList .
  var mod : Module .
  var v : Variable . var const : Constant . 
  var vs  : QidSet .
  vars sbs sbs' : SubstSet .
  var subst : Substitution .
  var cond : Condition .
  var rule : Rule .
  var rules : RuleSet .
  var attrs : AttrSet .
  var rid  qid modname dname : Qid .
  var vset : QidSet .
  var sortset : SortSet .  
  var n : Nat .
  var b b0 b1 : Bool .
  var res??  res0?? res1?? res2??  : [ResultPair?] .

	vars rinsts rinsts' : RInstSet .
	var rinst : RInst .
	vars occsT occsT' : Term .
	var orules : RuleSet .
	vars more? new? : Bool .
	vars occsT0 occsT1 : Term .
	var  dnames : QidList .

  sort SubstSet .
  op sb : Substitution -> SubstSet  [ctor] .
  op mt : -> SubstSet [ctor] .
  op __ :  SubstSet SubstSet -> SubstSet [ctor assoc comm id: mt] .
  eq sb(subst) sb(subst) = sb(subst) .

****************** op decls ***********************

**** map pl ruleset to PNTransList term 
**** pnTrans(rid,ioccs,ooccs,bokkc)
  ops pl2tlt  : Qid -> Term . ****

**** map set of pl rules to PNTransList term .
  ops plrules2tlt  : Module RuleSet -> Term . 

**** occs version of rules
  op plrules2orules : Module RuleSet -> RuleSet .
  op plrule2orule : Module Rule -> RuleSet .        **** 0 or 1 

**** PL rule condition has form thingVar soupVar := groundThingSoup
**** finds thing variable in PL rule condition
  op thingVar : Module TermList -> Qid .    
**** instance substs for PL rule condition
  op cond2sbs : Module Condition -> SubstSet .
  op cond2sbsX : Module Qid TermList -> SubstSet .

**** List of constants having one of given sorts
**** replace consSetBySort that returns a QidSet
  op constListBySort : OpDeclSet  SortSet  -> TermList .
  op constBySortZ : OpDecl  SortSet  -> TermList .

**** all instances given by condition for  PL conditional rule 
  op expandCond : Module Term Term Qid AttrSet SubstSet Nat -> RuleSet .

****  finds all substitutions for a set of variables
  op allInst : Module QidSet SubstSet -> SubstSet .
  op extendSbS : SubstSet Variable TermList -> SubstSet .
  op extendSbSX : SubstSet Variable Constant SubstSet -> SubstSet .

**** generates instances of orules
  op orules2pntl : Module RuleSet -> TermList .
  op orule2pntl : Module Rule -> TermList .
  op orule2pntlX : Module Term Term  Qid SubstSet Nat -> TermList .
  op orule2pnt : Module Term Term  Qid Substitution Nat -> TermList .

  op mkTransId : Qid Nat -> Qid .

****************** end op decls ***********************

**** basic in PL modules converting soup term to its 
  op soupT2tl : Module Term -> TermList .
  ceq soupT2tl(mod,t) =
       (if hasSort(mod,t','Soup)
        then (if (hasSort(mod,t','Thing)
                  or hasSort(mod,t','Location)
                  or hasSort(mod,t','Cell))
              then t'
              else (if getOp(t') == '__
                    then getArgs(t')
                    else empty fi)
               fi)
        else empty
        fi) 
    if res?? := metaReduce(mod,t)
    /\ t' := (if res?? :: ResultPair then getTerm(res??) else 'empty.Soup fi) .
    

**** mod must extend DISH-OPS
  op plT2occsT : Module Term -> Term .
  eq plT2occsT(mod,t) =
       (if metaReduce(mod,'pl2occs[t]) :: ResultPair 
        then getTerm(metaReduce(mod,'pl2occs[t])) 
        else 'none.Occs fi) .
  
**** map pl ruleset to PNTransList term .
****  ops pl2tlt  : Qid -> Term . ****
  eq pl2tlt(modname) = plrules2tlt([modname],upRls(modname,true)) .
***  eq pl2txlt(modname) = plrules2txlt([modname],upRls(modname,true)) .

**** map set of pl rules to PNTransList term .
****  ops plrules2tlt plrules2txlt : Module RuleSet -> Term . ****
***(  ceq plrules2txlt(mod,rules) =
     (if res?? :: ResultPair then getTerm(res??) else 'nil.PNTransList fi)
  if pntlT := plrules2tlt(mod,rules) 
  /\ res?? := metaReduce(mod,'pntl2pntxl[pntlT]) .
)
  eq plrules2tlt(mod,rules) =
       pntTL2pntlT(orules2pntl(mod, plrules2orules(mod,rules))) .

**** occs version of rules
****  op plrules2orules : Module RuleSet -> RuleSet .
****  op plrule2orule : Module Rule -> RuleSet .        **** 0 or 1 

  eq plrules2orules(mod,none) = none .
  eq plrules2orules(mod,rule rules) = 
        plrule2orule(mod,rule) plrules2orules(mod, rules) .

  ceq plrule2orule(mod,rl lhs => rhs [ attrs ] .) =
      (if ioccsT == 'none.Occs or ooccsT == 'none.Occs
       then none
       else  (rl ioccsT => ooccsT [ attrs ] .)
       fi)
     if ioccsT := plT2occsT(mod,lhs)
     /\ ooccsT := plT2occsT(mod,rhs) .
 
**** assumes conditions have the form thingvar soupvar := gs 
**** where thingvar occurs on lhs and gs is a group soup of things
**** Example: ?Bmp:Bmp S:Soup := Bmp2 Bmp4 Bmp7
  ceq plrule2orule(mod, (crl lhs => rhs if cond [ label(rid) attrs ] .)) =
      (if ioccsT == 'none.Occs or ooccsT == 'none.Occs
       then none
       else expandCond(mod, ioccsT, ooccsT,rid,attrs,sbs,0)
       fi)
     if ioccsT := plT2occsT(mod,lhs)
     /\ ooccsT := plT2occsT(mod,rhs) 
     /\ sbs := cond2sbs(mod,cond) .

****  op thingVar : Module TermList -> Qid .
  eq thingVar(mod,empty) = 'nonVariable .
  eq thingVar(mod,(t,tl)) =
     (if hasSort(mod,t,'Thing) :: Bool
      then (if hasSort(mod,t,'Thing) 
            then t
            else thingVar(mod,tl)
            fi)
      else 'nonVariable fi) .


****  op cond2sbs : Module Condition -> SubstSet .
****  op cond2sbsX : Module Qid TermList -> SubstSet .
  eq cond2sbs(mod,lhs := rhs) =
      (if thingVar(mod, soupT2tl(mod,lhs)) :: Variable
       then cond2sbsX(mod,thingVar(mod, soupT2tl(mod,lhs)), soupT2tl(mod,rhs)) 
       else mt fi) .
  eq cond2sbs(mod,cond) = mt [owise] .

  eq cond2sbsX(mod,v,empty) = mt .
  eq cond2sbsX(mod,v,(t,tl)) = (sb(v <- t) cond2sbsX(mod,v,tl)) .

**** op expandCond : Module Term Term Qid AttrSet SubstSet Nat -> RuleSet .
 eq expandCond(mod,ioccsT,ooccsT,rid, attrs,mt,n) = none .
 eq expandCond(mod,ioccsT,ooccsT,rid, attrs, sb(subst) sbs,n) =
      (rl substApp(subst,ioccsT) => substApp(subst,ooccsT) 
          [label(mkTransId(rid,n)) attrs] .)
     expandCond(mod,ioccsT,ooccsT,rid, attrs,sbs, s n) .

**** Given a set of variables, find all instances
****  op allInst : Module QidSet SubstSet -> SubstSet .
  eq allInst(mod,none, sbs) = sbs .
  ceq allInst(mod,v ; vs, sbs) = allInst(mod,vs,sbs')
***    if vals := constListBySort(upOpDecls('PROTEINOPS,true),  ****!!!!false
       if vals := constListBySort(upOpDecls(getName(mod),true),  ****!!!!false
                                (lesserSorts(mod,getType(v)) ; getType(v))) 
       /\ sbs' := extendSbS(sbs,v,vals) .
 *** skip non Var
  eq allInst(mod,qid ; vs, sbs) = allInst(mod,vs,sbs)  [owise] . 


****  op constListBySort : OpDeclSet  SortSet  -> TermList .
****  op constBySortZ : OpDecl  SortSet  -> TermList .
  eq constListBySort(none, sortset)  = empty .
  eq constListBySort(od:OpDecl ods:OpDeclSet, sortset) = 
       (constBySortZ(od:OpDecl, sortset) ,
       constListBySort(ods:OpDeclSet, sortset)) .

***!!!18apr04 suppressed constants with ? in name
  eq constBySortZ((op qid : tl:TypeList -> t:Type [atts:AttrSet] .),
                   sortset) 
      = if  ( ((tl:TypeList == nil) and (t:Type in sortset)) 
              and
              (find(string(qid),"?",0) == notFound)
             )
        then mkConst(qid,t:Type)
        else empty
        fi .

****  op extendSbS : SubstSet Variable TermList -> SubstSet .
****  op extendSbSX : SubstSet Variable Constant SubstSet -> SubstSet .

  eq extendSbS(sbs,v,empty) = mt .
  eq extendSbS(sbs,v, (const, vals)) = 
        extendSbSX(sbs,v,const, mt)  extendSbS(sbs,v,vals) .
  **** skip nonval
  eq extendSbS(sbs,v, (qid , vals)) = extendSbS(sbs,v,vals) [owise] . 

  eq extendSbSX(mt,v, const,sbs) = sbs .
  eq extendSbSX(sb(subst) sbs,v, const, sbs') = 
       extendSbSX(sbs,v,const, sbs' sb(subst ; v <- const)) .

****  op orules2pntl : Module RuleSet -> TermList .
****  op orule2pntl : Module Rule -> TermList .
****  op orule2pntlX : Module Term Term  Qid SubstSet Nat -> TermList .
****  op orule2pnt : Module Term Term  Qid Substitution Nat -> TermList .

  eq orules2pntl(mod,none) = empty .
  eq orules2pntl(mod,rule rules) = 
      orule2pntl(mod,rule) , orules2pntl(mod,rules) .

**** conditions have been eliminated from PL rules
  eq orule2pntl(mod,rl lhs => rhs [ label(rid) attrs ] .) = 
    orule2pntlX(mod,lhs,rhs,rid,allInst(mod,getVars(lhs),sb(none)),0) . 
**** ; getVars(getRhs(rule)) no need to get vars of rhs RIGHT??

  eq orule2pntlX(mod,lhs,rhs,rid,mt,n) = empty .
  eq orule2pntlX(mod,lhs,rhs,rid,sb(subst) sbs,n) =
      orule2pnt(mod,lhs,rhs,rid,subst,n),
      orule2pntlX(mod,lhs,rhs,rid,sbs,s n) .

**** CHECK HERE
**** 14nov09 need to check that preOccsT different from postOccT
  ceq orule2pnt(mod,lhs,rhs,rid,subst,n) = 
       (if (tl :: Term) then checkPNT(tl) else empty fi)
    if ridT := mkQidConst(mkTransId(rid,n))
    /\ preOccsT := substApp(subst,lhs)
    /\ postOccsT := substApp(subst,rhs)
    /\ res?? := metaReduce(mod,'mkPNTrans[ridT,preOccsT,postOccsT]) 
    /\ tl :=  (if res?? :: ResultPair then getTerm(res??) else empty fi) .

    op checkPNT : Term -> TermList .
    ceq checkPNT(t) =
      (if (ioccsT == 'none.Occs and ooccsT == 'none.Occs) then empty else t fi)
    if 'pnTrans[ridT,ioccsT,ooccsT,boccsT] := t .
    
    eq checkPNT(t) = empty [owise] .
    
**** pnTrans(rid,ioccs,ooccs,boccs)


****  op mkTransId : Qid Nat -> Qid .
  eq mkTransId(rid,0) = rid .
  eq mkTransId(rid,s n) = qid(string(rid) + "#" + string(s n,10)) .


*****************************************************************************
******!!!!HERE*****************************************************************
*****************************************************************************

**** To match a rule loccsT => roccsT in dishOccT, start with mtchnumber == 0
**** and add to the substitution set 
**** getSubstitution(metaXmatch([modname], 
****                  loccsT,dishOccsT,nil,0,unbounded,matchnumber))
**** until noMatch is returned.


************ ops on substitutions and rule instance sets *********************************
*** substitutions
*** sorts Assignment Substitution .
*** subsort Assignment < Substitution .
*** op _<-_ : Variable Term -> Assignment [ctor prec 63 format (nt d d d)] .
*** op none : -> Substitution [ctor] .
*** op _;_ : Substitution Substitution -> Substitution [ctor assoc comm id: none] .

**** assume range of subst is normalized -- loc, protein, simple modification
**** then syntactic equality of subst is semantic equalty (mod ac)
**** if we want modsets need to work harder to test subst equality


sort SubstSetRes .
op `{_`,_`} : Bool SubstSet -> SubstSetRes [ctor] .

op addSubst : SubstSet Substitution -> SubstSetRes .
eq addSubst(sb(subst) sbs,subst) = {false, sb(subst) sbs} .
eq addSubst(sbs,subst) = {true, sbs sb(subst)} [owise] .

sorts RInst RInstSet  .
subsort RInst < RInstSet .
op ri : Rule SubstSet -> RInst [ctor] .
op none : -> RInstSet [ctor] .
op __ : RInstSet RInstSet -> RInstSet [ctor assoc comm id: none ] .

**** associate each rule with the empty SubstSet
op initRInsts : RuleSet RInstSet -> RInstSet .
eq initRInsts(none,rinsts) = rinsts .
eq initRInsts(rule rules,rinsts) = initRInsts(rules,(rinsts ri(rule,mt))) .

**** turn a set of rule instances into a list of pnt terms
op rinsts2pntl : Module RInstSet TermList -> TermList .
op rinst2pntl : Module RInst TermList Nat -> TermList .
**** op orule2pnt : Module Term Term  Qid Substitution Nat -> TermList .
eq  rinsts2pntl(mod,none,tl) = tl .
eq  rinsts2pntl(mod,(rinst  rinsts),tl) =
      rinsts2pntl(mod,rinsts,rinst2pntl(mod,rinst,tl,0)) .

eq rinst2pntl(mod,ri((rl lhs => rhs [attrs] .),mt),tl,n) = tl .
eq rinst2pntl(mod,ri((rl lhs => rhs [label(rid) attrs] .),
                       sb(subst) sbs),tl,n) =
          rinst2pntl(mod,ri((rl lhs => rhs [label(rid) attrs] .), 
                       sbs), (tl,orule2pnt(mod,lhs,rhs,rid,subst,n)),s n) .


**** map pl rules of mod wrt union of all dishes to PNTransList term .

  op dnames2OccsT : Module QidList Term -> Term .
  eq dnames2OccsT(mod,nil,occsT) = occsT .
 ceq dnames2OccsT(mod,dname dnames,occsT) = dnames2OccsT(mod,dnames,occsT1)
  if res?? := metaReduce(mod, 'pl2occs[mkConst(dname,'Dish)])
  /\ occsT0 := 
      (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi)
  /\ res1?? := metaReduce(mod, 'addOccs[occsT,occsT0])
  /\ occsT1 :=
       (if res1?? :: ResultPair then getTerm(res1??) else 'none.Occs fi)
  .

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

**** map pl rules of mod wrt dish to PNTransList term .
op pld2tlt  : Qid Qid -> Term . 
ceq pld2tlt(modname,dname) = pldrules2tlt([modname],upRls(modname,true),occsT) 
  if res?? := metaReduce([modname], 'pl2occs[mkConst(dname,'Dish)])
  /\ occsT := (if res?? :: ResultPair then getTerm(res??) else 'none.Occs fi) .


**** map set of pl rules to PNTransList term relevant to occs Term .
**** first convert rules to occ form, then collect occs and rule insts
**** then convert ruleinsts to pnt term list, then to term.
op pldrules2tlt : Module RuleSet Term -> Term . 

eq pldrules2tlt(mod,rules,occsT) =
     pntTL2pntlT(odrules2pntl(mod, plrules2orules(mod,rules), occsT)) .

****                     Orules  occs
op odrules2pntl : Module RuleSet Term -> TermList .
eq odrules2pntl(mod,orules,occsT) = 
                odr2pntl(mod,initRInsts(orules,none),none,occsT,false) .

**** collect reachable dishes/occs and orule,substset pairs
**** return instantiated orules as pntTL.
****                 todo     done     occsT  more?
op odr2pntl : Module RInstSet RInstSet Term Bool -> TermList .
****                   cur   todo     done     occsT  more?
op odr2pntl1 : Module RInst RInstSet RInstSet Term  Nat Bool -> TermList .

**** round done
eq odr2pntl(mod,none,rinsts,occsT,more?) =
     (if more? 
      then odr2pntl(mod,rinsts,none,occsT,false) 
      else rinsts2pntl(mod,rinsts,empty) fi) .

        
eq odr2pntl(mod,(rinst rinsts),rinsts',occsT,more?) = 
         odr2pntl1(mod,rinst,rinsts,rinsts',occsT,0,more?) .

**** 18jul10 dealing with absent
var mpr? : MatchPair? .
ceq odr2pntl1(mod,ri((rl lhs => rhs [ attrs ] .),sbs),
                  rinsts,rinsts',occsT,n, more?) 
    =
    (if (mpr? :: MatchPair)
    then odr2pntl1(mod,ri((rl lhs => rhs [ attrs ] .),sbs'), rinsts, rinsts' ,
                    occsT',s n, (new? or more?))     
    else odr2pntl(mod,rinsts,rinsts' ri((rl lhs => rhs [ attrs ] .),sbs),
                  occsT',more?)   *** done with this rule
    fi) 
if mpr? := metaXmatch(mod, lhs,occsT,nil,0,unbounded,n)
/\ res1?? := (if (mpr? :: MatchPair) 
               then metaReduce(mod, 
                           'validOccs[substApp(getSubstitution(mpr?),rhs)])
               else failure fi)
/\ b := (if (res1?? :: ResultPair) 
        then downTerm(getTerm(res1??),false) 
        else false fi)
/\ res2?? := (if (mpr? :: MatchPair) and b
               then metaReduce(mod, 
                           'validIOOccs['absent.Modification,
                                        substApp(getSubstitution(mpr?),lhs),
                                        substApp(getSubstitution(mpr?),rhs)])
               else failure fi)
/\ b1 := (if (res2?? :: ResultPair) 
        then downTerm(getTerm(res2??),false) 
        else false fi)
/\ {new?,sbs'} := (if (b and b1)  ---- (mpr? :: MatchPair) and validOccs and validIOOccs
                  then addSubst(sbs,getSubstitution(mpr?) )
                  else {false,sbs} fi)
/\ res?? := (if (b and b1)               ---- (mpr? :: MatchPair) and valid
             then metaReduce(mod, 
                       'addOccs[substApp(getSubstitution(mpr?),rhs),occsT])
             else failure fi)
/\ occsT' := (if (res?? :: ResultPair) 
             then  getTerm(res??)
             else occsT fi) .



***(
ceq odr2pntl1(mod,ri((rl lhs => rhs [ attrs ] .),sbs),
                  rinsts,rinsts',occsT,n, more?) 
    =
    (if (mpr? :: MatchPair)
    then odr2pntl1(mod,ri((rl lhs => rhs [ attrs ] .),sbs'), rinsts, rinsts' ,
                    occsT',s n, (new? or more?))     
    else odr2pntl(mod,rinsts,rinsts' ri((rl lhs => rhs [ attrs ] .),sbs),
                  occsT',more?)   *** done with this rule
    fi) 
if mpr? := metaXmatch(mod, lhs,occsT,nil,0,unbounded,n)
/\ res1?? := (if (mpr? :: MatchPair) 
               then metaReduce(mod, 
                           'validOccs[substApp(getSubstitution(mpr?),rhs)])
               else failure fi)
/\ b := (if (res1?? :: ResultPair) 
        then downTerm(getTerm(res1??),false) 
        else false fi)
/\ {new?,sbs'} := (if b        ---- (mpr? :: MatchPair) and validOccs
                  then addSubst(sbs,getSubstitution(mpr?) )
                  else {false,sbs} fi)
/\ res?? := (if b              ---- (mpr? :: MatchPair) and valid
             then metaReduce(mod, 
                       'addOccs[substApp(getSubstitution(mpr?),rhs),occsT])
             else failure fi)
/\ occsT' := (if (res?? :: ResultPair) 
             then  getTerm(res??)
             else occsT fi) .

)

endfm
