(fmod METATEST is
 protecting META-LEVEL[RBP] .

sorts StrategyExpression Strategy .
sorts TermSet SetOfTermLists .
subsort Term < TermSet .
subsort TermList < SetOfTermLists .

op apply : Qid -> Strategy .
op applySomewhere : Qid -> Strategy .
op applySomewhereSubst : Qid Substitution -> Strategy .

op first : ResultPair -> Term .
op use : Module Term Qid Substitution -> Term .
op uselist : Module TermList Qid Substitution -> TermList .

*** Somewhat trickier ones to find all possible rewrites
*** using one rule at the top of the term:
op emptyTermSet : -> TermSet .
op set : TermSet TermSet -> TermSet [assoc comm id: emptyTermSet] .
op applyAll : Module Term Qid -> TermSet .
op applyAllHelp : Module Term Qid MachineInt -> TermSet .


var M : Module . var T : Term . var RL : Qid . var SUBST : Substitution .
var TL : TermList . var F CONST SORT : Qid . var S S' : Strategy .
var N : MachineInt .

eq first({T,SUBST}) = T .

eq use(M,F,RL,SUBST) = first(meta-apply(M,F,RL,SUBST,0)) .
eq use(M,{CONST}SORT,RL,SUBST) = first(meta-apply(M,{CONST}SORT,RL,SUBST,0)) .
eq use(M,F[TL],RL,SUBST) = 
          if first(meta-apply(M,F[TL],RL,SUBST,0)) == error*
          then (if uselist(M,(TL),RL,SUBST) == error* then error*
                else F[uselist(M,(TL),RL,SUBST)] fi)
          else first(meta-apply(M,F[TL],RL,SUBST,0)) fi .

eq uselist(M,T,RL,SUBST) = use(M,T,RL,SUBST) .
eq uselist(M,(T,TL),RL,SUBST) = if use(M,T,RL,SUBST) == error* then
                                  (if uselist(M,TL,RL,SUBST) == error* 
                                   then error*
                                   else (T,uselist(M,TL,RL,SUBST)) fi)
                                else (use(M,T,RL,SUBST),TL) fi .

*** This finds all the rewrites at top position in current term and rule:
eq applyAll(M,T,RL) = applyAllHelp(M,T,RL,0) .
eq applyAllHelp(M,T,RL,N) = 
           if first(meta-apply(M,T,RL,none,N)) == error* 
           then emptyTermSet
           else set(first(meta-apply(M,T,RL,none,N)),
                    applyAllHelp(M,T,RL,N + 1)) fi .

eq set(T,T) = T .
*** We now define the list of terms that can be reached by one rewrite step
*** [using a particular rule] that can be reached from some term.

op allRewrites : Module Term Qid -> TermSet .    *** all one-step rewrites 
                                                 *** from current term 
                                                 *** using a rule.
op emptySTL : -> SetOfTermLists .
op setTL : SetOfTermLists SetOfTermLists -> SetOfTermLists [assoc comm id: emptySTL] .
op allRewritesList : Module TermList Qid -> SetOfTermLists .
op useOn : Qid SetOfTermLists -> TermSet .
op tosetTL : TermSet -> SetOfTermLists .  *** Conversion.
op appfirst : TermSet SetOfTermLists -> SetOfTermLists .

vars TS TS' : TermSet .
vars STL STL' : SetOfTermLists .


eq setTL(TL,TL) = TL .

eq allRewrites(M,F,RL) = applyAll(M,F,RL) .
eq allRewrites(M,{CONST}SORT,RL) = applyAll(M,{CONST}SORT,RL) .
eq allRewrites(M,F[TL],RL) = set(applyAll(M,F[TL],RL),
                                 useOn(F,allRewritesList(M,TL,RL))) .
eq useOn(F,emptySTL) = emptyTermSet .
eq useOn(F,TL) = F[TL] .
eq useOn(F,setTL((TL),(STL))) = set(F[TL],useOn(F,STL)) .
*** strictly speaking, there is the need to add a meta-reduce
*** to F[TL] in the right-handside of the last equation, but since
*** it is unnecessary for configurations, it is omitted for
*** efficiency purposes

eq allRewritesList(M,T,RL) =   tosetTL(allRewrites(M,T,RL)) .
ceq allRewritesList(M,(T,TL),RL) = 
       setTL(appfirst(allRewrites(M,T,RL),(TL)),
             appfirst(T,allRewritesList(M,TL,RL))) if TL =/= nil .

*** This is rather the "product" between the set(list)
*** of first terms and the set (list) of termlists.
*** e. g., "[t;u;v] appfirst [(t1,t2);(t5,t6,t7)]" equals
*** [(t,t1,t2);(u,t1,t2);(v,t1,t2);(t,t5,t6,t7);(u,t5,t6,t7);(v,t5,t6,t7)]
eq appfirst(TS,emptySTL) = emptySTL .
eq appfirst(emptyTermSet,STL) = emptySTL .
ceq appfirst(T,setTL(TL,STL)) = setTL((T,TL), appfirst(T,STL)) 
                                if STL =/= emptySTL .
eq appfirst(T,TL) = (T,TL) .
ceq appfirst(set(T,TS),STL) = setTL(appfirst(T,STL), appfirst(TS,STL)) 
                              if TS =/= emptyTermSet .

*** Takes a TermSet into a SetOfTermLists (where each list is 
*** a singleton).
eq tosetTL(emptyTermSet) = emptySTL .
eq tosetTL(T) = T .
eq tosetTL(set(T,TS)) = setTL(T,tosetTL(TS)) .

*** allRewrites is extended to sets of rules:
op allRewrites : Module Term QidSet -> TermSet .
var QS : QidSet .
eq allRewrites(M,T,none) = emptyTermSet .
ceq allRewrites(M,T,(RL ; QS)) = set(allRewrites(M,T,RL),
                                     allRewrites(M,T,QS)) if QS =/= none .

*** Find irreducible forms:
op irreducibleforms : Module Term QidSet -> TermSet .
*** This calls irf(Module,termsToCheckInThisRound,TermsCheckedInThisRound,QS)
op irf : Module TermSet TermSet QidSet -> TermSet .

*** Trigger:
eq irreducibleforms(M,T,QS) = irf(M,meta-reduce(M,T),emptyTermSet,QS) .

*** End of process:
eq irf(M,emptyTermSet,emptyTermSet,QS) = emptyTermSet .

*** Next round:
eq irf(M,emptyTermSet,set(T,TS),QS) = irf(M,set(T,TS),emptyTermSet,QS) .

*** Find "next-round-form" of current term, if any, 
*** else add it to the set of irreducible forms:
ceq irf(M,set(T,TS),TS',QS) = set(T,irf(M,TS,TS',QS)) 
                              if allRewrites(M,T,QS) == emptyTermSet .
