# 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]))