# main entry point of the strategy.

# Here, the Haskell reductions (all ending in Reduction) are called, that _must_ be called in this order, since there are some dependencies.

# The HaskellSplit processor takes the set of start terms and makes multiple problems with one start term each.

# The HaskellNarrowing processor is the core of the termination proof: It applies evaluations to the start term, looking for

# loops in the call structure. Here the Haskell lazy evaluation, (type) case splitting, and generalizations are performed.

# The last command, mainQDP, calls the subfunction declared later; this will work on the DP Problems generated by the HaskellNarrowing processor

main = HaskellLambdaReduction:HaskellCaseReduction:HaskellIfReduction:HaskellIrrPatReduction:HaskellBindingReduction:HaskellCondReduction:HaskellNewTypeReduction:HaskellIrrPatReduction:HaskellLetReduction:HaskellNumReduction:HaskellSplit:HaskellNarrowing[AddTypes = False]:mainQDP

# subfunction mainQDP

# Here, the processors QDPDependencyGraph, QDPATransformaion, and QDPPolo are called in the order listed. The first one to succeed

# is taken (because of the keyword First) and the process is started over (because of the keyword Repeat).

# The arguments 0,* of Repeat mean that as long as there is one processor inside the First that succeeds, try again

# The QDPDependencyGraph processor looks at the DP problem and builds a new estimation of the Dependency Graph

# The QDPATransformation processor can transform a non-higher-order program into standard form (eliminating the app-symbol)

# The QDPPolo processor searches for a polynomial ordering such that all left hand sides are greater or equal than right hand sides

# and removes the strictly ordered ones

# This processor gets the parameter Range, which specifies what kind of polynomials are to be searched: Range=1 means that all

# coefficients are from the range {0,1}

mainQDP = Repeat(0,*,First(QDPDependencyGraph,QDPATransformation,QDPPolo[Range=1]))