fmod STRATEGY is
  protecting META-LEVEL .
  op apply : Module Term Qid -> Term .
  op extTerm : ResultPair -> Term .
  op extSubst : ResultPair -> Substitution .

  var M : Module .   
  var T : Term . 
  var L : Qid .      
  var SB : Substitution .

  eq apply(M, T, L) = extTerm(meta-apply(M, T, L, none, 0)) .
   
  eq extTerm({T, SB}) = T .
  eq extSubst({T, SB}) = SB .

  op applyWithSubst : Module Term Qid Substitution -> Term .

  eq applyWithSubst(M, T, L, SB) = extTerm(meta-apply(M, T, L, SB, 0)) .
 
  op applyIf : Module Term Qid Term MachineInt -> Term .
  op substitute : Term Substitution -> Term .
  op substituteAux : TermList Substitution -> TermList .

  var C : Term .

  eq applyIf(M, T, L, C, N)
    = if meta-apply(M, T, L, none, N) == {error*, none} 
      then error*
      else (if meta-reduce(M, substitute(C, 
                                extSubst(meta-apply(M, T, L, none, N))))
               == {'true}'Bool
            then extTerm(meta-apply(M, T, L, none, N))
            else  applyIf(M, T, L, C, (N + 1)) fi) fi .

  vars F S X Y : Qid .   
  var TL : TermList .

  eq substitute(T, none) = T .
  eq substitute(X, ((Y <- T); SB))
    = if X == Y then T else substitute(X, SB) fi .
  eq substitute({F}S, SB) = {F}S .
  eq substitute(F[TL], SB) = F[substituteAux(TL, SB)] .
  eq substituteAux((T, TL), SB) 
    = (substitute(T, SB), substituteAux(TL, SB)) .
  eq substituteAux(T, SB) = substitute(T, SB) . 

  sorts Node Tree TreeList Solution Position .

  op step : Qid ResultPair -> Node [ctor] .
  op tree : Node TreeList -> Tree [ctor] .
  op treeL : Tree TreeList -> TreeList [ctor] .
  op nilTreeL : -> TreeList [ctor] .

  op pos : MachineInt Position -> Position [ctor] .
  op nilPos : -> Position [ctor] .

  op sol : Node Solution -> Solution [ctor] .
  op nilSol : -> Solution [ctor] .

  op nextPos : Tree Position -> Position .
  op right : Position -> Position .
  op down : Position -> Position .
  op getNode? : Tree  -> Bool .
  op getNode : Tree  -> Node .
  op extTermNode : Node -> Term .
  op getSubTree : Tree Position -> Tree .
  op getSubTreeL : TreeList MachineInt -> Tree .
  op addSubTree : Tree Tree Position -> Tree .
  op addSubTreeL : TreeList Tree Position -> TreeList .
  op appendTreeL : TreeList TreeList -> TreeList .
  op extSol : Tree Position -> Solution .
  op extSolAux : TreeList Position -> Solution .
  op appendSol : Solution Solution -> Solution .

  vars QL QL' : QidList .  var Nd : Node .            
  vars Tr Tr' : Tree .     vars TrL TrL' : TreeList . 
  var P : Position .       vars Sol Sol' : Solution .
  var N : MachineInt .

  eq nextPos(Tr, P)
    = if getNode?(getSubTree(Tr, right(P))) == true
      then right(P) else down(P) fi .

  eq right(pos(N, P)) 
    = if P == nilPos then pos((N + 1), P) else pos(N, right(P)) fi .

  eq down(nilPos) = pos(1, nilPos) .
  eq down(pos(N, P)) = pos(N, down(P)) .

  eq getNode?(tree(Nd, TrL)) = true .

  eq getNode(tree(Nd, TrL)) = Nd .
  
  eq extTermNode(step(L, {T, SB})) = T .

  eq getSubTree(Tr, nilPos) = Tr .

  eq getSubTree(tree(Nd, TrL), pos(N, P)) 
    = getSubTree(getSubTreeL(TrL, N), P) .

  eq getSubTreeL(treeL(Tr, TrL), N)
    = if N == 1 then Tr else getSubTreeL(TrL, _-_(N, 1)) fi .
 
  eq addSubTree(tree(Nd, TrL), Tr, nilPos)
    = tree(Nd, appendTreeL(TrL, treeL(Tr, nilTreeL))) .

  eq addSubTree(tree(Nd, TrL), Tr, pos(N, P))
    = tree(Nd, addSubTreeL(TrL, Tr, pos(N, P))) .

  eq addSubTreeL(treeL(Tr, TrL), Tr', pos(N, P))
    = if N == 1 
      then treeL(addSubTree(Tr, Tr', P), TrL) 
      else treeL(Tr, addSubTreeL(TrL, Tr', pos(_-_(N, 1), P))) fi .

  eq appendTreeL(nilTreeL, TrL) = TrL .
  eq appendTreeL(treeL(Tr, TrL), TrL') 
    = treeL(Tr, appendTreeL(TrL, TrL')) .

  eq extSol(tree(Nd, TrL), nilPos) = sol(Nd, nilSol) .
  eq extSol(tree(Nd, TrL), pos(N, P)) 
    = sol(Nd, extSolAux(TrL, pos(N, P))) .

  eq extSolAux(treeL(Tr, TrL), pos(N, P))
    = if N == 1 then extSol(Tr, P) 
                else extSolAux(TrL, pos(_-_(N, 1), P)) fi .

  eq appendSol(nilSol, Sol) = Sol .
  eq appendSol(sol(Nd, Sol), Sol') = sol(Nd, appendSol(Sol, Sol')) .

  op findPlan : Module Tree Position Term 
                QidList QidList MachineInt -> Solution .

  op findPlanAux : Module Tree Position Term 
                   QidList QidList MachineInt Node -> Solution .

  var RP : ResultPair .

  eq findPlan(M, Tr, P, T, (L QL), QL', N)   
    = if meta-apply(M, extTermNode(getNode(getSubTree(Tr, P))), 
                    L, none, N)  == {error*, none}
      then findPlan(M, Tr, P, T, QL, QL', 0)
      else findPlanAux(M, Tr, P, T, (L QL), QL', N,
          step(L, meta-apply(M, extTermNode(getNode(getSubTree(Tr, P))),
                             L, none, N)))
      fi .

  eq findPlan(M, Tr, P, T, nil, QL', N) 
    = findPlan(M, Tr, nextPos(Tr, P), T, QL', QL', 0) .

  eq findPlanAux(M, Tr, P, T, QL, QL', N, step(L, RP)) 
    = if meta-reduce(M, '_==_[T, extTerm(RP)]) == {'true}'Bool
      then appendSol(extSol(Tr, P), sol(step(L, RP), nilSol))
      else findPlan(M, addSubTree(Tr, tree(step(L, RP), nilTreeL), P), 
                    P, T, QL, QL', (N + 1)) 
      fi .
endfm