# 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]:workOnQDP


# subfunction workOnQDP
# Here, the processors QDPDependencyGraph, QDPATransformaion, QDPSizeChange (in different configurations), 
# the subfunction parallel, 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 QDPSizeChange processor looks for decreases in the term structure
# 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. The coefficients are from range {0,1,2}, the maximum degree is 1 and argument filterings are
# considered when looking for usable rules

workOnQDP = RepeatS(0,*,First(QDPDependencyGraph, QDPATransformation, QDPSizeChange[Subterm=True],  QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=0,AfsRestriction=2], parallel,QDPPolo[Range=2,Degree=1,Active=True]))

# subfunction parallel
# tries in parallel the Size Change and RuleRemoval processors for a maximum of 5000 ms
# thereafter, a polynomial ordering is searched, where the coefficients are from the 
# range {0,1}, maximum degree is 1, and if there is an argument filtering, take this into
# account when searching for usable rules
parallel = First(Timer(5000,Any(QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=2,AfsRestriction=2], QDPRuleRemoval[Range=2])), Timer(30000,QDPPolo[Range=1,Degree=1,Active=True]))