ceq irf(M,set(T,TS),TS',QS) = irf(M,TS,set(allRewrites(M,T,QS),TS'),QS)
                              if allRewrites(M,T,QS) =/= emptyTermSet .

***
*** Specific constants for this example:
***
op allstaticrules : -> QidSet .   *** all rules in the static spec
eq allstaticrules =  ('Start ; 'RecMessage1 ; 'RecMessage2 ; 'AckParent ; 'RecAckParent ; 'RecAckSibling ; 'ResetSource ) .


op alldynamicrules : -> QidSet .
eq alldynamicrules =  ('Send ; 'RepeatRecCurrentMsg ; 'RecNewMsg ; 'RecNewMsgLeaf ; 'ActiveRecOldMsg ; 'PassiveRecOldMsg ; 'MsgNotReceivable ; 'RecAckNewerMsg ; 'PassiveRecAckCurrentMsg ; 'ActiveRecAckCurrentMsg ; 'ActiveRecAckCurrentMsgNoParent ; 'UndefRecAckCurrentMsg ; 'ActiveRecAckOldMsg ; 'PassiveRecAckOldMsg ; 'RecAckForNewSource ; 'AckNotReceivable ; 'Link ; 'MultiLinkUp ; 'ActiveLink ; 'PassiveLink ; 'Failure ; 'MultiLinkDown ; 'ActiveFailure ; 'UndefActiveFailure ; 'PassiveFailure ; 'FailureNoSrc ) .


endfm)